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!
Best Answer
In principle, the answer can depend on the proof system, but as long as you stick to some of the usual Hilbert-style or sequent proof systems, this shouldn’t matter.
First, as explained in https://mathoverflow.net/questions/120106, the question is equivalent to provability of the consistency of FPA in $I\Delta_0+\Omega_1$. (The fact that you are using second order objects to encode proofs and formulas corresponds to using all numbers instead of just the logarithmically small ones in $I\Delta_0+\Omega_1$, hence you end up with the usual consistency statement.)
Now, working in $I\Delta_0+\Omega_1$ (or equivalently, Buss’s $S_2$), the consistency of FPA is equivalent to the consistency of the second-order theory of the model with one-element first-order universe (in whatever finite language, it’s all equivalent), since the two theories are interpretable in each other. This in turn can be reduced to the quantified propositional calculus: since there is only one first-order element (and only one $n$-tuple of elements for every $n$), you can ignore first-order quantifiers and variables, and replace second-order variables with propositional variables both in second-order quantifiers and in atomic formulas. (Purely first-order atomic formulas such as $t=s$ can be replaced with the constant $\top$ for truth.) Thus, the question becomes whether $I\Delta_0+\Omega_1$ proves the consistency of the quantified propositional calculus ($G$).
The answer is that this is one of the major open problems in the area, but it is conjectured to be false. There is a kind of correspondence of subsystems of bounded arithmetic to propositional proof systems; in particular, the fragments $T^i_2$ of $S_2$ (${}=I\Delta_0+\Omega_1$) correspond to the fragments $G_i$ of the quantified propositional calculus, obtained by restricting all formulas in the proof (or alternatively, all cut formulas in the sequent calculus formulation) to $\Sigma^q_i$ or $\Pi^q_i$ formulas (= formulas in prenex form with at most $i$ quantifier blocks). This means:
$T^i_2$ proves the consistency (and even some form of reflection principle) of $G_i$.
Conversely, $\mathrm{Con}_{G_i}$ implies over a weak base theory all $\forall\Delta^b_1$-consequences of $T^i_2$ (and more complex consequences of $T^i_2$ can be axiomatized by an appropriate reflection principle). A related fact is that if $T^i_2$ proves a $\forall\Sigma^b_i$ statement, one can translate it into a sequence of quantified propositional tautologies which will have polynomially bounded proofs in $T^i_2$.
If $P$ is any propositional proof system whose consistency is provable in $T^i_2$, then $G_i$ polynomially simulates $P$.
$S_2$ is the union of its finitely axiomatizable fragments $T^i_2$. This means that $S_2$ proves the consistency of each fragment $G_i$, but on the other hand, if it proved the consistency of the full quantified propositional calculus $G$, it would imply that $G_i$ polynomially simulates $G$ for some $i$, and this is assumed to be false. To put it differently, the $\forall\Delta^b_1$-consequences of $S_2$ (as well as $S_2$ itself) are not assumed to be finitely axiomatizable.
The correspondence of theories and propositional proof systems also extends to complexity classes. Sets definable by $\Sigma^b_i$ formulas in the standard model of arithmetic are exactly those computable in the $i$-level $\Sigma^P_i$ of the polynomial hierarchy. The theories $T^i_2$ have induction for $\Sigma^b_i$ formulas, and their provably total $\Sigma^b_{i+1}$-definable functions are $\mathrm{FP}^{\Sigma^P_i}$, so these theories correspond to levels of the polynomial hierarchy. On the propositional side, satisfiability of $\Sigma^q_i$ formulas is a $\Sigma^P_i$-complete problem. Taking the union, $S_2$ corresponds to the full polynomial hierarchy $\mathrm{PH}$. However, the complexity class corresponding to $G$ is $\mathrm{PSPACE}$, as satisfiability of unrestricted quantified propositional formulas is $\mathrm{PSPACE}$-complete. Thus, asking $S_2$ to prove the consistency of $G$ is in the same spirit as collapsing $\mathrm{PSPACE}$ to $\mathrm{PH}$ (and therefore to some its fixed level). (Don’t quote me on this. While the collapse of the $T^i_2$ hierarchy does imply the collapse of $\mathrm{PH}$, for propositional proof systems this becomes only a loose analogy.)
In order to give also an upper bound on the consistency strength, the consistency of $G$, and therefore of FPA, is provable in theories corresponding to $\mathrm{PSPACE}$. The best known such theory is Buss’s theory $U^1_2$, which is a “second-order” extension of $S_2$ with comprehension for bounded sets defined by bounded formulas without second-order quantifiers, and length induction for bounded $\Sigma^1_1$-formulas. Notice that things get really messy here, as the first-order objects of $U^1_2$ correspond to second-order objects of FPA, and second-order objects of $U^1_2$ have no analogue in FPA. Alan Skelley formulated an equivalent (technically, RSUV-isomorphic) theory $W^1_1$. This is syntactically a third-order arithmetic, and it is more directly comparable to FPA (as numbers of one theory correspond to numbers of the other, and sets correspond to sets). $W^1_1$ proves the consistency of $G$, and thus of FPA.