[FOM] Axiomatic Syntax
Harvey Friedman
friedman at math.ohio-state.edu
Mon Sep 1 18:49:34 EDT 2003
Reply to Heck.
On 9/1/03 4:08 PM, "Richard Heck" <heck at fas.harvard.edu> wrote:
Friedman wrote:
>>
>> 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.
>>
Heck wrote:
> How compelling it is to say this will depend a little bit upon one's
> purposes. I'll say a further word about this matter shortly.
Friedman wrote:
>
>> This Lemma works for PA formulated with primitive recursive function symbols.
>>
Heck wrote:
> It is worth emphasizing this point: The lemma mentioned works /only/ for
> a version of PA that has some additional function symbols for primitive
> recursive functions.
It might be interesting to investigate just what function symbols are needed
for this self reference lemma. In particular, I have never seen proofs that
various natural collections of functions are insufficient for this. Of
course, formulating this investigation in a robust way is a challenge, since
it is dependent on Godel numberings - the very issue that is the main point
of my posting on Axiomatic Syntax.
As a related warmup investigation of independent interest, one could try to
prove that there is no arithmetization of syntax that is given by "natural
mathematical functions". I.e., numerical functions of the kind that come up
in mathematics.
>
Heck suggests that in the Self Reference lemma above, the self reference is
not entirely DIRECT self reference, as the sentence phi(t) is not referred
to by t explicitly, but rather implicitly.
I would put it this way: In order to have direct self reference, one would
want, e.g., a nonnegative integer n such that
the Godel number of phi(n*) is n
where n* is the term 1+1+1+...+1, n times. Or perhaps some other standard
canonical name for n such as its base 10 representation. The latter would be
supported by having base 10 exponentiation available as a primitive in PA.
Now obviously we are not going to be able to find n such that
the Godel number of phi(n*) is n
under any natural Godel numbering, because under any natural Godel
numbering, the Godel number of a sentence is always at least as large as the
number of symbols.
However, presumably one can prove the following result: (I don't have the
time now to think about it right now).
THEOREM(?) There is no natural Godel numbering such that the following is
true. Let phi(x) be a formula of PA with only the free variable x. Then
there exists n such that the Godel number of phi(n*) is n, where n* is the
base 10 representation of n.
Heck brings up a well known example of Russell involving the poet Scott and
"author of Waverly". Russell makes a distinction between
1. the author of Waverly.
2. Sir Walter Scott.
In modern mathematical logic terms, one considers 1 to be a denoting term.
One considers 2 to be not only a denoting term, but a denoting term in
NORMAL FORM.
The idea is that DIRECT self reference can only be accomplished through the
use of terms in NORMAL FORM. Thus in the self reference lemma quoted above,
one is using denoting terms, but not a term in NORMAL FORM. The THEOREM(?)
suggests that one cannot use terms in the usual NORMAL FORMS.
Before going on further, let me emphasize this.
WARNING. All of these issues surrounding "honest self reference", etc., are
COMPLETELY IRRELEVANT for Godel's theorems. This stuff is ONLY USED AS
LEMMAS in order to facilitate the proof of Godel's theorems.
NEVERTHELESS. It is of intrinsic interest.
Heck now makes a perceptive DISANALOGY between the Russell case and the
above self reference lemma. Namely, although the closed term t is not in
normal form, it is much closer to being in normal form than is "the author
of Waverly". One can cast this relative "closeness" in terms of necessity or
a preexisting algorithm for conversion to normal form or provable equality
with the normal form, etcetera, which one does not prima facie have at all
in the case of "the author of Waverly".
Heck suggests the problem "what is one to make of this disanalogy?"
Of course, one thing to make of this disanalogy is to upgrade the status of
the above self reference lemma as some sort of legitimate self reference.
In any case, a research project suggested by these considerations is to
introduce DIRECT SELF REFERENCE into PA.
I have discussed this already on the FOM with the use of nested quote signs.
However, I sensed a difficulty with this. In fact, even if one wants to
simply be allowed to refer to any particular sentence in the language,
without any direct self reference, but with only direct reference, one has
to be careful about ambiguities.
Computer science oriented people came into the discussion to say that all of
this has been done perfectly well by programming methodology people. My
instincts were to question that this was done in a way that philosophers
would accept. I never went into this in detail.
Certainly the Kripke stuff is normally couched simply in terms of Godel
numberings and does not seek to do self reference directly.
Harvey Friedman
More information about the FOM
mailing list