[FOM] Godel's Theorems

[Harvey Friedman]

Reply to Murphy  5/3/03  9:03AM
Reply to Boucher  5/4/03  7:12AM

>
>>  Again,would they give up the English translation of the second
>>  incompleteness theorem for PA?
>
>I am hardly the gold standard of interpretation, either for LW or the
>authors.  However, since the second theorem depends on the first and the
>first depends on the construction of sentence for which they would argue we
>have no legitimate English translation, then I don't think they would have
>to accept the second theorem as stated in English.

The issue of English translation of "PA is consistent", or "T is 
consistent" for the system T that I prefer to work with, in no way 
depends on the issue of English translation of "this sentence is not 
provable in PA" or "this sentence is not provable in PM". There is no 
self reference issue in "PA is consistent" or "T is consistent" 
(except perhaps the subtle matter I addressed concerning how one 
chooses to talk in PA or T about the choice of "letters" for PA or T).

>
>>  But why isn't the link between Ordinary Language and formal languages
>>  and systems such as the language of PA and the system PA, already
>>  solid enough to justify such "leaps"?
>
>The problem is with the "definitions and transformations" that get you from
>the natural language to the formal system and back.

What's the problem, especially if we use a faithful foundation like 
the one I proposed in my previous posting, or in my posting that is 
just about to go out entitled in response to Heck on "Real Numbers"? 
I set such systems up particuarly to address this issue, and I think 
it is addressed satisfactorily.

>With paraphrase, in
>other words (I think this is the point Putnam and Floyd are making in the
>last part of the paper).  For example, I have several introductory logic
>texts that claim that paraphrase is "more an art then a science".

Not a problem

>What does
>this imply? What is  the relationship between a natural language sentence
>and the various paraphrases it goes through before it "becomes" something in
>the formal system.

This is very solid in the situation at hand.

>I would think and argue that it is not entailment.

It is not formal entailment, since the translation starts with 
something that is pre-formal.

>  And
>if it is not--if there is no rule constrained means of going from one to the
>other-- then is the relationship magical?  A typical semantic theory might
>take a natural language sentence, give it a surface syntactic structure, and
>then a deep syntactic structure, before assigning a final interpreted
>logical form.  Does each transformation require a certain amount of voodoo?
>If so, why get led down this garden path?

No voodoo.

The essential question is: where does the burden of proof lie? To me, 
it is obvious that it first lies on people on my side to give a more 
honest foundations - which is, given present experience, pretty easy 
to do. Then the burden of proof lies on those who want to complain. I 
don't think that the complainers have said much yet.

Boucher:

Harvey Friedman wrote:

>...
>
>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.

Boucher:


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

Friedman:

I never said it was necessary. In fact, it is derivable, but very 
convenient.It is derivable because of the finitude axiom, axiom 9.

Boucher:

Of course "faithful" may be in the eyes of the beholder, but can't 
PA2 (second-order arithmetic) serve to provide a faithful rendition?

Friedman:

Axioms 1-10 are for supporting the conduct of FINITE mathematics. 
Witness the axiom of finitude, axiom 9. PA_2 goes way beyond finite 
mathematics, in any sense of the word. Read what I have in capitals.

Of course, you are trying to support a much stronger claim that what 
I have made in capitals, but I set my weaker claim up in order to 
make the philosophical importance more obvious and also in order to 
make the claim more difficult to attack on philosophical grounds.