[FOM] First-order arithmetical truth

[John McCarthy]

Francis Davey includes


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

Yes, and surely it is Godel's greatest fault to have got his
ideas from a distinction between provability and truth.  It's a
pity that Godel wasn't scooped by someone with a more appropriate 
attitude.