[FOM] Provability of Consistency

[Anton Freund]

I would like to add a few thoughts to the discussion about Sergei
Artemov's paper on finite consistency proofs:

(1) As far as I understand, Hilbert's program is more about
Pi^0_1-reflection than about consistency. The idea is that
Pi^0_1-statements are particularly meaningful, because all their instances
are decidable and they can be refuted by concrete counterexamples. It is
well-known that consistency (in the usual sense) implies
Pi^0_1-reflection: Given a PA-proof of (all x.phi(x)) with a
quantifier-free formula phi, we want to show that (all x.phi(x)) is true.
Aiming at a contradiction, assume that there is a number y such that
phi(y) fails. Since phi defines a decidable property this failure can be
detected by an explicit verification. By formalizing this verification one
obtains a PA proof of (not phi(y)) (this step is known as
Sigma^0_1-completeness). Together with the given PA-proof of (all
x.phi(x)) one obtains a PA-proof of a contradiction. But we have assumed
that PA is consistent. So (all x.phi(x)) must be true after all. The
finite consistency statements of Artemov do not allow to deduce
Pi^0_1-reflection (because the number y in the above argument may be
"non-standard", so that the proof of (not phi(y)) in PA has "non-standard
code"). Thus they do not revive this crucial aspect of Hilbert's program.

(2) It seems that the goal of Hilbert's program was to prove
\Pi^0_1-reflection (or consistency) for PA in a theory T that is weaker
than PA (I believe that the expression "finitistic" usually refers to
primitive recursive arithmetic, which is much weaker than PA). Here
Gödel's theorem provides a definite obstruction: If T is weaker than PA,
then PA will typically prove the \Pi^0_1-statement Con(T) while T does not
(note that this is not about the interpretation of Con(T), just about the
fact that it is a \Pi^0_1-statement).

(3) I would like to point out related results by Pavel Pudlák: In his
paper "On the length of proofs of finitistic consistency statements in
first order
theories" (Logic Colloquium 1984) he shows that the formalization of
partial satisfaction leads to *polynomial length* proofs for the finite
consistency of PA in PA itself. Pudlák has conjectured that there are no
polynomial PA-proofs for the finite consistency of considerably stronger
theories (see also his recent survey on "Incompleteness in the finite
domain", BSL 23(4) 2017). Some recent progress can be found in
arXiv:1712.03251.