FOM: Intuitionism (Tait)

[Vladimir N.Krupski]

> 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,

Thank you, you are right.
Now I see that the corresponding proof predicate can be
constructed via Fixed Point Theorem for arithmetic. But some
question remains open for me. This construction involves diagonalization
and is too complex for practical implementation as a proof checking
program (i.e. the program which computes the proof predicate Prf(x,y) ).
The value of Prf(n,F) depends on the choice of a formula  which
represents _this_ Prf in arithmetic. 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)).
May be it is impossible in some sense but I fail to formalize this feeling.

Vladimir N. Krupski
Associate Professor
Department of Mathematical Logic and Theory of Algorithms
Moscow State University, Russia.

homepage: http://lpcs.math.msu.ru/~krupski/
e-mail: krupski at lpcs.math.msu.ru  (office)
        kru at voll.math.msu.su      (home)