[FOM] Godel and PA

[Martin Davis]

Joe Shipman wrote:

"I have always wondered why Godel didn't first prove his theorems for PA
with Exponentiation, or even for Exponential Function Arithmetic, and then
show that Exponentiation was representable."

This is an apparently common misconception. Godel's proved his theorems not
for PA, but for a system with a countable  infinity of types and atomic
formulas of the form a(b)  where a is one type higher than b. Peano
postulates were assumed for the bottom type. And he did prove, as a
separate result, that all primitive recursive relations are arithmetic.

Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20170302/16b846e0/attachment.html>