[FOM] Attack/defense on Godel

[Harvey Friedman]

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.

One small difficulty is the concept of "letter". There are two 
approaches. One is to simply give an adhoc assignment for the 
finitely many letters used for the alphabet of ZFC and T. This is 
fully defensible, since mathematicians do this kind of thing all the 
time when trying to be very precise about technical material. The 
other approach is to consider the letters to be any distinct 
entities, and take the consistency statement to assert that it holds 
for any choice of entities for letters. Also one proves that if it 
holds for some choice of entities for letters, it holds for all 
choices of entities for letters.