[FOM] Fwd: Forward: Provability of Consistency

Tue Mar 26 11:57:12 EDT 2019

---------- Forwarded message ---------
From: Kennedy, Juliette <juliette.kennedy at helsinki.fi>
Date: Mon, Mar 25, 2019 at 11:21 PM
Subject: Re: [FOM] Forward: Provability of Consistency
To: Foundations of Mathematics <fom at cs.nyu.edu>, Martin Davis <
martin at eipye.com>

The old question whether the Second Incompleteness theorem has been
established or not has been discussed by Feferman, Detlefsen, Franks,
Pudlak and others, mostly centering on the three Hilbert-Bernays
derivability conditions as given in Hilbert and Bernays 1934.

There is also the Kuratowski proof:

Set theory cannot prove that set theory is consistent in the strong sense
that some *V*α is a model of set theory. For suppose it does. Then there is
α such that *V*α is a model of set theory. Hence there is also in *V*α some
β<α such that *V*βis a model of set theory. Continuing in this way we get
an infinite descending sequence of ordinals, a contradiction.

See Kripke 2009. See also
https://plato.stanford.edu/entries/goedel/incompleteness-hilbert.html

All the best,

Juliette

Department of Mathematics and Statistics
P.O. Box 68 (Gustaf Hällströmin katu 2b)
FI-00014 University of Helsinki, Finland
tel. (+358-9)-191-51446, fax (+358-9)-191-51400
mobile: +358-50-371-4576

www.math.helsinki.fi/logic/people/juliette.kennedy/
------------------------------
*From:* fom-bounces at cs.nyu.edu <fom-bounces at cs.nyu.edu> on behalf of
Artemov, Sergei <SArtemov at gc.cuny.edu>
*Sent:* Monday, March 25, 2019 3:27:41 PM
*To:* Foundations of Mathematics
*Subject:* Re: [FOM] Forward: Provability of Consistency

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

_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
https://cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20190326/0233a325/attachment-0001.html>