Explicit Provability and Constructive Semantics

Abstract In 1933 Gödel introduced a calculus of provability (also known as modal logicS4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logicLPof propositions and proofs and show that Gödel's provability calculus is nothing but the forgetful projection ofLP. This also achieves Gödel's objective of defining intuitionistic propositional logicIntvia classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics forIntwhich resisted formalization since the early 1930s.LPmay be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus.