[FOM] Godel and PA

[Lawrence Paulson]

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20170304/1e92c03b/attachment-0001.html>