Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation
Logique classique et intuitionniste: formulations équivalentes en déduction naturelle, traduction de Gödel-Kolmogorov-Glivenko
Résumé
This report first shows the equivalence bewteen several formulations of classical logic in intuitionistic logic (tertium non datur, reductio ad absurdum, Pierce's law). Then it establishes the correctness of the G\"odel-Kolmogorov translation, whose restriction to the propositional case is due to Glivenko. This translation maps a formula F of first order logic to a formula F¬¬ in such a way that F is provable in classical logic if and only if F¬¬ is provable in intuitionistic logic. All formal proofs are presented in natural deduction. These questions are well-known proof theoretical facts, but in textbooks, they are often ignored or left to the reader. Because of the combinatorial difficulty of some of the needed formal proofs, we hope that this report may be useful, in particular to students and colleagues from other areas.
Ce rapport commence par établir l’équivalence entre diverses formulation de la lo- gique classique (tiers exclu, raisonnement par l’absurde, loi de Pierce) en logique intui- tionniste. Nous montrons ensuite la correction de la traduction de Gödel-Kolmogorov, dont la restriction au cas propositionnel est due à Glivenko. Cette traduction associe à toute formule F de la logique du premier ordre une formule F¬¬ telle que F est démontrable en logique classique si et seulement si F¬¬ est démontrable en logique intuitionniste. Toutes les preuves formelles sont présentées en déduction naturelle.
Ces résultats de théorie de la démonstration sont bien connus, mais dans les ou- vrages où ils sont mentionnés, leurs démonstrations sont souvent laissées en exercice au lecteur. Vue la difficulté combinatoire de certains des cas de ces démonstrations, nous pensons que ce rapport pourra être utile aux étudiants et aux collègues d’autres domaines.