I will ask the question first and then explain.

QUESTION: FPA can prove its own consistency in the Godelian sense. But can it really prove its consistency?

FPA is a multi-sorted first-order theory, with lower-case or small letters (for numbers) and upper-case or big letters for relations of n-arity (n >= 1). (Practically, I think one can limit the theory to relations where n = 1, 2, or 3.)

Full comprehension is assumed.

FPA has a constant symbol 0, a 1-ary relationship N (natural number), and a 2-ary relationship symbol S (successoring).

In this context the Peano Axioms can be written:

(PA1) N0

(PA2) $\forall$n (Nn $\Rightarrow$ $\exists$m (Nm & Sn,m))

(PA3) $\forall$n$\forall$m$\forall$m' (Nn & Nm & Nm' & Sn,m & Sn,m' $\Rightarrow$ m = m')

(PA4) $\forall$n$\forall$m$\forall$n' (Nn & Nm & Nn' & Sn,m & Sn',m $\Rightarrow$ n = n')

(PA5) $\forall$n (Nn $\Rightarrow$ $\neg$ Sn,0)

(PA6) $\forall$P (P0 & $\forall$n$\forall$m(Pn & Sn,m $\Rightarrow$ Pm) $\Rightarrow$
$\forall$n(Nn $\Rightarrow$ Pn))

FPA assumes all the Peano Axioms except (PA2), that is, everything except the totality of the successor relationship. It has as its standard models all the initial segments as well as the standard model of the natural numbers. {0} is a model. It is therefore agnostic as to whether the natural numbers go on and on.

In FPA it is possible to define formula for addition, multiplication, less than, exponentiation, and, except obviously for totality and any related property, prove the usual properties. Intuitively, the existence of a natural number n implies that every number less than n exists.

Predicates for numbers can be defined:

one(n) if and only if S0,n & Nn,

two(n) if and only if $\exists$x (one(x) & Sx,n) & Nn

Obviously one cannot prove there exists any n such that one(n). But if such an n exists, then one can show it has all the usual properties of 1. Similarly for two, three, etc.

FPA proves the Fundamental Theorem of Arithmetic.

Recursion is available and it is possible to define formula expressing syntax in the Godel fashion. For instance, Term1(n) ("n is a lower-case term") might be defined as: seven(n) $\vee$ $\exists$y$\exists$z (+(y,y,n) & eleven(z) & z >= n). (Seven(n) expresses n is 0, and the lower-case variables are the even numbers >= eleven.)

One can continue and define a formula GProof(n,x) which says that n is the Godel number of a proof in FPA of a wff whose Godel number is x. Letting $\mathcal{F}$ be "$\neg$ 0 = 0", then GCons(FPA) is the formula:

$\neg$ $\exists$p (GProof(p,$\mathcal{F}$))

But FPA proves GCons(FPA). Intuitively the reasoning goes like this. Suppose $\neg$ GCons(FPA). Then there is a number p such that GProof(p,$\mathcal{F}$). But, because of the nature of Godelization, and its use of a single number to represent sequences of numbers via exponentiation, this is a very big number, easily bigger than what is required to define "true in {0}" for all propositions of length smaller than the propositions in the purported proof. FPA can show the axioms are true in {0}, that the deduction rules preserve truth in {0} for all steps in the proof, but of course $\mathcal{F}$ is not true in {0}. Contradiction, so FPA proves GCons(FPA).

Well this does seem like a bit of a cheat, because it uses the fact that Godelization, by using numbers to represent sequences, needs very big numbers. Instead of lower-case numbers to code a sequence, one can use upper-case letters: R is a sequence if and only if dom(R) is {x : x <= n} for some natural number n. One can then redefine a formula RProof(R,S) which says that R is a sequence representing a proof of the proposition represented by the sequence S. And define a new formula RCons(FPA).

The question is: does FPA prove RCons(FPA)?

The proof for the Godelization formula doesn't go through because now only a small number (the length of the proof) is implied, and this is not enough, at least prime facie, to construct a model of true-in-{0} for the propositions in the proof. To show that FPA proves RCons(FPA), it would suffice to show that any proof of an inconsistency would have to be very, very long. To show that FPA doesn't prove RCons(FPA), maybe Godel's original proof would go through, but this makes me nervous, because of the problem with GCons(FPA).

Sorry for the long question, but any help appreciated!