Intermediate logics and factors of the Medvedev lattice

In this paper we shall prove theorems about some systems of sentential calculus, by making use of results we have established elsewhere regarding closure algebras and Brouwerian albegras. We shall be concerned mostly with the Lewis system and the Heyting system. Some of the results here are new (in particular, Theorems 2.4, 3.1, 3.9, 3.10, 4.5, and 4.6); others have been stated without proof in the literature (in particular, Theorems 2.1, 2.2, 4.4, 5.2, and 5.3). Show more

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