Formalization of Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic
by
Sergei Artemov
Moscow University and Cornell University

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 intuitionistic logic Int with respect to this semantics remained open since the early 1930s. This question was known to be a part of the more general problem of finding the intended provability semantics for Goedel's modal logic S4 (was open since 1933). We present complete solutions to both of these problems. We found the logic of explicit provability (LP) with the atoms "t is a proof of F"

and establish the completeness of LP with respect to the intended provability interpretation. We establish that S4 is nothing but the forgetful projection of LP, and thus every theorem of S4 (therefore, every theorem of Int) can be regarded as a specific statement about proofs built according to the requirements of the BHK semantics. This semantics, unlike Kleene realizability, turned out to be adequate for Int. The complete text of the paper can be found by http://www.cs.cornell.edu/Info/People/artemov/publ/html Technical report CFIS98-10 `Explicit provability:the intended semantics for intuitionistic and modal logic'.

Explicit provability:the intended semantics for intuitionistic and modal logic

Date received: February 17, 1999