[FOM] Axiomatic Syntax

[Torkel Franzen]

Richard Heck says:

 >So similarly, one might well want also to say that phi(diag(*phi(x)*)) 
 >does not /refer/ to itself at all. It does not really say of itself that 
 >it has phi. Rather, it says that there is an object, namely, the one and 
 >only one sentence that diagonalizes phi(x), that has phi. That object 
 >happens to be the very sentence phi(diag(*phi(x)*)), but that fact is no 
 >part of what that sentence /says/. Formally, we may think of the numeral 
 >for its goedel number as a sentence's /name/. So, from this point of 
 >view, only a sentence of the form phi(n), for n a numeral, could really 
 >say of itself that it had phi.

  Such considerations are not specifically tied to self-referential
sentences, but apply equally to intensional locutions in general. We
might want to say that a formalization in PA of the fundamental
theorem of arithmetic does not /say/ that every natural number has a
unique prime decomposition at all (since it must use some coding of
finite sequences of natural numbers as natural numbers). Rather, it
formulates an arithmetical statement which is provably equivalent to a
formalization of the fundamental theorem of arithmetic in an extension
by definitions of PA, where that proof is of an elementary and uniform
kind.

The general pattern when we talk of a formalization A* in a formal
theory T (such as PA or ZF or ACA_0) of a statement A ("This sentence
is unprovable in T", "Every natural number has a unique prime
decomposition", Ramsey's theorem, the fundamental theorem of calculus,
etc) seems to be that A* is the translation into primitive notation of
a statement A' in an extension by definitions (or perhaps: a
conservative extension) T' of T, such that A' can be proved equivalent
to a "direct" formalization of A in T' using only the principles of
some general translation scheme.

A special case is when the general translation scheme is based on some
mathematical theorem A, which can then presumably not be faithfully
expressed using that same translation scheme. Suppose we handle finite
sequences in PA through Gödel's beta-lemma: for every finite sequence
<a1,..,am> of natural numbers, there are numbers k and m such that
beta(k,m,i)=ai for every i<=m. If we now translate the beta-lemma
itself using a representation of sequences as numbers derived from the
beta-lemma, we get essentially the statement that for all k and m
there are k' and m' such that beta(k',m',i)=beta(k,m,i+1) for
i<beta(k,m,0), which does not convey the same information as the
beta-lemma, although for every choice of n, the beta-lemma restricted
to sequences of length n can be faithfully expressed.

---
Torkel Franzen