[FOM] Attack/defense on Godel

[Andrew Boucher]

Harvey Friedman wrote:

> Here I want to give my thoughts on what I take to be an interesting 
> attack on the Godel theorems, and how it can be repelled.
>
> I think that the attack is much more interesting against Godel's 
> second incompleteness theorem than against the first.
>
> It is said that Godel's second theorem tells us that, for instance, PA 
> does not prove that PA is consistent.
>
> We can state this with some care about just what it takes to prove it, 
> as follows.
>
> *If PA is consistent then PA does not prove that PA is consistent. 
> Furthermore, this is proved within a very weak fragment of PA.*
>
> The attack goes like this.
>
> #Godel shows that some particular formal sentence A that is clearly 
> related to the assertion that PA is consistent, is not provable in PA.
>
> However, this particular formal sentence A should not (automatically) 
> be identified with the actual assertion that PA is consistent. In 
> particular, it involves rather complicated arithmetic definitions, and 
> is certainly not any kind of direct translation of the assertion that 
> PA is consistent.#
>
> How does one defend against this attack? It seems to me to be closely 
> related to what Floyd must be talking about??
>
> I think it is best to move to adjust the formal systems under 
> discussion in order to get around such an attack.
>
> *****************************
>
> I claim that Godel's 2nd incompleteness theorem, in proper generality, 
> shows the following.
>
> A FAITHFUL FORMALIZATION OF FINITE MATHEMATICS HAS BEEN GIVEN THAT IS 
> GENERALLY ACCEPTED AS BEING INCLUSIVE. THIS FORMALIZATION INCLUDES A 
> FAITHFUL FORMALIZATION, B, OF THE ASSERTION THAT ZFC IS CONSISTENT. 
> HOWEVER, B CANNOT BE PROVED IN THIS FAITHFUL FORMALIZATION. 
> FURTHERMORE, THIS FACT IS ESTABLISHED WITHIN FINITE MATHEMATICS 
> TOGETHER WITH THE ASSUMPTION THAT THE FAITHFUL FORMALIZATION OF 
> MATHEMATICS IS CONSISTENT. IN ADDITION, ZFC CAN BE REPLACED BY THE 
> FAITHFUL FORMALIZATION OF FINITE MATHEMATICS.
>
> The faithful formalization of finite mathematics that is at least 
> inclusive, that I have in mind, is the system T, whose language has 
> epsilon,=,N,0,S, and whose axioms areas follows. Here N is the unary 
> relation for "x is a natural number". Also S is the binary relation 
> for "x,y are natural numbers and y is the successor of x".
>
> 1. If x,y are not natural numbers and have the same elements, then 
> they are equal.
>
> 2. Pairing.
>
> 3. Union.
>
> 4. Power set.
>
> 5. Foundation for arbitrary formulas.
>
> 6. Separation for arbitrary formulas.
>
> 7. Replacement.
>
> 8. Choice.
>
> 9. Every nonempty set has an epsilon maximal element (i.e., every set 
> is finite).
>
> 9. Successor axioms for N,0,S.
>
> 10. Induction scheme on N using N,0,S, but arbitrary formulas.
>
> This system T really does faithfully mirror how a mathematician would 
> carefully and fully rigorously discuss the syntax of ZFC, and also of 
> T. In particular, it avoids any kind of Godel numbering. One literally 
> talks about finite sequences of letters. Finite sequences are defined 
> as functions with domain an initial segment of the natural numbers, etc.

Am I missing something, or is Choice really necesary to be part of T?

Of course "faithful" may be in the eyes of the beholder, but can't PA2 
(second-order arithmetic) serve to provide a faithful rendition?  That 
is, second-order arithmetic has access to big-letters, and one can use 
them, instead of coded numbers, to define sequences:  
    Seq(R,n) abbreviates (R is 1-1 onto with domain [1,n]).
This would seem to be "faithful", or at least as faithful as a rendition 
in T. One can then define predicates Wff and Proof, again in an 
apparently faithful way (without recourse to coding), and go on to 
prove, in PA2, that  formal system X cannot prove the "real" consistency 
of formal system X (where X is ZFC, PA1, or PA2).  

I think what becomes interesting is when you consider fragments of PA2. 
 The fragment of PA2 which I call F (second-order arithmetic without the 
assumption of Ad Infinitum) *can* define Seq(R,n) and render faithful 
(at least in the eye of this beholder) renditions of Seq(R,n), WffInX, 
SentenceInX, and ProofInX (where X is some formal system).  

F + "10 exists" can then prove the First Incompleteness Theorem, i.e. 
for X = PA, PA2, or ZFC,
    (there exists G)(SentenceInX(G)
    & (ConsOfX => (R) ! ProofInX(R,G) & (R) ! ProofInX(R,"!G")).

Here ! means "not".

In fact, the proof goes through as suggested in my last posting.  There 
are two cases. If Ad Infinitum, then follow Godel's Proof, and set G = 
the Godel-Rosser sentence.  And if not Ad Infinitum, then there exists a 
maximum number >= 10.  Then consider a proposition P consisting of as 
many conjuncts "! 0 = 0" as possible, i.e. where P and !P exist, but not 
"P & 0 = 0" (this not existing because its length is longer than the 
maximum number).    There can, obviously, be no proof of P or !P, 
because any purported proof needs to be more than one line and thus 
would be too big to exist.  

Why "10 exists"?  Well you need at least one conjunct of "0 = 0", and 
there are 10 symbols in "! (0 = 0 & 0 = 0)".    Maybe a sharper bound is 
possible!

I'm not sure if F + "n exists" (for a number n of one's choosing) is 
sufficient to prove the Second Incompleteness Theorem, however.