[FOM] Provability of Consistency

[Artemov, Sergei]

Well, I feel misunderstood. Perhaps, I have not been focusing on the heart of the matter enough. One more attempt. After many exchanges, this will be a quick one. 

We have been questioning logical adequacy of Con(PA) as The model of consistency, and its failure to exactly model “no natural number is a code of a PA-proof of 0=1.” 

However, I agree, Con(PA) does the G2 job, to some extent. By the formalization principle, for any finitely established Pi_1-sentence “for all natural numbers n=0,1,2,… P(n) holds” its arithmetization “as is” \forall x.P(x) is provable in PA. By Goedel’s fixed point argument, if PA is consistent, then PA|-/- Con(PA). Hence “for all natural numbers n=0,1,2,… P(n) holds” is not finitarily provable. With all my skepticism w.r.t. Con(PA) as the right model for consistency (due to missing domain condition), it does the job. Like each human casts a shadow, X has no shadow, hence X is not human - this is a correct argument, though all remarks that a shadow is not a good model of a human remain valid.  

The point though is somewhere else. 

1. The formalization principle applies to schemes of sentences as well, not only to single sentences. A scheme S is true/provable iff each instance of S is true/provable, the standard way. A scheme is finitarily provable if each instance of S is. 

2. We need to consider schemes, since o/w even some most basic notions, such as induction, which are obviously finitarily provable (as the basic ingredient of PA) are not provable as sentences. There are more examples of this kind. 

3. The classical G2/Con(PA) argument deals with arithmetical condition “for all natural numbers n=0,1,2,… ~Proof(n,0=1)” and shows that this condition is not finitary provable. However, Hilbert, if we trust the SEP article “Hilbert’s Program”, starts with combinatorial formulation “no finite sequence S is a PA-proof of 0=1” which is not about natural numbers. Within the mathematical tradition, a mathematician can view Hilbert’s consistency equivalently as an informal quantified statement “for all finite sequences S, S is not a PA-proof of 0-1”, or as a scheme “S is not a PA-proof of 0-1” with parameter S ranging over finite sequences of formulas. After applying Goedel numbers, we will get either an informal P_1 arithmetical sentence “for all natural numbers n=0,1,2,… ~Proof(n,0=1)” or a scheme “~Proof(n,0=1)” for all n=0,1,2,…. There conditions on (standard) natural numbers are still equivalent to a mathematician. 

4. Applying the formalization principle, we end up with either Con(PA) or ConS(PA), which behave radically different. In particular, ConS(PA) is finitarily provable (hence PA proves ConS(PA) as well). Since ConS(PA) is a LEGITIMATE formalization of PA-consistency, this makes my point: G2’s impossibility spell is no longer absolute, a straight formalization of Hilbert’s notion of consistency, ConS(PA), is finitarily provable. 

Everybody is welcome to compare arithmetical models of consistency Con(PA) and ConS(PA), their pro et contra, like them or not, but ConS(PA) has the right to exist and be a part of the proof theoretical and foundational landscape. 

There are three obvious strong points in ConS(PA) vs. Con(PA). 

i) ConS(PA) respects the domain condition and does not spill over to nonstandard natural numbers and hence is well principled in this department. 

ii) ConS(PA) is internally provable, which breaks the G2 impossibility barrier and vindicates Hilbert’s consistency Program.

iii) ConS(PA) opens a new research avenue in proof theory and foundations. 

Respectfully.
Sergei

Sorry, it took me so long to formulate my position in one blurb.
 
________________________________________
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, April 1, 2019 4:10 AM
To: fom at cs.nyu.edu
Subject: Re: [FOM] Provability of Consistency

Dear Sergei,

Thank you again for your explanations! I agree that we should not prolong
this line of discussion much more, because I think that most arguments
have been made explicit. Nevertheless I would like to clarify my own
position with respect to our last exchange:

I do not at all intend to question any standard notions of logic, such as
the first-order language or the Peano axioms. Note that my worries about
the Peano axioms did not arise from my own position, but from an extreme
case that I devised to understand yours. My own conclusion from this
extreme case would be that your use of standard and non-standard numbers
is not suitable to analyse the question at hand.

It is probably fair if I commit to something positive and sketch my view
on consistency: I think that there are several possible approaches, but in
the end I would probably settle for the one described by Timothy Chow [FOM
post from Fri Mar 29 12:15:05]: Mathematical experience suggests that any
finitistic proof of a statement about finite and certain infinite objects
(natural numbers, syntax, finite graphs, computable sets ...) can be
mimicked by a formal PA-proof of the natural formalization of this
statement (without any domain conditions). As Tim points out, if we accept
this claim and Gödel's theorem, then we must accept that the consistency
of PA cannot be proved by finitary means (whatever our view on
non-standard numbers).

To conclude I would like to comment on your examples of reals vs. complex
numbers and integers vs. natural numbers. I do not find these examples
convincing, because I do not think that the situation is analogous to
standard vs. non-standard. In any suitable mathematical context there will
be a well-determined set of reals and a well-determined set of complex
numbers. But there is no set of non-standard numbers – the notion of
non-standard number does only make sense with respect to a specific model.
Similarly, there is no set of standard numbers. There is just a set of
natural numbers (and, of course, a set of integers, of reals, of complex
numbers ...). I think that this difference to the case of reals vs.
complex numbers is important.

I would also like to thank you for the discussion!

Best,
Anton

_______________________________________________
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=T42O_zYeHhF26klEBwP2aQHxDQiCn2Xykej04tQe3CE&s=K8xq3v6HDGqecoBo67hbgqYBciCap4_7u6RRASU2G-w&e=