# [FOM] Provability of Consistency

Mon Mar 25 15:09:10 EDT 2019

```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