[FOM] Only one proof

[Aatu Koskensilta]

Quoting John Baldwin <jbaldwin at uic.edu>:

> On Mon, 31 Aug 2009, Aatu Koskensilta wrote:
>
>> Another example: Gödel's proof for the first incompleteness theorem
>> understood as the result that the set of Pi-1 truths is productive.
>> I'm not aware of any way of proving this result without going through
>> essentially the recursion theoretic contortions found in the original
>> proof. (I may well be just ignorant.)
>
> I am not sure of how `understood as productive' affects the  
> observation that via Paris-Harrington, the first incompleteness  
> theorem can be proved without coding syntax.  This sure qualifies as  
> a different proof.

A different proof, to be sure. But how do you propose to squeeze out  
of Paris-Harrington the productivity of the set of Pi-1 truths?  
Charles Silver mentions also Kripke's model theoretic proof (of Pi-2  
incompleteness). This proof too doesn't yield in any obvious way the  
productivity of the set of Pi-1 truths -- which, arguably, is the  
recursion theoretic core of the first incompleteness theorem.

-- 
Aatu Koskensilta (aatu.koskensilta at uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen"
  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus