[FOM] First-order arithmetical truth

[mario]

Tim,

On Mon, 2006-10-16 at 18:16 -0400, Timothy Y. Chow wrote: 
> Francis Davey wrote:
... 
> 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 [1] you lack the ability to distinguish the intended model of PA from 
> another model, it would seem that [3] you also lack the ability to distinguish 
> the intended meaning of the term "formal system" from some other meaning.

1. Do you argue for [1]->[3] above along the following (one line longer)
sketch:

if    (1) somebody lacks the ability to distinguish the intended model
of PA from another model,
then  (2) (s)he lacks the ability to distinguish the intended model of
meta-PM from another model, 
then  (3) (s)he lacks the ability to distinguish the intended meaning of
the term "formal system" from some other meaning.

Say meta-PM is any theory which is sufficient to axiomatize
metamathematical results about Principia Mathematica and/or ZFC. 

2. How do you argue for (2)->(3)?

thanks 
mario