Une note sur le système CNL$^2_4$ de Grigoriev et Zaitsev

Informations fondamentales

• ID de l'article: 2501.00500
• Titre: Une note sur le système CNL$^2_4$ de Grigoriev et Zaitsev
• Auteurs: Hitoshi Omori (Université de Tohoku), Jonas R. B. Arenhart (Université fédérale de Santa Catarina)
• Classification: cs.LO (Logique)
• Date de publication/Conférence: NCL'24 (Théorie et applications des logiques non classiques), EPTCS 415, 2024
• Lien de l'article: https://arxiv.org/abs/2501.00500

Résumé

Cet article approfondit l'étude du système de logique à quatre valeurs CNL$^2_4$ récemment proposé par Oleg Grigoriev et Dmitry Zaitsev. Les auteurs non seulement clarifient les liens entre ce système et les systèmes connexes développés par Paul Ruet et Norihiro Kamide, mais discutent également de deux importantes questions philosophiques qui en résultent : la première est le « thème haackien » — comment comprendre la signification des connecteurs et la nature de la vérité dans les logiques multivaluées ; la deuxième est l'approfondissement du « problème de Carnap » — un même système de preuve peut avoir au moins quatre interprétations différentes et incompatibles.

Contexte et motivation de la recherche

Problèmes fondamentaux

1. Problème de compréhensibilité de la signification des connecteurs: Dans les systèmes de logique multivaluée, comment rendre compréhensible aux logiciens classiques la signification des connecteurs non classiques et la nature de la vérité.
2. Problème d'indétermination sémantique: Un même système formel peut posséder plusieurs interprétations sémantiques incompatibles, entraînant une indétermination du sens.

Importance de la recherche

• Les systèmes de logique non classique s'écartent des normes classiques, mais nous devons maintenir notre compréhension des connecteurs et des conséquences logiques
• Stratégie proposée par Susan Haack : éliminer le mystère des systèmes non classiques en fournissant des interprétations « quasi classiques »
• Explorer la relation entre les systèmes formels et leurs interprétations, ce qui constitue un problème central de la philosophie de la logique

Limitations des approches existantes

• Absence d'analyse systématique des relations entre le système CNL$^2_4$ et d'autres systèmes de logique à quatre valeurs connexes
• Manque de discussion philosophique approfondie sur le problème des interprétations multiples
• Nécessité de meilleures stratégies pour améliorer la compréhensibilité des systèmes de logique non classique

Contributions principales

1. Fourniture d'un système de déduction naturelle pour CNL$^2_4$, avec preuves de correction et de complétude
2. Preuve de la complétude définitionnelle et de la complétude de Post pour CNL$^2_4$
3. Révélation de quatre interprétations différentes du système CNL$^2_4$, correspondant chacune à une compréhension sémantique distincte
4. Établissement de liens précis entre CNL$^2_4$ et les systèmes de Ruet et Kamide
5. Analyse approfondie de la manifestation du « problème de Carnap » et du « thème haackien » dans ce système
6. Proposition d'une approche de sémantique relationnelle pour améliorer la compréhensibilité classique du système

Détails méthodologiques

Définition du système

Langage: Le langage L de CNL$^2_4$ contient:

• Ensemble de connecteurs: {∼, ∧, ∨}
• Ensemble dénombrable de variables propositionnelles: Prop

Sémantique:

• Quatre valeurs de vérité: {1, i, j, 0}
• Fonction d'interprétation: I: Prop → {1, i, j, 0}
• Ensemble de valeurs désignées: D = {1, i}

Tables de vérité:

A  ∼A     A∧B  1 i j 0     A∨B  1 i j 0
1   i      1   1 i j 0      1   1 1 1 1
i   0      i   i i 0 0      i   1 i 1 i
j   1      j   j 0 j 0      j   1 1 j j
0   j      0   0 0 0 0      0   1 i j 0

Système de preuve

Les auteurs fournissent un système de déduction naturelle RCNL$^2_4$, comprenant les règles suivantes:

Règles standard:

• Introduction/élimination de la conjonction
• Introduction/élimination de la disjonction

Règles spéciales:

• (∼∼1): A ∼∼A / B
• (∼∼2): A∨∼∼A
• Diverses formes des lois de De Morgan

Quatre modes d'interprétation

Les auteurs découvrent que le système CNL$^2_4$ peut avoir quatre interprétations différentes:

Où: v=vrai, f=faux, b=à la fois vrai et faux, n=ni vrai ni faux

Points d'innovation technique

1. Cadre unifié

Fourniture d'un cadre unifié par la sémantique relationnelle (sémantique de Dunn) pour comprendre les quatre interprétations différentes, en réécrivant les quatre valeurs {1,i,j,0} comme .

2. Preuve de complétude fonctionnelle

Preuve que le système CNL$^2_4$ est fonctionnellement complet, c'est-à-dire qu'il peut définir toutes les fonctions quaternaires possibles, notamment:

• Toutes les fonctions δ: δₐ(b) = 1 si et seulement si a = b
• Toutes les fonctions constantes: Cₐ(b) = a

3. Définissabilité de la négation classique

La négation classique peut être définie à l'intérieur du système, fournissant aux logiciens classiques des outils familiers.

Configuration expérimentale

Vérification théorique

Les auteurs valident les résultats théoriques de la manière suivante:

1. Preuves de correction et de complétude:
   • Utilisation du lemme standard de Lindenbaum
   • Construction de valuations canoniques
   • Preuve du lemme d'extension
2. Vérification de la complétude fonctionnelle:
   • Application du théorème de Słupecki
   • Vérification de la définissabilité de toutes les fonctions unaires
   • Preuve de l'existence de fonctions binaires essentielles

Résultats expérimentaux

Résultats théoriques principaux

Théorème 1 (Correction): Pour tous Γ∪{A} ⊆ Form, si Γ ⊢ A, alors Γ |=CNL$^2_4$ A

Théorème 2 (Complétude): Pour tous Γ∪{A} ⊆ Form, si Γ |=CNL$^2_4$ A, alors Γ ⊢ A

Théorème 5 (Complétude définitionnelle): CNL$^2_4$ est définitionnellement complet

Corollaire 1 (Complétude de Post): CNL$^2_4$ est complet au sens de Post

Résultats de validité

Proposition 1: Les énoncés suivants sont valides dans CNL$^2_4$:

• B |=CNL$^2_4$ (A∨∼∼A)
• B |=CNL$^2_4$ ∼(A∨∼∼A)
• A∧∼∼A |=CNL$^2_4$ B
• ∼(A∧∼∼A) |=CNL$^2_4$ B

Proposition 2: Les énoncés suivants ne sont pas valides dans CNL$^2_4$:

• q ⊭CNL$^2_4$ p∨∼p
• p∧∼p ⊭CNL$^2_4$ q
• ∼∼p ⊭CNL$^2_4$ p
• p ⊭CNL$^2_4$ ∼∼p

Travaux connexes

Systèmes de logique à quatre valeurs

1. FDE (First-Degree Entailment): Fondement de la logique de Belnap-Dunn
2. Système de Ruet: Ajout d'un opérateur de négation spécial à la base de FDE
3. Système de Kamide: Une autre approche de la logique à quatre valeurs

Contexte philosophique

1. Stratégie de Susan Haack: Amélioration de la compréhensibilité des systèmes non classiques par des interprétations classiques
2. Problème de Carnap: Un système de preuve ne peut pas déterminer de manière unique l'interprétation prévue
3. Thèse de variation de sens de Quine: Le changement logique entraîne-t-il un changement de sens?

Conclusions et discussion

Conclusions principales

1. Équivalence des systèmes: CNL$^2_4$ sous différentes interprétations est équivalent à des systèmes logiques connus (Ruet, Kamide, etc.)
2. Indétermination du sens: Un même système de preuve peut supporter quatre compréhensions sémantiques fondamentalement différentes, ce qui constitue un approfondissement du problème de Carnap
3. Compréhensibilité classique: Par la stratégie haackienne et la sémantique relationnelle, les logiciens classiques peuvent comprendre ce système
4. Statut de la négation: Le caractère de ∼ en tant que véritable négation dépend de l'interprétation adoptée et des exigences concernant la négation

Limitations

1. Problème du choix d'interprétation: Absence de raison purement logique pour choisir l'une des quatre interprétations
2. Difficultés de communication: Les personnes utilisant le même système peuvent avoir des compréhensions complètement différentes sans le savoir
3. Problème de fixation du sens: Le système lui-même ne peut pas fixer la signification des connecteurs

Directions futures

1. Extension à d'autres systèmes multivaluées: Application de la méthode d'analyse à d'autres logiques non classiques
2. Critères pratiques: Développement de critères pratiques pour le choix d'une interprétation spécifique
3. Approfondissement philosophique: Exploration ultérieure de la relation entre les systèmes formels et le sens

Évaluation approfondie

Points forts

1. Contributions théoriques profondes: Non seulement des résultats techniques, mais aussi une discussion approfondie de questions importantes de philosophie de la logique
2. Analyse complète: Examen du système sous plusieurs angles: théorie de la preuve, sémantique et philosophie
3. Relations claires: Établissement explicite des relations avec les systèmes existants
4. Innovation méthodologique: Application de la stratégie haackienne à l'analyse de la logique à quatre valeurs

Insuffisances

1. Utilité pratique limitée: Principalement une analyse théorique, manque de considérations applicatives
2. Solutions incomplètes: Bien que les problèmes soient identifiés, l'indétermination du sens n'est pas complètement résolue
3. Complexité technique: La complexité des quatre interprétations peut limiter l'application pratique du système

Impact

1. Valeur théorique élevée: Offre une nouvelle perspective pour l'analyse philosophique des logiques multivaluées
2. Contribution méthodologique: Démontre comment analyser systématiquement les systèmes de logique non classique
3. Signification interdisciplinaire: Établit des liens entre la logique formelle et la philosophie de la logique

Scénarios d'application

1. Recherche en philosophie de la logique: Fournit des cas d'étude pour discuter des relations entre sens, vérité et systèmes logiques
2. Théorie de la logique multivaluée: Offre une méthodologie pour l'analyse d'autres systèmes multivaluées
3. Conception de systèmes formels: Sensibilise les concepteurs au problème de l'indétermination sémantique

Références bibliographiques

L'article cite 24 références importantes, notamment:

• Philosophy of Logics de Susan Haack
• Les travaux classiques de Quine sur la déviation logique
• Les recherches connexes sur la logique de Belnap-Dunn
• Les systèmes de logique à quatre valeurs de Ruet et Kamide
• Les résultats classiques sur la complétude fonctionnelle (théorème de Słupecki)

Évaluation globale: Cet article est un travail théorique de haute qualité en logique qui non seulement fournit des résultats techniques solides, mais explore également des questions philosophiques importantes. La valeur principale de l'article réside dans la révélation du problème profond de l'indétermination du sens dans les systèmes de logique formelle et la fourniture de stratégies pour améliorer la compréhensibilité. Bien que principalement théorique, il apporte une contribution importante au développement de la logique et de la philosophie de la logique.