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
everything
else will be OK.
Vladimir Krupski
Associate Professor
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
mailing list