The intended meaning of intuitionistic logic is given by the Brouwer- Heyting-Kolmogorov (BHK) semantics which informally defines intuitionistic truth as provability and specifies the intuitionistic connectives via operations on proofs. The natural problem of formalizing the BHK semantics and establishing the completeness of propositional intuitionistic logic Int with respect to this semantics remained open until recently. This question turned out to be a part of the more general problem of the intended semantics for Godel's modal logic of provability S4 with the atoms 'F is provable' which was open since 1933. In this paper we present complete solutions to both of these problems. We find the logic of explicit provability (LP) with the atoms 't is a proof of F' and establish that every theorem of S4 admits a reading in LP as the statement about explicit provability. This provides the adequate provability semantics for S4 along the lines of a suggestion made by Godel in 1938. The explicit provability reading of Godel's embedding of Znt into S4 gives the desired formalization of the BHK semantics: Int is shown to be complete with respect to this semantics. In addition, LP has revealed the relationship between proofs and types, and subsumes the lambda-calculus, modal lambda-calculus and combinatory logic.
展开▼
