[FOM] Godel and PA

[Richard Heck]

On 03/04/2017 12:41 PM, Joe Shipman wrote:
> This was the point of my original query. There is a very easy
> isomorphism between the theory of HF and the theory of Peano
> arithmetic where exponentiation is a built in function whose totality
> is assumed. If you only have addition and multiplication in your
> language there is much more technical work to do which only obscures
> the metamathematical issues.  The representability of exponentiation
> in terms of addition and multiplication ought to be treated as a
> separate (and interesting and important) result but not as an
> essential component of "Godel's Incompleteness Theorems": even though
> historically Godel also proved this result it should be seen as a
> different piece of math.

This sort of approach is taken in the most recent editions of Boolos,
Burgess, and Jeffrey's /Computability and Logic/: The incompleteness
theorem is proved first for Q plus the recursion equations for
exponentiation, and then it is shown how to eliminate the latter. This
allows one to use the coding of sequences via prime factorization, which
makes things much simpler.

That said, I would suggest that there is another serious cost to using
hereditariy finite set theory or some extension of PA, namely, the one
that motivates BB&J's use of a certain extension of Q. (It's a nice
question, to which I do not know the answer, whether one could instead
use an extension of R to include exponentiation.) That raises, the
question, for me, whether the sort of approach Świerczkowski uses really
requires such strong resources. The axiomatization of hereditarily
finite set theory he uses is: empty set, adjunction and an induction
scheme. Dropping the latter leaves adjunctive set theory, which is
mutually interpretable with Q and, like Q, finitely axiomatized. Much of
the "easy coding" Świerczkowski mentions will still be possible there.

Richard Heck

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20170304/234593e9/attachment.html>