FOM: Intuitionism (Tait)

[Vladimir N.Krupski]

Sorry, there was a misprint in the fixed poin equation from my
previous posting. The definition of a recursive proof predicate
which satisied the Tait's condition should be:
 Prf(n,F) <->
 "n is a Godel number of a (standard) proof of some
 formula G and G is the shortest formula for which
 F = Prf(n,Prf(n, ... Prf(n,G)...))".

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)