Semantic Incompleteness of Liberman et al. (2020)'s Hilbert-style System for Term-modal Logic K with Equality and Non-rigid Terms

Basic Information

• Paper ID: 2501.00486
• Title: Semantic Incompleteness of Liberman et al. (2020)'s Hilbert-style System for Term-modal Logic K with Equality and Non-rigid Terms
• Author: Takahiro Sawasaki (Faculty of Liberal Arts, Kanazawa University)
• Classification: cs.LO (Computer Science - Logic)
• Conference: Non-Classical Logics Theory and Applications (NCL'24), EPTCS 415, 2024
• Paper Link: doi:10.4204/EPTCS.415.9

Abstract

This paper demonstrates the semantic incompleteness of the Hilbert-style system for the minimal normal term-modal logic K proposed by Liberman et al. (2020) in "Dynamic Term-modal Logics for First-order Epistemic Planning." The system handles logic with equality and non-rigid terms. Term-modal logic is a class of first-order modal logic featuring term-indexed modal operators indexed by terms from first-order language. Although certain first-order formulas are valid in the Kripke semantics of the proposed term-modal logic across all frame classes, they are not derivable in Liberman et al.'s Hilbert-style system. The author demonstrates this fact by introducing non-standard Kripke semantics that relativize the meanings of constants and function symbols to the meanings of relation symbols with which they are combined.

Research Background and Motivation

Problem Background

1. Importance of Term-modal Logic: Term-modal logic, developed by Thalmann and Fitting et al., is a class of first-order modal logic with term-indexed modal operators t, more expressive than multimodal propositional logic, with widespread applications in epistemic logic and deontic logic.
2. Liberman et al.'s System: They developed a first-order dynamic epistemic logic for cognitive planning with term-modal logic as the underlying logic. Technically, this is a constant-domain bipartite normal term-modal logic with equality and non-rigid terms.
3. Defects in Syntactic Definition: The original Definitions 1-3 contain two problems:
   • Type assignments and term definitions are mutually dependent, forming circular definitions
   • Certain expressions that should be formulas (such as x=x) cannot actually become formulas

Research Motivation

1. Theoretical Completeness: Proving the semantic incompleteness of the existing system HK to reveal its theoretical limitations
2. Logical Foundations: Providing theoretical foundations for further development of term-modal logic
3. Methodological Innovation: Revealing inadequacies of logical systems through non-standard semantics

Core Contributions

1. Proved Semantic Incompleteness: First rigorous proof that Liberman et al.'s Hilbert-style system HK is incomplete with respect to TML semantics
2. Constructed Counterexample Formula: Found the formula x = c → (P(x) → P(c)), which is valid in TML semantics but not derivable in HK
3. Introduced Non-standard Semantics: Innovatively proposed non-standard Kripke semantics that relativize the meanings of constants and function symbols to the meanings of relation symbols
4. Corrected Syntactic Definitions: Made necessary corrections to the original syntactic definitions, resolving circular definitions and type-matching problems
5. Provided Theoretical Insights: Revealed that this incompleteness is unrelated to the term-modal aspect but stems from fundamental problems in first-order modal logic

Methodology Details

Task Definition

Prove the semantic incompleteness of Hilbert-style system HK with respect to TML semantics, i.e., find a formula that is valid in TML semantics but not derivable in HK.

Syntactic Correction

The author first corrected the original syntactic definitions:

Definition 1 (Signature):

• Type set TYPE = {agt, obj, agt or obj}
• Partial order relation ⪯ defined as agt ⪯ agt or obj and obj ⪯ agt or obj
• Type assignment function maps variables to concrete types and relation symbols to type sequences

Definition 2 (Typed Terms): Recursively define term types, ensuring type consistency in function applications

Definition 3 (Language): Define formula structure using BNF notation, ensuring that s in term-modal operator Ks must be of agent type

Non-standard Semantics Construction

Core Innovation: In non-standard models, the interpretation of constants and function symbols depends on triples ⟨symbol, world, relation set⟩, rather than traditional pairs ⟨symbol, world⟩.

Definition 9 (Non-standard Model):

N = ⟨D,W,R,J⟩
where J maps ⟨c,w,X⟩ to elements in Dt(c)

Key Insight: This allows the same constant c to have different meanings in different relations P(c) and Q(c):

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

Incompleteness Proof Strategy

1. Construct Counterexample: Use the formula x = c → (P(x) → P(c))
2. Prove TML Validity: Show the formula is obviously valid in standard TML semantics
3. Prove HK Soundness: Prove HK is sound with respect to non-standard semantics
4. Prove Non-standard Invalidity: Construct a non-standard model making the formula invalid
5. Derive Incompleteness: From soundness, conclude the formula is not derivable in HK

Experimental Setup

Theoretical Verification Method

This paper employs pure theoretical proof methods without experimental data:

1. Formula Validity Verification: Prove the target formula's validity in TML semantics through semantic analysis
2. System Soundness Proof: Verify all axioms of HK remain valid in non-standard semantics
3. Counterexample Construction: Carefully design non-standard models making the target formula invalid

Proof Techniques

• Induction: Used for proving substitution lemmas and satisfaction equivalence
• Semantic Analysis: Analyze truth conditions of formulas across different semantic frameworks
• Model Construction: Design concrete counterexample models

Experimental Results

Main Theoretical Results

Proposition 1: The formula x = c → (P(x) → P(c)) is valid in TML semantics Proof: Direct semantic analysis based on transitivity of equality

Proposition 2: The formula is invalid in non-standard semantics Proof: Construct a concrete counterexample model where:

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

Theorem 1 (Soundness): HK is sound with respect to non-standard semantics Proof: Verify all axioms and inference rules preserve validity in non-standard semantics

Theorem 2: The formula x = c → (P(x) → P(c)) is not derivable in HK Proof: Directly follows from soundness and Proposition 2

Corollary 1 (Semantic Incompleteness): HK is semantically incomplete with respect to TML semantics

Key Technical Insights

1. Preservation of Substitution Lemma: Non-standard semantics still preserves the fundamental properties of substitution
2. Treatment of Modal Operators: The term t in term-modal operator Kt uses the empty set as relational context, ensuring consistency with standard semantics
3. Specificity of Equality Relation: The equality relation = maintains standard interpretation, unaffected by relational context

Related Work

Development of Term-modal Logic

1. Foundational Work: Thalmann (2000), Fitting et al. (2001) established foundational theory of term-modal logic
2. Application Domains:
   • Epistemic Logic: Kooi (2008), Rendsvig (2010-2011), Wang & Seligman (2018)
   • Deontic Logic: Sawasaki et al. (2019-2021), Frijters (2021-2023)

Completeness Problems in First-order Modal Logic

1. Classical Difficulties: Fagin et al. (2003) identified technical challenges in first-order modal logic completeness
2. Restrictive Axioms: Variable-restricted versions of axioms adopted to avoid derivability of invalid formulas
3. Open Problems: Sound and complete Hilbert-style systems for FOML semantics remain open

Unique Contributions of This Paper

Compared to existing work, this paper is the first to:

• Rigorously prove incompleteness of a specific term-modal logic system
• Introduce innovative non-standard semantic methods
• Reveal that the problem's root lies at the first-order level rather than the modal level

Conclusions and Discussion

Main Conclusions

1. Incompleteness Confirmed: Liberman et al.'s HK system indeed exhibits semantic incompleteness
2. Problem Localization: Incompleteness originates at the first-order logic level, unrelated to term-modal characteristics
3. Method Validity: Non-standard semantics provides an effective tool for analyzing such problems

Limitations

1. Scope Restriction: Analysis applies only to the specific HK system, not covering all term-modal logic systems
2. Constructedness: Non-standard semantics is constructed for specific purposes and may not apply to other analyses
3. Practicality: Direct implications of theoretical results for practical applications require further investigation

Future Directions

1. Complete System Construction: Seek sound and complete Hilbert-style systems for term-modal logic K
2. Natural Language Applications: Apply non-standard semantics to analyze context-dependent reference of nouns in natural language
3. System Extensions: Investigate completeness problems for other term-modal logic systems

In-depth Evaluation

Strengths

1. Theoretical Rigor: Complete proofs with sufficient technical details and flawless logical reasoning
2. Methodological Innovation: Introduction of non-standard semantics demonstrates unique technical insight
3. Problem Importance: Resolves a fundamental theoretical problem in term-modal logic
4. Writing Clarity: Clear paper structure and accurate technical exposition

Weaknesses

1. Impact Scope: Results are primarily theoretical with limited guidance for practical applications
2. Solution Provision: Identifies problems but lacks constructive solutions
3. Generalizability: Degree of method generalization requires verification

Influence

1. Theoretical Contribution: Provides important negative results for term-modal logic theory development
2. Method Value: Non-standard semantic methods may inspire research in related fields
3. Foundational Significance: Reveals deep difficulties in first-order modal logic completeness problems

Applicable Scenarios

1. Logic Research: Provides reference for theoretical research in term-modal and first-order modal logic
2. Formal Verification: Systems requiring precise logical reasoning must consider such incompleteness
3. Epistemic Logic: Applications like cognitive planning must account for limitations of underlying logical systems

References

The paper cites 24 related references, primarily including:

• Liberman et al. (2020): Original paper of the analyzed system
• Fitting et al. (2001): Foundational work on term-modal logic
• Fagin et al. (2003): Classical textbook on first-order modal logic reasoning
• Thalmann (2000): Early development of term-modal logic

Through rigorous theoretical analysis, this paper reveals the incompleteness of an important logical system. Although the result is negative, it holds significant importance for understanding the theoretical foundations of term-modal logic. The introduction of non-standard semantics demonstrates innovative technical approaches that may inspire research in related fields.