FOM: Intuitionism (Tait)

[Axiomize@aol.com]

Subj:FOM: Intuitionism (Tait) 
Date:6/10/02 7:51:05 AM Eastern Daylight Time
From:krupski at lpcs.math.msu.ru
Reply-to:kru at voll.math.msu.su
To:fom at math.psu.edu
CC:Dean.Buckner at btopenworld.com
Sent from the Internet (Details)

RE: FOM: Intuitionism (Tait)

> "What would prove "P is provable" other than a proof of P".

(The proof of P) + (the proof that this proof is correct and really proves P)

Vladimir Krupski

 - - -

Since every recursively enumerable predicate has a wff that is provable just 
when the predicate is true (Proposition 3.23, p. 131, Elliott Mendelson, 
1964, Introduction to Mathematical Logic, Van Nostrand, New York), and 
provability is recursively enumerable,  then I would expect as much 
(provability of P representing both the predicate and the wff, here.)

Charlie Volkstorf,
Senior Analyst
M-Tools
Cambridge, MA