[FOM] (no subject)

[Artemov, Sergei]

Small things.

> I don't know what you're trying to say with your 
> allusion to cargo cults, but the assertion I just made, that in the 
> statement of G2, Con(PA) is just a string that does not have to be 
> assigned a meaning, is about as uncontroversial a statement as one 
> gets in this subject.

On the contrary, logic normally considers two sides of formulas,  syntactic and semantic. One a textbook in logic: shortly after defining terms and formulas, it introduces the notions of interpretation and truth values. When you speak about provability, immediately after some kind of soundness and, when possible, completeness results are provides. In a theory with an outstanding natural semantics, such as PA, a standard model provides the intended semantics of the language^ a logical equivalent of mathematical notion of truth for arithmetical formulas. Furthermore, if a theory is incomplete, like PA, truth and provability do not coincide and their interplay is a big deal. In particular, provability in PA is completely characterized as truth in all models of PA, most of which are nonstandard. So the syntax and semantics in arithmetic are normally considered together. 

In particular, when we write Con(PA) which IS a string of symbols, then immediately the corresponding semantic questions pop up: is the formula mathematically true? is this formula provable? The former is true in then standard model, the latter is true in all modals of PA, including nonstandard models. Model analysis is necessary when we decide whether or not Con(PA) is a fair arithmetical presentation of Hilbert’s consistency, etc. The question itself is about semantics, so we need to look at the models. This explains my joke about cargo cult: in this kind of questions, considering a formula as a syntactic object only, without analyzing its behavior in models of PA, does not make much sense.   

> in the clause "Con(PA) is not derivable in 
> PA," the word "derivable" refers to real PA-derivations.  By any normal 
> standards of English usage, G2 is therefore "about" real PA-derivations.

Absolutely. I was talking not about G2 but about Con(PA) = \forall x(~Proof(x,0=1). In the context of provability in PA, this formula should necessarily be considered in arbitrary PA-models, including nonstandard. In a nonstandard model M, \forall x ranges over both standard and nonstandard numbers.