Mathematical Logic Tradition
According to Brouwer, truth in constructive (intuitionistic) mathematics means the existence of a proof, cf. Troelstra and van Dalen (1988). In 1931-34, Heyt- ing and Kolmogorov gave an informal description of the intended proof-based semantics for intuitionistic logic (Kolmogoroff, 1932; Heyting, 1934), which is now referred to as the Brouwer-Heyting-Kolmogorov (BHK) semantics.
According to the BHK conditions, a formula is “true” if it hasa proof. Furthermore, a proof of a compound statement is connected to proofs of its components in the following way:
This provides a remarkably useful informal way of understanding what is and what is not intuitionistically acceptable. For instance, consider the classical
Kolmogorov explicitly suggested that the proof-like objects in his interpretation (“problem solutions”) came from classical mathematics (Kolmogoroff, 1932). Indeed, from a foundational point of view this reflects Kolmogorov’s and Godel’s goal to define intuitionism within classical mathematics. From this standpoint, intuitionistic mathematics is not a substitute for classical mathematics, but helps to determine what is constructive in the latter.
The fundamental value of the BHK semantics for the justification logic project is that informally but unambiguously BHK suggests treating justifications, here mathematical proofs, as objects with operations.
In Gddel (1933), Gddel took the first step toward developing a rigorous proof-based semantics for intuitionism. Gddel considered the classical modal logic S4 to be a calculus describing properties of provability:
(1) Axioms and rules of classical propositional logic,
(2) ?(F → G) → (?F → ?G),
(3) ?F → F,
(4) ?F → ??F,
Based on Brouwer’s understanding of logical truth as provability, Godel defined a translation tr(F) of the propositional formula F in the intuitionistic language into the language of classical modal logic: tr(F) is obtained by prefixing every subformula of F with the provability modality ?.
Informally speaking, when the usual procedure of determining classical truth of a formula is applied to tr(F), it will test the provability (not the truth) of each of F’s subformulas, in agreement with Brouwer’s ideas. From Godel’s results and the McKinsey- Tarski work on topological semantics for modal logic (McKinsey and Tarski, 1948), it follows that the translation tr(F) provides a proper embedding of the Intuitionistic Propositional Calculus, IPC, into S4, i.e., an embedding of intu- itionistic logic into classical logic extended by the provability operator.
)
Conceptually, this defines IPC in S4.
Still, Godel’s original goal of defining intuitionistic logic in terms of classical provability was not reached because the connection of S4 to the usual mathematical notion of provability was not established. Moreover, Gddel noted that the straightforward idea of interpreting modality ?F as F is provable in a given formal system T contradicted his second incompleteness theorem. Indeed, ?(?F → F) can be derived in S4 by the rule of necessitation from the axiom ?F → F. On the other hand, interpreting modality ? as the predicate of formal provability in theory T and F as contradiction converts this formula into a false statement that the consistency of T is internally provable in T.
The situation after Godel (1933) can be described by the following figure where “X c→ Y” should be read as “X is interpreted in Y”:
IPC → S4 → ? → CLASSICALPROOFS.
In a public lecture in Vienna in 1938, Gddel observed that using the format of explicit proofs
t is a proof of F (1.4)
can help in interpreting his provability calculus S4 (Godel, 1938). Unfortunately, Godel (1938) remained unpublished until 1995, by which time the
Gcidelian logic of explicit proofs had already been rediscovered, axiomatized as the Logic of Proofs LP, and supplied with completeness theorems connecting it to both S4 and classical proofs (Artemov, 1995, 2001).
The Logic of Proofs LP became the first in the justification logic family. Proof terms in LP are nothing but BHK terms understood as classical proofs. With LP, propositional intuitionistic logic received the desired rigorous BHK semantics:
IPC → S4 → LP → classicalproofs.
Several well-known mathematical notions that appeared prior to justification logic have sometimes been perceived as related to the BHK idea: Kleene realizability (Troelstra, 1998), Curry-Howard isomorphism (Girard et al., 1989; Troelstra and Schwichtenberg, 1996), Kreisel-Goodman theory of constructions (Goodman, 1970; Kreisel, 1962, 1965), just to name a few. These interpretations have been very instrumental for understanding intuitionistic logic, though none of them qualifies as the BHK semantics.
Kleene realizability revealed a fundamental computational content of formal intuitionistic derivations; however it is still quite different from the intended BHK semantics. Kleene realizers are computational programs rather than proofs. The predicate “r realizes F” is not decidable, which leads to some serious deviations from intuitionistic logic. Kleene realizability is not adequate for the intuitionistic propositional calculus IPC. There are realizable propositional formulas not derivable in IPC (Rose, 1953).[3]
The Curry-Howard isomorphism transliterates natural derivations in IPC to typed !-terms, thus providing a generic functional reading for logical derivations. However, the foundational value of this interpretation is limited because, as proof objects, Curry-Howard !-terms denote nothing but derivations in IPC itself and thus yield a circular provability semantics for the latter.
An attempt to formalize the BHK semantics directly was made by Kreisel in his theory of constructions (Kreisel, 1962, 1965). The original variant of the theory was inconsistent; difficulties already occurred at the propositional level. In Goodman (1970) this was fixed by introducing a stratification of constructions into levels, which ruined the BHK character of this semantics. In particular, a proof of A → B was no longer a construction that could be applied to any proof of A.
1.3