Exposé de Jan von Plato The exact correspondence between intuitionistic and modal logic

The exact correspondence between intuitionistic and modal logic

Gödel, working within axiomatic logic, succeeded in 1933 in establishing a translation from theorems of intuitionistic propositional logic to ones in classical logic enriched with a modal provability operator. He managed to define a converse correspondence in 1941, one that began with a construtivization 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 used states that indirect proof is not needed in derivations of translations of intuitionistic formulas. It turns out, in particular, that the classical nature of Gödel's modal logic of provability plays no role at all, which fact undermines the whole idea of interpreting intuitionistic logic within the classical one, as a kind of "provability fragment" within it.