In Mendelson's Introduction to Mathematical Logic, the proof of Godel's Theorem for S (his axiomatic arithmetic) goes via proving that a sentence that can be interpreted as "This statement has no proof in S" cannot be proved either false or true in S, if S is consistent.
According to the completeness of the Predicate Calculus, any logically valid wf of a theory K is a theorem of K. The statement I interpret as "This statement has no proof in S" cannot be proved either false or true, so I presume that there are models of arithmetic (or rather of axiom system S) in which it is false, and models in which it is true. Is this correct?
A model of arithmetic in which it is true seems sane enough. Are there models of S in which a proof of what is interpreted as "This statement has no proof in S" turns up as some sort of non-standard number, or have I got completely confused? I have a vision in my mind of a non-standard number encoding "1 is not a proof of S. 2 is not a proof of S. 3 is not a proof of S...." or in some other way satisfying the equation that asserts that X is a proof of Y, if not the mathematician posing the equation :-)
