[FOM] Forward: Provability of Consistency

[Artemov, Sergei]

Dear Tim,

Thank you for reiterating the traditional views of the subject, which makes it easier to show what is wrong with them. The logic of the paper is more refined than you suggest.  

TC <You say in your paper that Con(PA) "states consistency of both standard 
and nonstandard proof codes."  This makes no sense.  Con(PA) is a formal 
string and does not state anything.>

Well, we don’t want to be a version of the Cargo Cult (worshipping life-size replicas of airplanes out of straw) and to believe in formal strings without any connection to their meaning and function. So, a formal string, e.g., Con(PA), has exact semantics, which we should know and take into account. There are at least three relevant levels of understanding of an arithmetical formula F: 

1. “Naive” mathematical reading F as a mathematical statement about natural numbers.

2. Semantics in the standard model of arithmetic. This is actually a glorified version of (1) for logicians. 

3. Provability in PA. This one is quite relevant in the context of Goedel’s Second Incompleteness Theorem, G2. 

Con(PA) is an adequate formalization of consistency of PA in the standard model (2), and, perhaps, that is why “general” mathematicians have been willing to accept Con(PA) as in (1). No problems here. 

However, our goal is to make a semantic sense out of (3), to understand what is really going on in G2. By Goedel’s Completeness Theorem, a formula F is derivable in PA iff F holds in all PA-models, most of them nonstandard. Each non-standard model has an initial segment consisting of standard numbers 0,1,2,… followed by an infinite amount of so-called nonstandard numbers, abstract elements of the model, which do not correspond to any numerals n. 

The proof of G2 states that Con(PA) is not derivable in PA which, semantically, is equivalent to existing of a model M of PA in which Con(PA) fails. So, there is an element \alpha in M for which Proof(\alpha, 0=1) is true. It is easy to observe that \alpha cannot be from the standard initial segment (there are many ways to show that ~Proof(n,0=1) for any standard n, pick the one you like). The conclusion: Con(PA) indeed fails in some models of PA (hence is not PA-provable), but ONLY on nonstandard elements which do not correspond to real derivations in PA. This sketch of the semantic analysis of G2 shows that G2 is not about real PA-derivations, each of which is in fact not a proof of 0=1. 

The traditional connection of G2 to consistency of real PA-proofs is actually a sophisticated logical error. Here is a simple example to explain this logical error to a mathematician. Suppose you want to check whether the following (true) statement is formally provable: R = “no x is a real root of x^2+1.” We pick a rich relevant theory of complex numbers C and note that R is not provable in C by the following reasoning: take an evaluation x=i and get x^2+1=0. Conclusion: R is true but not provable. A simple mistake here was to accept a fake witness for x^2+1=0, which is not a real number. The same reasoning error occurs in interpreting G2 as an impossibility of real PA-proofs of consistency: we tacitly accept a fake witness \alpha for Proof(x,0=1), the one which does not correspond to a real PA-derivation. I repeat, there is nothing wrong with G2, but its “impossibility” reading for real PA-derivations is plain erroneous.  

Actually, this is one (out of several) arguments showing that Con(PA) in the context of provability does not serve as an adequate formalization of the fact that no real PA-derivation is a proof 0=1. In the simple situation 1-2, this does not show, but in a more challenging environment of (3), Con(PA) fails on some nonstandard elements and this  prevents provability of Con(PA) in PA. Apparently, G2 leaves open the question of whether we can establish by finitary means that real PA-derivations do not contain 0=1. 

A logician would say that the problem is with the limited expressive power of the first-order language of PA which does not actually distinguish standard and nonstandard elements of the model. This feature alone is responsible for unprovability of Con(PA) which by its “for all x” quantifier necessarily spans over both standard and nonstandard numbers. 

As a logician, I have always loved Con(PA), but facing these arguments I have to admit that Con(PA) is not an adequate formalization of real consistency in the context of provability in PA. We have to explore alternative ways to look for finitary consistency proofs (no matter how painful this might appear to myself, the logic community in general, interpreters and commentators on consistency matters, etc.). 

Since the internalized universal quantifier “for all x” in Con(PA) is the principal suspect, we have to try other legitimate logical ways to formalize consistency, and such a format easily suggests itself: a scheme of consistency. Informally, consistency may be regarded as a mathematical claim depending on a parameter S ranging over PA-derivations

4. S does not contain 0=1. 

To prove consistency is a legitimate combinatorial math problem about finite strings of formulas of PA. There are no codes here and nothing actually requiring arithmetization. However, to compare it back-to-back with Con(PA) we shape it flawlessly as an arithmetical scheme with the natural parameter n over codes of proofs

5. ConS(PA) = ~Proof(n,0=1). 

Schemes in arithmetic have long been first class citizens: induction scheme, weak induction schemes, reflection schemes, sigma-completeness, truth definitions, etc. I suggest regarding (5) under the same angle: as a legitimate object in the proof theory of PA. Nobody questions finitary character of the induction scheme in PA, the same holds for ConS(PA). 

There are several arguments in favor of adopting (5) as a possible arithmetical form of consistency. 

6. Con(PA) and ConS(PA) are equivalent over the standard model of arithmetic, hence for a “general” mathematician (a scheme is true iff all its formulas are true). 

7. Since Con(PA)/G2 analysis of Hilbert’s finitary consistency program turned out to be problematic, we don’t have a choice other than opting for ConS(PA), FOR HILBERT”S FINITARY CONSISTENCY POOFS PROGRAM. 

This does not deny a paramount importance of Con(PA) and G2. They are jewels of mathematics, indispensable for proof theoretical analysis, comparing theories, studying interpretability, complexity, and zillions of other matters, a real asset for logic. There is one thing they don’t do though: representing consistency of real PA-proofs in PA, and we have to use the scheme ConS(PA) instead. 

Now let me comment on your other question. 

TC <(*) Any finitistic proof that PA is consistent can be mimicked by a 
	formal proof of Con(PA) from the axioms of PA.>

This is a simplistic reading of the formalization of finitary proofs principle since it does not cover a mathematically acceptable situation when consistency of each real PA-derivation S is proven constructively by finitary means, but the proofs substantially depend on S and do not convert into one uniform proof that fits all S’s. 

Again, to make a point, consider the arithmetical induction principle Ind, which is a scheme, not a formula. One cannot deny that induction is finitary provable, it is just one of the basic tools of combinatorial reasoning. However, its formalization in PA is possible only step-by-step: each instance of Ind is mimicked by a formal proof in PA, namely by this instance itself. Since PA is not finitely axiomatizable, there is no one PA-proof of the whole Ind. 

Consistency is the case similar to induction: it is finitary provable but its provability is not mimicked by a single formal proof in PA. 

Furthermore, if we understand (*) exclusively for Con(PA) as a formula, then we have to admit that Hilbert’s question about finitary consistency proof for PA is equivalent to the question about consistency proof for PA in a finite fragment of PA which is a priori unrealistic. So, my take on (*) is more refined: yes, but we have to accommodate finitary provable schemes and case-by-case formalizations of their proofs in PA. 

So, I suggest studying the scheme ConS(PA) as a legitimate form of consistency, equivalent to Con(PA) in the standard model (i.e., for a “general” mathematician). This quite legitimate (and, so far, the only unproblematic) arithmetization of consistency for the purposes of Hilbert’s program yields an answer to Hilbert’s consistency question, and this answer is: consistency of PA is mathematically provable by finitary means. 

In the future rounds of discussion, please, be specific about elements of this construction you don’t trust. A naked “I am not convinced” is not convincing. 

Sergei