Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation - LIRMM - Laboratoire d’Informatique, de Robotique et de Microélectronique de Montpellier Access content directly
Reports (Research Report) Year : 2016

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

Abstract

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.

Domains

Logic [math.LO]

Dates and versions

lirmm-01281243 , version 1 (01-03-2016)

Identifiers

Cite

Richard Moot, Christian Retoré. Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation. [Research Report] LIRMM; LABRI. 2016. ⟨lirmm-01281243⟩
197 View
0 Download

Altmetric

Share

Gmail Facebook X LinkedIn More