[FOM] First-order arithmetical truth

[Timothy Y. Chow]

Francis Davey wrote:

>However, it is not true to say that Godel's theorems (in context I 
>assume his two incompleteness theorems) are "about the intended 
>structure". The first incompleteness theorem is first described as a way 
>of showing that certain statements of PM are formally undecidable. In 
>other words they can be understood without any reference to a model of 
>PM (or PA).

You misunderstand Arnon Avron's point.  Goedel's theorems are about formal 
systems.  But what is a formal system?  How can I tell the "intended" 
formal systems (the ones that deal with proofs of "finite" length, in a 
certain "intended" sense of the word "finite") from the unintended formal 
systems whose proofs are "finite" only in an "unintended" sense of the 
word "finite"?

If you lack the ability to distinguish the intended model of PA from 
another model, it would seem that you also lack the ability to distinguish 
the intended meaning of the term "formal system" from some other meaning.

Tim