Skip to Main content Skip to Navigation
Reports

Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation

Richard Moot 1 Christian Retoré 2
2 TEXTE - Exploration et exploitation de données textuelles
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
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.
Document type :
Reports
Complete list of metadata

https://hal-lirmm.ccsd.cnrs.fr/lirmm-01281243
Contributor : Christian Retoré <>
Submitted on : Tuesday, March 1, 2016 - 7:01:01 PM
Last modification on : Friday, June 4, 2021 - 12:32:02 PM

Links full text

Identifiers

  • HAL Id : lirmm-01281243, version 1
  • ARXIV : 1602.07608

Citation

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⟩

Share

Metrics

Record views

254