FOM: Intuitionism (Tait)

[Vladimir N. Krupski]

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)