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

Christian Retoré 1 2
1 TEXTE - Exploration et exploitation de données textuelles
LIRMM - Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier
Résumé : 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.
Type de document :
Rapport
[Research Report] LIRMM; LABRI. 2016
Liste complète des métadonnées

https://hal-lirmm.ccsd.cnrs.fr/lirmm-01281243
Contributeur : Christian Retoré <>
Soumis le : mardi 1 mars 2016 - 19:01:01
Dernière modification le : mercredi 7 novembre 2018 - 14:00:03

Lien texte intégral

Identifiants

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

Citation

Christian Retoré, . Classical logic and intuitionistic logic: equivalent formulations in natural deduction, Gödel-Kolmogorov-Glivenko translation. [Research Report] LIRMM; LABRI. 2016. 〈lirmm-01281243〉

Partager

Métriques

Consultations de la notice

141