Summer 1993

We use formal semantic analysis to generate intuitive confidence that the Heyting Calculus is an appropriate system of deduction for constructive reasoning. Well-known modal semantic formalisms have been defined by Kripke and Beth, but these have no formal concepts corresponding to constructions, and shed little intuitive light on the meanings of formulae. In particular, the well-known completeness proofs for these semantics do not generate confidence in the sufficiency of the Heyting Calculus, since we have no reason to believe that every intuitively constructive truth is valid in the formal semantics.

Läuchli has proved completeness for a realizability semantics with formal concepts analogous to constructions, but the analogy is inherently inexact. We argue that, in spite of this inexactness, every intuitively constructive truth is valid in Läuchli's semantics, and therefore the Heyting Calculus is powerful enough to prove all constructive truths. Our argument is based on the postulate that a uniformly constructible object must be communicable in spite of imprecision in our language, and we show how the permutations in Läuchli's semantics represent conceivable imprecision in a language, independently of the particular structure of the language.

We look at some of the details of a generalization of Läuchli's proof of completeness for the propositional part of the Heyting Calculus, in order to expose the required model constructions and the constructive content of the result. We discuss the reasons why Läuchli's completeness results on the predicte calculus are not constructive. A pleasing side-effect is a simpler version of tableaux proof procedures in the style of Beth and Fitting.