[FOM] Axiomatic Syntax

[Harvey Friedman]

Reply to Franzen.

On 9/2/03 3:25 AM, "Torkel Franzen" <torkel at sm.luth.se> wrote:

> 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.
> 

Put slightly differently, how do we formalize the idea that:

the Godel beta function lemma is provable in PA based on 0,S,+,x?

There is a way to do this. We can define what we mean by "an adequate
formalization of finite sequences" within PA. Then we can show that under
any adequate formalization of finite sequences, the Godel beta function
formulated with respect to it, is provable in PA.

I am not sure how my point affects the Heck/Franzen interchange.

***************************************

Concerning the correct point that it may sometimes be subtle to formalize
the idea that a given mathematical assertion is provable in a given formal
system: 

The issue does not seem to arise for systems such as ZFC that are intended
to reflect the whole of mathematical practice. One can make a very well
accepted definitional extension of ZFC which is good enough for
uncontroversial direct formalization of 'all' mathematical statements.

I don't think that this has ever been done really neatly, as there are some
subtleties involved. I am truly shocked as to how cumbersome and ugly the
stuff is out there. Nevertheless, it can be done very nicely.

If we restrict to finite mathematics, then we can do this with weak
fragments of ZFC that omit the axiom of infinity.

Harvey Friedman