FOM: Intuitionism (Tait)
Vladimir N. Krupski
krupski at lpcs.math.msu.ru
Sun Jun 9 09:15:16 EDT 2002
RE: FOM: Intuitionism (Tait)
> William Tait gives a neat argument (23 May 2002) that the proposition that p
> is the same as the proposition that it is provable that p.
> "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)
When we will suppose that this one coincides with the proof of P, i.e.
(The proof of P) = (The proof of P) + (the proof that this proof is correct and
really proves P)+...,
then the notion of proof will be too complex. In particular, the predicate "x is
a proof" seems to
be undecidable in this case. If we agree with this undecidability then
else will be OK.
Department of Mathematical Logic and Theory of Algorithms
Moscow State University, Russia
e-mail: krupski at lpcs.math.msu.ru (office)
kru at voll.math.msu.su (home)
More information about the FOM