On Proof Realization of Intuitionistic Logic
Sergei Nikolaevich Artemov · 1997
Abstract : In 1933 Godel Introduced an axiomatic system, currently known as S4, for a logic of an absolute provability. The problem of finding a fair probability model for S4 was left open. In the current paper we demonstrate how the Intuitionistic propositional logic Int can be directly realized by proof polynomials. It is shown that Int is complete with respect to this proof realizability.