[FOM] Godel and PA

[Joe Shipman]

I'm aware of that, I was making a more mundane technical point, which is that it's much easier to get to the core results and separate the philosophy from the details by using exponentiation, and concentrate all the technical  difficulty in the "representing exponentiation" part which is an interesting stand-alone result anyway.

-- JS

Sent from my iPhone

> On Mar 2, 2017, at 6:34 PM, Martin Davis <martin at eipye.com> wrote:
> 
> 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                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                               
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom