🔢 mathematics

Classical Logic as Intuitionistic Logic with Duality

Cet article propose une nouvelle sémantique de la preuve pour la logique classique qui étend la logique intuitionniste en opérant sur des littéraux duaux primitifs plutôt que sur des propositions atomiques, démontrant ainsi que la logique classique peut être comprise comme une logique intuitionniste complétée par un principe de dualité encodé de manière inférentielle.

Auteurs originaux : Alexander V. Gheorghiu, Yll Buzoku

Publié 2026-06-03

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Alexander V. Gheorghiu, Yll Buzoku

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

L'idée centrale : La logique comme un jeu de « Oui » et de « Non »

Imaginez que vous essayez d'expliquer le fonctionnement de la logique à un ami. Habituellement, nous pensons que la logique est un ensemble de règles pour déterminer ce qui est Vrai et ce qui est Faux.

Cet article propose une autre façon de voir les choses. Au lieu de demander « Est-ce que cette affirmation est vraie ? », les auteurs demandent : « Puis-je l'affirmer ? » (dire « Oui ») ou « Puis-je la nier ? » (dire « Non »).

Leur slogan principal est :

Logique Classique = Logique Intuitionniste + Dualité

En français courant : ils disent que la logique « classique » complexe que nous utilisons en mathématiques et en sciences est en fait simplement la logique « intuitionniste » plus simple (qui est très stricte sur la preuve) plus une règle spéciale qui traite le « Oui » et le « Non » comme deux forces égales et opposées dès le départ.

Les personnages de l'histoire

Pour comprendre leur argument, nous devons rencontrer les trois personnages principaux de leur récit :

Le Contenu (le « Quoi ») : C'est l'idée brute, comme « Le concert est bien ».
La Force (le « Comment ») : C'est la manière dont vous délivrez l'idée. Vous pouvez l'Affirmer (dire « Le concert est bien ! ») ou la Nier (dire « Le concert est mauvais ! »).
La Formule (la « Structure ») : C'est la phrase complexe construite à partir de ces idées, comme « Si le concert est bien, alors je resterai ».

L'ancienne méthode vs La nouvelle méthode

L'ancienne méthode (Logique traditionnelle) :
Imaginez que vous avez un interrupteur. Il est soit ON (Vrai), soit OFF (Faux).

Si vous voulez dire « Non », il vous suffit de basculer l'interrupteur sur OFF.
Dans cette vision, « Nier » quelque chose revient simplement à « Affirmer son contraire ».
Le Problème : Les auteurs disent que c'est trop simple. Cela suppose que nous savons déjà que la réponse est soit oui, soit non avant même de commencer à argumenter. C'est comme supposer que l'interrupteur fonctionne déjà avant même de l'avoir branché.

La nouvelle méthode (L'approche des auteurs) :
Imaginez une conversation entre deux personnes, un « Adepte du Oui » et un « Adepte du Non ».

Ils ne commencent pas avec un interrupteur. Ils commencent avec des Littéraux.
Un Littéral est un acte de parole de base.
- Littéral Positif : « J'affirme : Le concert est bien. »
- Littéral Négatif : « Je nie : Le concert est bien » (ce qui revient à dire « Le concert est mauvais »).
Point crucial : Ces deux éléments ne sont pas définis l'un par rapport à l'autre. On ne dit pas « La négation est juste l'opposé de l'affirmation ». Ce sont deux outils distincts et primitifs, comme un marteau et un tournevis. Vous ne pouvez pas transformer un marteau en tournevis simplement en le retournant ; ils sont fondamentalement différents.

Le secret de la « Dualité »

L'article soutient que pour passer de la logique simple (Intuitionniste) à la logique complexe (Classique), il suffit d'ajouter une règle sur la façon dont ces outils de « Oui » et de « Non » interagissent au niveau le plus bas (le niveau atomique).

Ils introduisent deux règles simples pour ces outils de base :

La règle d'« Exclusion » : On ne peut pas dire « Oui » et « Non » à la même chose exactement au même moment. Si vous essayez d'affirmer « Le concert est bien » ET de nier « Le concert est bien », vous faites planter le système (vous obtenez une contradiction, ou « absurdité »).
La règle de l'« Analyse de cas » : Si vous pouvez prouver un résultat que vous supposiez « Oui » OU que vous supposiez « Non », alors vous n'avez pas besoin de savoir lequel est vrai pour obtenir le résultat. Vous pouvez simplement dire : « C'est prouvé dans les deux cas ».

L'analogie :
Imaginez que vous essayez d'entrer dans un club.

Logique Intuitionniste : Vous avez besoin d'une invitation spécifique (une preuve) pour entrer. Si vous ne l'avez pas, vous ne pouvez pas entrer.
Logique Classique (avec Dualité) : Vous pouvez entrer si vous avez un laissez-passer « Oui » OU si vous avez un laissez-passer « Non » (qui agit comme un laissez-passer « Non, je ne reste pas dehors »).
Les auteurs montrent que si vous avez ces deux laissez-passer (Affirmation et Négation) et les deux règles ci-dessus, vous pouvez construire toute la structure de la Logique Classique sans jamais avoir besoin de supposer l'existence préalable d'un univers « Vrai/Faux ».

Pourquoi est-ce important (Le « Pourquoi devrais-je m'en soucier ? »)

Les auteurs résolvent un puzzle philosophique.

Le Puzzle : Comment pouvons-nous utiliser la Logique Classique (qui suppose que tout est soit Vrai, soit Faux) si nous sommes des « Anti-réalistes » (des personnes qui croient que la vérité est quelque chose que nous construisons par la preuve, et non quelque chose qui flotte dans le ciel) ?
La Solution : En traitant le « Oui » et le « Non » comme deux actes de parole égaux et primitifs, ils montrent que la Logique Classique n'a pas besoin de supposer qu'un monde « Vrai/Faux » existe au préalable. Elle a seulement besoin des règles de la façon dont nous argumentons avec le « Oui » et le « Non ».

La réussite technique

L'article réalise quelque chose de très habile mathématiquement :

Ils prennent les règles standards et simples de la Logique Intuitionniste (qui sont déjà bien comprises).
Ils ajoutent les règles de « Dualité » (Exclusion et Analyse de cas) uniquement au niveau le plus bas (les littéraux).
Ils prouvent que cet ajout simple crée le système complet et puissant de la Logique Classique.

Ils appellent cela la Sémantique d'extension de base (Base-Extension Semantics). Pensez à la construction d'une maison :

La Logique Intuitionniste est la fondation et la charpente.
La Logique Classique est la même maison, mais avec une « Porte Duale » spéciale installée tout en bas.
Une fois cette porte installée, toute la maison fonctionne différemment, permettant tout le raisonnement complexe que nous utilisons en mathématiques classiques, mais elle a été construite en utilisant uniquement les briques constructives simples de la logique intuitionniste.

Résumé

L'article affirme que : La Logique Classique n'est pas une vérité mystérieuse et préexistante. C'est simplement la Logique Intuitionniste (une logique basée sur la preuve) plus un accord simple sur le fait que le « Oui » et le « Non » sont deux forces égales et opposées que nous pouvons utiliser pour construire des arguments complexes.

En traitant la « Négation » comme un outil primitif plutôt que comme simplement « l'affirmation du contraire », ils offrent une nouvelle façon constructive de comprendre comment le raisonnement classique fonctionne sans avoir besoin de croire en un univers magique « Vrai/Faux ».

Résumé Technique : La Logique Classique comme Logique Intuitionniste avec Dualité

1. Le Problème
L'article traite d'un défi fondamental de la théorie de la signification : fournir une sémantique de type preuve-théorique (P-tS) pour la logique classique qui adhère aux principes anti-réalistes (constructivistes) sans présupposer le principe de bivalence ou de vérité de vérification-transcendante. Bien que Sandqvist ait développé avec succès une sémantique d'extension de base (B-eS) pour la logique intuitionniste (IPL) et une version pour la logique classique (CPL), des limites subsistent. La sémantique CPL de Sandqvist est restreinte à des connecteurs spécifiques (initialement $\to, \bot, \forall$ ) et repose sur une preuve de complétude techniquement complexe impliquant l'induction sur les barres. De plus, les approches existantes peinent souvent à traiter le langage propositionnel complet (incluant $\lor$ et $\exists$ ) de manière constructive. Les auteurs visent à résoudre cela en proposant une B-eS pour la logique propositionnelle classique complète qui maintient une preuve de complétude élémentaire et constructive, répondant ainsi au défi de Dummett concernant la réconciliation de l'inférence classique avec le sens anti-réaliste.

2. Méthodologie et Cadre Philosophique
Les auteurs proposent un cadre bilatéraliste où la logique classique est conceptualisée comme « Logique Intuitionniste + Dualité ». Cette approche s'écarte des vues traditionnelles en distinguant le contenu de la force illocutoire au niveau atomique, tout en traitant les formules complexes comme des structures logico-grammaticales plutôt que comme des propositions portant elles-mêmes une force.

Les Littéraux comme Propositions : Le système introduit des « littéraux » ( $L$ ) comme les seuls objets d'assertion et de négation. Un contenu $c$ est apparié à une force pour former un littéral positif ( $c^+$ , assertion) ou un littéral négatif ( $c^-$ , négation/dénégation). Crucialement, la dualité est primitive : $c^+$ et $c^-$ sont des actes de parole atomiques indépendants, non définis via la négation ( $\neg$ ).
Structures Logico-Grammaticales : Les formules complexes (par exemple, $\phi \land \psi$ ) ne sont pas des propositions à affirmer ou à nier, mais des structures organisant le raisonnement. Par conséquent, la distinction bilatérale (assertion vs négation) est restreinte au niveau atomique (littéraux).
Dualité Inférentielle : La classicalité est récupérée non pas en ajoutant une sémantique de valeurs de vérité, mais en introduisant deux principes d'inférence harmonieux au niveau atomique (suivant Negri et von Plato) :
1. Exclusion (EXC1) : Affirmer et nier un même contenu mène à l'absurdité ( $l, l^\perp \vdash \bot$ ).
2. Analyse de Cas (EXC2) : Si une conclusion découle à la fois d'une assertion et de sa négation duale, elle en découle directement ( $l \vdash \phi, l^\perp \vdash \phi \implies \vdash \phi$ ).

3. Développement Technique

Système de Déduction Naturelle ( $NK^\pm$ ) : Les auteurs définissent un système de déduction naturelle comprenant les règles intuitionnistes standards ($NJ$) plus les règles de dualité atomique (EXC1 et EXC2). Ce système traite les littéraux comme la base, avec des formules complexes construites via les connecteurs standards.
Sémantique d'Extension de Base (B-eS) :
- Bases ( $B$ ) : Une base est un ensemble de règles atomiques (relations inférentielles entre littéraux).
- Dérivabilité ( $\vdash_B$ ) : La dérivabilité dans une base est définie de manière inductive. Elle inclut les règles structurelles standards (réflexivité, application) et les deux nouvelles clauses (exc1, exc2) qui imposent la dualité au niveau du littéral.
- Support ( $\Vdash_B$ ) : La validité d'une formule est définie de manière inductive sur la structure des formules. Crucialement, les clauses de support pour les connecteurs ( $\to, \land, \lor$ ) sont identiques aux définitions intuitionnistes de Sandqvist. Le caractère classique de la sémantique est porté entièrement par les clauses de dualité dans la définition de la dérivabilité dans la base, et non par les clauses de support pour les formules complexes.
- Validité ( $\Gamma \Vdash \phi$ ) : Une formule est valide si elle est supportée dans toutes les bases.

4. Résultats Clés

Correction (Théorème 5.1) : Le système est correct : si $\Gamma \vdash_{NK^\pm} \phi$ , alors $\Gamma \Vdash \phi$ . La preuve procède par induction sur la dérivation, montrant que les règles classiques (EXC1, EXC2) préservent le support.
Complétude (Théorème 6.2) : Le système est complet : si $\Gamma \Vdash \phi$ $Γ ⊩ ϕ$ , alors $\Gamma \vdash_{NK^\pm} \phi$ $Γ ⊢_{N K^{\pm}} ϕ$ .
- La preuve adapte la méthode élémentaire de Sandqvist pour la logique intuitionniste.
- Elle utilise une « base de simulation » ( $\mathcal{N}$ ) construite à partir des sous-formules du séquent.
- Un opérateur d'« aplatissement » (flattening) mappe les formules complexes vers des littéraux atomiques au sein de la base de simulation.
- Le lemme de « Naturalisation » démontre que la dérivabilité dans la base de simulation peut être traduite en retour en dérivabilité dans $NK^\pm$ .
- Contrairement aux approches précédentes, cette preuve traite le langage propositionnel complet (incluant $\lor$ ) et repose sur des ressources mathématiques élémentaires, évitant l'induction sur les barres ou les modèles canoniques.

5. Signification et Revendications
L'article affirme fournir une nouvelle sémantique de type preuve-théorique pour la logique classique qui :

Unifie l'IPL et la CPL : Il démontre que la logique classique peut être comprise comme la logique intuitionniste complétée par un principe primitif de dualité au niveau atomique.
Respecte l'Anti-Réalisme : En évitant les valeurs de vérité et la bivalence, et en utilisant une preuve de complétude constructive, il offre un fondement véritablement anti-réaliste pour la logique classique, répondant au défi fondamental de Dummett.
Simplifie la Complexité Technique : En restreignant le bilatéralisme aux littéraux et en traitant les formules complexes comme structurelles, les auteurs parviennent à une preuve de complétude au « caractère étonnamment élémentaire » comparable au travail de Sandqvist sur la logique intuitionniste, surmontant les difficultés techniques des tentatives précédentes de B-eS classique.
Offre une Alternative à la Modélisation : Les auteurs positionnent ce travail comme une alternative à la sémantique de type modèle et aux approches de P-tS existantes qui reposent sur des concepts de type modèle (telles que celles de Makinson ou Eckhardt et Pym), visant à établir un compte purement inférentialiste de la logique classique.

L'article conclut que ce cadre ouvre la possibilité d'un traitement systématique des logiques classiques analogue au traitement systématique déjà établi pour les logiques intuitionnistes au sein de la tradition P-tS.