[FOM] Godel and PA

[Joe Shipman]

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.

For an interesting alternative development, I recommend very strongly Manin's GTM text, which does all the major results up through Matijasevich's in a very different order with very different dependencies.

-- JS

Sent from my iPhone

> On Mar 4, 2017, at 8:51 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> This may be a good time for another plug for "Finite sets and Gödel's incompleteness theorems" by S. Świerczkowski. He he fixes on the hereditarily finite sets (rather than natural numbers) as the foundation and presents a clear and reasonably formal development, with rather few gaps. His preference for basing the formalisation on Sigma-formulas eliminates the need for the upper bounds that started this thread. The penalty for this convenience is that certain parts of the argument will have to be formalised explicitly in the embedded calculus, but most readers will be prepared to take that for granted. He also simplifies the condition of omega-consistency to just consistency (an aspect of the argument that I never really grasped).
> 
> As with Gödel's work on constructible sets, subsequent presentations are often very clear, and going to Gödel’s original publications only make sense on historical grounds and to read his often insightful comments on his aims for the work.
> 
> https://eudml.org/doc/285944
> 
> Larry Paulson
> 
> 
>> On 3 Mar 2017, at 17:40, Richard Heck <richard_heck at brown.edu> wrote:
>> 
>>> On 03/02/2017 06:34 PM, Martin Davis wrote:
>>> Godel 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.
>> 
>> Just to be completely precise: In the system Gödel calls P, the axioms he assumes at type 1 are just the successor axioms and induction (as a single axiom). I.e., he does not include axioms for addition and multiplication. Indeed, + and × are not primitives but are treated as defined, presumably via the Dedekind-Frege method. (The same goes for equality.) What this means is that the proof Gödel actually gives does make real use of the type structure.
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20170304/6f170009/attachment.html>