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



How to reconcile Godel's theorem with the completeness of the Predicate Calculus?
A model of arithmetic in which the G"odel sentence "I am unprovable" is false is necessarily a non-standard model. It contains an infinite element which satisfies, in the model, the formula expressing the property of being a proof of the G"odel sentence --- a formula that is not satisfied by any standard natural number (not even in a non-standard model).


