[FOM] Axiomatic Syntax

[Arnon Avron]

Here is my first, superficial reaction to Friedman's Posting. I say in advance
that I need time to think about it, so maybe some questions and points
I raised are total nonsense.

> 1. Show that under any two reasonable codings of the syntax of PA, the
> consistency statements are provably equivalent within PA.
> 
> 2. Show that under any two reasonable codings of the syntax of PA, the self
> referential constructions due to Godel yield statements provably equivalent
> within PA.
> 
> Now 2 follows from 1, since the Hilbert Bernays and Jerosolow work directly
> show that the self referential constructions in question, with respect to
> any particular reasonable codings of syntax, give the consistency statement
> with respect to that coding. So we have only to worry about 1.

Definitely, as far as simlple equivalence goes. I should warn however
again that when it comes to a debate concerning the *content* of a 
sentence (like: whether a given sentence is self-referential) such 
equivalence is only
a necessary condition. After all, all theorems of PA are equivalent
in PA. Does this means that they all have the same content?

  But this was only a side remark. The subject treated here
is much more important than the debate that starts this excehange of postings.
 
> The strategy in giving an appropriate set of conditions is to first, at the
> conceptual level, identify the syntax of PA with an obvious many sorted
> relational structure, in a finite relational type. The sorts correspond to
> the relevant syntactic categories, the functions correspond to the basic
> syntactic operations, and the relations correspond to the basic syntactic
> relations. 
> 
> It is important that this structure be presented in a certain way. It must
> be INDUCTIVELY PRESENTED. I do not have the time to describe, in general,
> what this means. I would bet that an appropriate notion of this kind is
> already in the literature. But in any case, it will be obvious that the
> structure we are interested in, which is to be identified with the syntax of
> PA, is in fact inductively presented. NOTE: I don't quite see that the well
> known notion of finitely presented is quite enough for this.

Although certainly sound in the right direction, this is still
a little vague. What is the "*obvious*  many sorted relational structure
(is there only one?), what is the "certain way" that this
structure should be presented? Especially the last remark
(with which I tend to agree) indicates that we might not still 
have a satisfactory solution!

> In any case, the natural presentation of our structure is in fact an
> inductive presentation.
> 
> It will be clear that our particular inductively presented structure
> satisfies the obvious PRINCIPLE(S) OF INDUCTION - with respect to all
> predicates. This is a second order condition, and MUCH TOO CRUDE for our
> purposes. The principle of induction should be clear for any inductively
> defined structure. 

I would say more. To my opinion (I might have said it already before)
First-order language is too weak for the task, while second-order is
far too strong. I believe that the correct framework is an extension
of First-order logic with a transitive closure operation for which
induction is a built-in *logical* rule (formulated a la Gentzen)  
and in which (like in Feferman's FS_0) one can form ordered pairs.
I have started to do some (very initial) work in this direction
in my paper "Transitive Closure and the mechanization of Mathematics"
(in "Thirty Five Years of Automating Mathematics", edited
by F. Kamareddine, pp. 149-171, Kluwer Academic Publishers, 2003).
 
> We can turn the inductive presentation of our structure into finitely many
> BASIC UNIVERSAL SENTENCES true in the structure. These universal sentences
> are very special - they correspond to an inductive presentation.
> 
> However, we can define what we mean by an ARITHMETIC INTERPRETATION of our
> structure (or any inductively presented structure). The domains, relations,
> and functions are all given by arithmetic formulas, and the structure must
> obey those finitely many basic universal sentences.

Dont you need to redefine here the concept of an arithmetic formula
so it will make sense for any inductively presented structure (independent
of any coding)?

> 
> It now makes sense to impose the PRINCIPLE OF ARITHMETIC INDUCTION on the
> arithmetic interpretations. This is the principle of induction stated only
> for all arithmetic formulas.
> 
> *FACT 2* Any two arithmetic interpretations of our structure that satisfy
> these basic universal sentences AND THE PRINCIPLE OF ARITHMETIC INDUCTION
> are ARITHMETICALLY ISOMORPHIC.

I am a little bit confused. I apologize. What does "ARITHMETICALLY ISOMORPHIC"
exactly mean?
 
> *FACT 3* There exists an arithmetic interpretation of our structure that
> provably in PA satisfies the basic universal sentences AND THE PRINCIPLE OF

I am even more confused now. In what sense is it "provably in PA"?
Is (as I suspect) a natural coding is needed to make this statement
meaningful?  And if so - are we not back to the question: what 
is a natural coding?

> So we define an adequate arithmetization of syntax simply as an
> arithmetically presented structure such that in PA, we can prove that the
> basic universal sentences and the principle of arithmetic induction hold.

I am not sure that I completely understand this definition at the moment.
Does it suply a constructive criterion for adequate arithmetization?
And might it not be too broad? For example: is the compostion of one
adequate encoding with a p.r. function which is (provably in PA)
1-1 and onto also adequate according to this definition? (note that
if this is the case then for *every* \phi and n we can find an
adequate encoding such that the code of \phi(n) is exactly n!)
 
> There is a form of the self reference lemma that makes the self referential
> nature of this business as clear as I have ever seen it made in print. I saw
> this first in Jerosolow.
> 
> SELF REFERENCE LEMMA. Let phi(x) be a formula of PA with only the free
> variable x. There exists a closed term t such that the godel number of the
> sentence phi(t) IS the correct value of t.
> 
> It is compelling to say that:
> 
> The sentence phi(t) asserts that the property phi holds of the sentence
> itself. 

I dont find it compelling at all, and for two reasons. One is more
or less that noted already by Heck: the fact that you can use
arbitrary (or even not so arbitrary) p.r. functions to construct such
a sentence is hardly surprising, and it only means that the value
of $t$ and the number which is the code of  phi(t) are the same -
but this equality of the term with the number  is itself a
content-ful proposition (in which most ingredients of the 
"self-reference" have been built!). Hence the phi(t)
cannot be said to assert a property of itself. The second reason
that this lemma is again code-dependent. Change the code, and the 
same sentence is not asserting anything about itself anymore,
but another one does. The two might be equivalent in PA, but
self-reference is not a property that is preserved by equivalence in PA
(well, to my opinion it is not a property that a sentence of PA
can possibly have, so I am talking myself on a rather semi-intuitive,
vague level).

Why I am so insisting about the last point, that is not technically
significant? I'll try to explain this in a different posting.

Arnon Avron