FOM: Intuitionism (Tait)

[Axiomize@aol.com]

Subj:RE: FOM: Intuitionism (Tait) 
Date:6/14/02 10:01:39 AM Eastern Daylight Time
From:kru at voll.math.msu.su
To:fom at math.psu.edu
Sent from the Internet (Details)

>> Since (Proposition 3.23, p. 131, Elliott Mendelson, 1964, Introduction to 
Mathematical Logic, Van Nostrand, New York),  then I would expect as much.
>> Charlie Volkstorf

> Thank you.  Now I see that the corresponding proof predicate can be 
constructed via Fixed Point Theorem but I don't see any direct ("suitable for 
programming") construction of a decidable (\Delta_{1}-formula) proof 
predicate with the property Prf(n,F)->Prf(n,Prf(n,F)).
> Vladimir N. Krupski

Must the proof of P be the same as the proof that this proof proves P?  As a 
proof proves only one sentence (if we defined it to include corollaries, then 
Prf would no longer be recursive, but only recursively enumerable), then F 
would have to coincide with Prf(n,F).

Would a recursive f such that Prf(n,F)->Prf(f(n),Prf(n,F)) be helpful?  
(Shall we make the implication two-way?)  Or perhaps combine them into 
Prf(n,F^Prf(n,F))? 

Charlie Volkstorf
M-Tools
Cambridge, MA