[FOM] Axiomatic Syntax

[Harvey Friedman]

Reply to Avron.

On 8/28/03 5:12 AM, "Arnon Avron" <aa at tau.ac.il> wrote:

> I did not try to be creative here. On the contrary. I kept asking, and
> more than once, for references  to relevant works (and got none so far).

> Again, in my messages I wrote at least twice that I am sure that such
> conditions exist, and ask for references. I could certainly find some
> myself, but why reinventing the wheel and devote time and energy
> to  things that are well-known? One of the benefits I expect
> from something like FOM is getting  this kind of information.
> So this might be the end of this particular story if you tell me
> (and perhaps some other few people in the list who might also not know)
> what are these well-known conditions (it should not take more than
> 10-15 lines, I believe) and/or provide appropriate references!
> 

Normally I would have replied the same day you asked about this, but I have
been finishing the first BRT paper, a very time consuming and intensive
task. 

I was expecting your queries to have been answered a long time ago by other
FOM subscribers, but it appears that this is not going to happen.

In the interest of time, I will only consider the case of PA = Peano
Arithmetic, where less care is needed than for weak fragments.

There are two issues.

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.

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.

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. 

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.

*FACT 1* Any two structures satisfying these basic universal sentences, that
are FINITELY GENERATED from their constants, are isomorphic.

If the general notion of inductively presented structure is set up right,
then the associated universal sentences should be pulled from the
presentation in a canonical way, and FACT 1 will always hold.

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.

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.

So far, we have been model theoretic and recursion theoretic. We now have to
be proof theoretic.

*FACT 3* There exists an arithmetic interpretation of our structure that
provably in PA satisfies the basic universal sentences AND THE PRINCIPLE OF
ARITHMETIC INDUCTION. Let I,J be two arithmetic interpretations of our
structure that provably in PA satisfy the basic universal sentences AND THE
PRINCIPLE OF ARITHMEITC INDUCTION. Then an arithmetically defined
isomorphism between I and J can be exhibited and verified provably within
PA. As an immediately consequence, the CONSISTENCY STATEMENTS relative to I
and J are provably equivalent within PA.

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.

The theorem is that the consistency statements with respect to any two
adequate arithmetizations of syntax are provably equivalent in PA.

I was going to present the structure associated with syntax in full detail,
together with the associated basic universal sentences, but I realized that
this will not (?) be necessary for the interested parties, who can figure
this out on their own. There are some nonobvious points, however, and no
doubt it can be done badly. So I will stop the discussion of axiomatic
syntax here.  

> As to the main issue of the discussion. I repeat that according to
> the definition of a Godel sentence you gave in your previous posting
> (and I certainly take you as an authority on the subject)
> Con_T is a Godel sentence for T - and it certainly does not
> "speak about itself". End of this story!?
> 
> 
>

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. 

This Lemma works for PA formulated with primitive recursive function
symbols. 

Harvey Friedman