Incomplétude Sémantique du Système à la Hilbert de Liberman et al. (2020) pour la Logique Modale Terminale K avec Égalité et Termes Non-rigides

Informations Fondamentales

• ID de l'article: 2501.00486
• Titre: Semantic Incompleteness of Liberman et al. (2020)'s Hilbert-style System for Term-modal Logic K with Equality and Non-rigid Terms
• Auteur: Takahiro Sawasaki (Faculté des Sciences et Lettres, Université de Kanazawa)
• Classification: cs.LO (Informatique - Logique)
• Conférence de publication: Non-Classical Logics Theory and Applications (NCL'24), EPTCS 415, 2024
• Lien de l'article: doi:10.4204/EPTCS.415.9

Résumé

Cet article démontre l'incomplétude sémantique du système à la Hilbert pour la logique modale terminale K minimale et régulière proposée par Liberman et al. (2020) dans « Dynamic Term-modal Logics for First-order Epistemic Planning ». Ce système traite de la logique avec égalité et termes non-rigides. La logique modale terminale est une classe de logique modale du premier ordre possédant des opérateurs modaux terminaux indexés par des termes du langage du premier ordre. Bien que certaines formules du premier ordre soient valides dans la sémantique de Kripke de la logique modale terminale proposée sur toutes les classes de cadres, elles ne sont pas dérivables dans le système à la Hilbert de Liberman et al. L'auteur démontre ce fait en introduisant une sémantique de Kripke non-standard qui rend la signification des symboles de constante et de fonction relative à la signification des symboles de relation auxquels ils sont associés.

Contexte et Motivation de la Recherche

Contexte du Problème

1. Importance de la logique modale terminale: La logique modale terminale, développée par Thalmann et Fitting et al., est une classe de logique modale du premier ordre possédant des opérateurs modaux t indexés par des termes, plus expressive que la logique propositionnelle multimodale, largement appliquée à la logique épistémique et la logique morale.
2. Système de Liberman et al.: Ils ont développé une logique épistémique dynamique du premier ordre pour la planification cognitive, utilisant la logique modale terminale comme logique sous-jacente. Techniquement, il s'agit d'une logique modale terminale régulière biclassifiée à domaine constant avec égalité et termes non-rigides.
3. Défauts de la définition syntaxique: Les définitions originales 1-3 présentent deux problèmes:
   • L'assignation de type et la définition des termes sont mutuellement dépendantes, formant une définition circulaire
   • Certaines expressions qui devraient être des formules (comme x=x) ne peuvent pas réellement être des formules

Motivation de la Recherche

1. Intégrité théorique: Démontrer l'incomplétude sémantique du système HK existant, révélant ses limitations théoriques
2. Fondements logiques: Fournir une base théorique pour le développement ultérieur de la logique modale terminale
3. Innovation méthodologique: Révéler les insuffisances des systèmes logiques par le biais de sémantiques non-standard

Contributions Essentielles

1. Démonstration de l'incomplétude sémantique: Première preuve rigoureuse que le système à la Hilbert HK de Liberman et al. est incomplet par rapport à la sémantique TML
2. Construction de formules contreexemples: Identification de la formule x = c → (P(x) → P(c)), qui est valide dans la sémantique TML mais non dérivable dans HK
3. Introduction d'une sémantique non-standard: Proposition innovante d'une sémantique de Kripke non-standard rendant la signification des symboles de constante et de fonction relative à la signification des symboles de relation
4. Correction des définitions syntaxiques: Corrections nécessaires apportées aux définitions syntaxiques originales, résolvant les problèmes de définition circulaire et d'appariement de types
5. Fourniture d'intuitions théoriques: Révélation que cette incomplétude n'est pas liée à l'aspect modal terminale, mais provient de problèmes fondamentaux de la logique modale du premier ordre

Détails Méthodologiques

Définition de la Tâche

Démontrer l'incomplétude sémantique du système à la Hilbert HK par rapport à la sémantique TML, c'est-à-dire trouver une formule valide dans la sémantique TML mais non dérivable dans HK.

Correction Syntaxique

L'auteur corrige d'abord les définitions syntaxiques originales:

Définition 1 (Signature):

• Ensemble de types TYPE = {agt, obj, agt or obj}
• Relation d'ordre partiel ⪯ définie par agt ⪯ agt or obj et obj ⪯ agt or obj
• Fonction d'assignation de type mappant les variables à des types concrets et les symboles de relation à des séquences de types

Définition 2 (Termes typés): Définition récursive du type des termes, assurant la cohérence des types dans l'application de fonctions

Définition 3 (Langage): Définition des structures de formules utilisant la forme BNF, garantissant que s dans l'opérateur modal Ks doit être de type agent

Construction de la Sémantique Non-standard

Innovation centrale: Dans le modèle non-standard, l'interprétation des symboles de constante et de fonction dépend du triplet ⟨symbole, monde, ensemble de relations⟩, plutôt que du couple traditionnel ⟨symbole, monde⟩.

Définition 9 (Modèle non-standard):

N = ⟨D,W,R,J⟩
où J mappe ⟨c,w,X⟩ à un élément de Dt(c)

Intuition clé: Cela permet à une même constante c d'avoir des significations différentes dans différentes relations P(c) et Q(c):

• J(c,w,J(P,w)) ≠ J(c,w,J(Q,w))

Stratégie de Preuve d'Incomplétude

1. Construction du contreexemple: Utilisation de la formule x = c → (P(x) → P(c))
2. Preuve de validité TML: Démonstration que cette formule est évidemment valide dans la sémantique TML standard
3. Preuve de correction de HK: Démonstration que HK est correct par rapport à la sémantique non-standard
4. Preuve d'invalidité non-standard: Construction d'un modèle non-standard rendant la formule invalide
5. Déduction d'incomplétude: Déduction de la non-dérivabilité de la formule dans HK par correction

Configuration Expérimentale

Méthode de Vérification Théorique

Cet article emploie une méthode de preuve purement théorique, sans données expérimentales:

1. Vérification de validité de formule: Démonstration par analyse sémantique de la validité de la formule cible dans la sémantique TML
2. Preuve de correction du système: Vérification individuelle de tous les axiomes de HK dans la sémantique non-standard
3. Construction de contreexemple: Conception minutieuse d'un modèle non-standard rendant la formule cible invalide

Techniques de Preuve

• Induction: Utilisée pour prouver le lemme de substitution et l'équivalence de satisfaction
• Analyse sémantique: Analyse des conditions de vérité des formules dans différents cadres sémantiques
• Construction de modèle: Conception de modèles contreexemples concrets

Résultats Expérimentaux

Résultats Théoriques Principaux

Proposition 1: La formule x = c → (P(x) → P(c)) est valide dans la sémantique TML Preuve: Analyse sémantique directe, basée sur la transitivité de l'égalité

Proposition 2: Cette formule est invalide dans la sémantique non-standard Preuve: Construction d'un modèle contreexemple concret, où:

• Dagt = {α, β}
• J(c,w,{⟨d,d⟩ | d ∈ Dagt or obj}) = α
• J(c,w,{α}) = β
• J(P,w) = {α}
• v(x) = α

Théorème 1 (Correction): HK est correct par rapport à la sémantique non-standard Preuve: Vérification individuelle de tous les axiomes et règles d'inférence préservant la validité dans la sémantique non-standard

Théorème 2: La formule x = c → (P(x) → P(c)) n'est pas dérivable dans HK Preuve: Déduction directe de la correction et de la Proposition 2

Corollaire 1 (Incomplétude sémantique): HK est sémantiquement incomplet par rapport à la sémantique TML

Intuitions Techniques Clés

1. Préservation du lemme de substitution: La sémantique non-standard préserve toujours les propriétés fondamentales de la substitution
2. Traitement des opérateurs modaux: Le terme t dans l'opérateur modal Kt utilise l'ensemble vide comme contexte de relation, assurant la cohérence avec la sémantique standard
3. Particularité de la relation d'égalité: La relation d'égalité = préserve l'interprétation standard, non affectée par le contexte de relation

Travaux Connexes

Développement de la Logique Modale Terminale

1. Travaux fondateurs: Thalmann (2000), Fitting et al. (2001) établissent les fondations théoriques de la logique modale terminale
2. Domaines d'application:
   • Logique épistémique: Kooi (2008), Rendsvig (2010-2011), Wang & Seligman (2018)
   • Logique morale: Sawasaki et al. (2019-2021), Frijters (2021-2023)

Problèmes de Complétude en Logique Modale du Premier Ordre

1. Difficultés classiques: Fagin et al. (2003) soulignent les défis techniques de la complétude en logique modale du premier ordre
2. Axiomes restrictifs: Adoption de versions à variables restreintes des axiomes pour éviter la dérivabilité de formules invalides
3. Problèmes ouverts: Un système à la Hilbert sémantiquement correct et complet pour la logique modale du premier ordre reste un problème ouvert

Contribution Unique de cet Article

Comparé aux travaux existants, cet article est le premier à:

• Démontrer rigoureusement l'incomplétude d'un système spécifique de logique modale terminale
• Introduire une méthode de sémantique non-standard innovante
• Révéler que la source du problème réside au niveau du premier ordre plutôt qu'au niveau modal

Conclusion et Discussion

Conclusions Principales

1. Confirmation d'incomplétude: Le système HK de Liberman et al. présente effectivement une incomplétude sémantique
2. Localisation du problème: L'incomplétude provient du niveau de la logique du premier ordre, indépendante des caractéristiques modales terminales
3. Validité de la méthode: La sémantique non-standard fournit un outil efficace pour analyser ce type de problème

Limitations

1. Restriction de portée: L'analyse s'applique uniquement au système HK spécifique, ne couvrant pas tous les systèmes de logique modale terminale
2. Nature constructive: La sémantique non-standard est construite à des fins spécifiques et peut ne pas s'appliquer à d'autres analyses
3. Applicabilité pratique: L'impact direct des résultats théoriques sur les applications pratiques nécessite une recherche ultérieure

Directions Futures

1. Construction de systèmes complets: Recherche d'un système à la Hilbert sémantiquement correct et complet pour la logique modale terminale K
2. Applications au langage naturel: Application de la sémantique non-standard à l'analyse de la dépendance contextuelle de la référence nominale en langage naturel
3. Extension des systèmes: Étude des problèmes de complétude pour d'autres systèmes de logique modale terminale

Évaluation Approfondie

Avantages

1. Rigueur théorique: Preuve complète avec détails techniques suffisants, raisonnement logique irréprochable
2. Innovativité méthodologique: L'introduction de la sémantique non-standard démontre une intuition technique distinctive
3. Importance du problème: Résout un problème théorique fondamental dans le domaine de la logique modale terminale
4. Clarté de la rédaction: Structure claire de l'article, expression technique précise

Insuffisances

1. Portée de l'impact: Les résultats sont principalement d'importance théorique, avec une orientation pratique limitée
2. Solutions: Identifie le problème mais ne fournit pas de solution constructive
3. Généralité: Le degré de généralisation de la méthode reste à vérifier

Influence

1. Contribution théorique: Fournit un résultat négatif important pour le développement théorique de la logique modale terminale
2. Valeur méthodologique: La méthode de sémantique non-standard peut inspirer les recherches dans les domaines connexes
3. Signification fondamentale: Révèle les difficultés profondes des problèmes de complétude en logique modale du premier ordre

Scénarios d'Application

1. Recherche en logique: Fournit des références pour la recherche théorique en logique modale terminale et logique modale du premier ordre
2. Vérification formelle: Dans les systèmes formalisés nécessitant un raisonnement logique précis, il faut tenir compte de ce type d'incomplétude
3. Logique cognitive: Dans les applications telles que la planification cognitive, il faut noter les limitations du système logique sous-jacent

Références Bibliographiques

L'article cite 24 références pertinentes, incluant principalement:

• Liberman et al. (2020): Article original du système analysé
• Fitting et al. (2001): Travaux fondateurs de la logique modale terminale
• Fagin et al. (2003): Manuel classique du raisonnement en logique modale du premier ordre
• Thalmann (2000): Développement précoce de la logique modale terminale

Cet article révèle par une analyse théorique rigoureuse l'incomplétude d'un important système logique. Bien que le résultat soit négatif, il possède une signification importante pour la compréhension des fondations théoriques de la logique modale terminale. L'introduction de la sémantique non-standard démontre une approche technique innovante qui pourrait inspirer les recherches dans les domaines connexes.