Explicit provability and constructive semantics (Q2732527)

Gödel introduced a calculus of provability, which is the modal logic known as S4 now, and left open its exact intended semantics. As is also well known, Solovay established afterwards that arithmetical provability is formalized as a modality by another modal logic which is usually called GL. This gap is filled in this paper by a logic, called LP, of propositions and proofs, in which, by making use of the newly introduced notion of proof constants, explicit provability is formalized as ``(a proof constant) \(c\) is a (code of) proof of (a formula)'' not as the usual ``there exists some (code of) proof of (a formula)''. The author proves not only the completeness of LP with respect to the standard arithmetical provability interpretation but also that LP is considered as a realization of the modal logic S4 in the sense, in short, that the S4 modality formalizes the meta-level existence of some proof constant \(c\) such that ``\(c\) is a (code of) proof of (a formula)''. Thus the provability interpretation of S4 modality is established through explicit provability. Moreover, according to the well-known correspondence between the modal logic S4 and intuitionistic logic this provability interpretation of S4 achieves Gödel's objective of defining intuitionistic propositional logic via classical proofs, and provides a Brouwer-Heyting-Kolmogorov style provability semantics for intuitionistic logic. The author also remarks that the logic LP may be regarded as a unified underlying structure for intuitionistic logic, modal logics, typed combinatory logic, and lambda-calculus.