[FOM] Advanced systems programming and the consistency of PA^{2}

[Peter Apostoli]

Dear FOM,

A propos the thread on interpreting the object language of a formal system in the metatheory (as, e.g., in systems programming), readers of FOM may find the advanced systems programming in 

The analytic conception of truth and the foundations of arithmetic. 
The Journal of Symbolic Logic, 65 (1) 33-102 (2000)


of some interest.

More importantly, the paper purports to prove the consistency of Peano's second order postulates for the arithmetic of the natural numbers by a semantic version of a cut elimination proof, one that uses inductively constructed partial truth predicates in the style of Paul Gilmore and Saul Kripke. However, the construction uses mathematical induction only up to the first uncountable ordinal (the same as the ordinal of Gentzen's cut elimination proof for first order PA). This seems in direct conflict with the claim one finds in the Folklore that the cut elimination proof for second order PA *requires* immensely large ordinals. Thus the possibility arises that the extreme complexity of existing cut elimination consistency proofs for second order PA arises from details (artifacts) of Gentzens format and syntactic nature of the cut elimination proof, and not from any intrinsic property of the consistency problem for PA itself.

My question is, can anyone find a mistake in the cited paper, or explain the apparent conflict some other way?

BTW: No references to Goedel (the first systems programmer) should be required to treat this problem.

Best Wishes

Peter A.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/fom/attachments/20030615/c37a8f8f/attachment.html