[FOM] Provability of Consistency

[Artemov, Sergei]

All mathematical statements in Anton Freund’s post are correct. However, it appears that this post misrepresents Hilbert’s program and hence misses the main point of the PoC paper.  

I am not an expert in the history of logic, but the claim “Hilbert's program is more about Pi^0_1-reflection than about consistency,” appears to refer to post-G2 reformulations of Hilbert’s Program made retroactively to fit G2/Con(PA) format. When Hilbert’s program appeared in the 1920s, arithmetization did not exist yet, so Con(T)/Pi^0_1-reflection just cannot be the original formulation. 

The whole idea of the PoC paper is to show that Con(T) formula distorts the mathematical notion of consistency from the original Hilbert’s program: 
“The goal of Hilbert's program is then to give a contentual, metamathematical proof that there can be no derivation of a contradiction, i.e., no formal derivations of a formula A and of its negation ¬A.” 
(From R. Zach. Hilbert's Program, The Stanford Encyclopedia of Philosophy (Spring 2016),
URL = https://plato.stanford.edu/archives/spr2016/entries/hilbert-program/)

In the same SEP article, “Hilbert’s program,” there is not a single mentioning of Pi^0_1-reflection. 

Please read Section 1.1 of the PoC paper “Consistency problem: lost in translation” which offers a pedestrian analysis of this matter. In the nutshell: Hilbert asked about mathematical consistency of REAL derivations. Subsequent arithmetization as the formula Con(T) has distorted the problem due to weakness of the first-order arithmetic and existence of non-standard models. Since G2 deals with Con(T) which is stronger than Hilbert’s metamathematical notion of consistency, G2’s claim that PA|-/-Con(PA) does not close the possibility of proving mathematical consistency of PA in PA. The PoC paper does what G2/Con(PA) did not and could not do: provides a proof of Hilbert’s consistency of PA formalizable in PA. 

In summary, Anton Freund’s post is mathematically correct, but not quite relevant. 

I am also taking this opportunity to express my deep respect to mathematical work made in this area of proof theory by many authors, including Pavel Pudlak whose survey has been cited in the PoC paper.   

Sergei Artemov

________________________________________
From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Anton Freund [freund at mathematik.tu-darmstadt.de]
Sent: Monday, March 25, 2019 3:09 PM
To: fom at cs.nyu.edu
Subject: Re: [FOM] Provability of Consistency

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.

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
https://urldefense.proofpoint.com/v2/url?u=https-3A__cs.nyu.edu_mailman_listinfo_fom&d=DwIFAw&c=8v77JlHZOYsReeOxyYXDU39VUUzHxyfBUh7fw_ZfBDA&r=vtfGbdUbVrB70ksnRgFs_T_U9JW0KuiKAy7FCssagUA&m=jub6x76nZG7Iua8gsyGqykObAjBkrzF1MfXOs06H-I4&s=fVZ0v-aY3n3hVhZUEBWXK3b964YnGI8XiRpzpLIm4kI&e=