The exact correspondence between intuitionistic and modal logic
Jan Von Plato
University of Helsinki
Abstract:
Gödel, working within axiomatic logic, succeeded in 1933 in establishing a translation from theorems of intuitionistic propositional logic to ones of classical logic enriched with a modal provability operator. He managed to define a converse correspondence in 1941, one that began with a constructivization of classically proved theorems. Here a thoroughly elementary approach is presented, by which formal derivations in each of the two systems are related to each other by direct syntactic translations. The Main Lemma gives proof transformations by which indirect proof is eliminated in derivations of translations of intuitionistic formulas. It is for this conservativity of classical over intuitionistic logic for translated formulas that Gödel's modal translation succeeds in singling out an intuitionistic ''provability fragment'' within the classical modal calculus that coincides with intuitionistic logic.