PaperlayerView exact revision on arXiv

Source-linked AI summary

On the Minimum Many-Valued Modal Logic over a Finite Residuated Lattice

Felix Bou, Francesc Esteva, Lluis Godo, Ricardo Rodriguez

arXiv:0811.2107v2math.LO

TL;DR

The paper addresses how to axiomatize minimum many-valued modal logics over finite residuated lattices when standard normality assumptions may fail. It develops expansions of non-modal axiomatizations for several frame classes, with and without canonical constants, and establishes related decidability and scope results.

  • Problem

    A systematic treatment of minimum many-valued modal logics is lacking, particularly for finite residuated lattices and settings where the normality axiom K fails.

  • Method

    The paper studies necessity-only Kripke semantics over full, idempotent, and crisp frames and expands axiomatizations of the corresponding non-modal residuated-lattice logics.

  • Results

    The paper gives these axiomatization expansions for finite residuated lattices with canonical constants, and axiomatizes each basic frame class for finite MV chains without canonical constants.

  • Takeaways & Limitations

    The results provide a framework for studying minimum many-valued modal logics over particular finite residuated lattices rather than only over classes of lattices.

  • Takeaways & Limitations

    Finite-model witnessing is not general, although all finite Kripke models are modally witnessed when the residuated lattice is a chain.

Abstract

from arXiv · show

This paper deals with many-valued modal logics, based only on the necessity operator, over a residuated lattice. We focus on three basic classes, according to the accessibility relation, of Kripke frames: the full class of frames evaluated in the residuated lattice (and so defining the minimum modal logic), the ones evaluated in the idempotent elements and the ones evaluated in 0 and 1. We show how to expand an axiomatization, with canonical constants in the language, of a finite residuated lattice into one of the modal logic, for each one of the three basic classes of Kripke frames, over the very lattice. And we also give axiomatizations for the case of a finite MV chain but this time without canonical constants.

1 Introduction

The paper develops a systematic framework for minimum many-valued modal logics over finite residuated lattices, focusing on necessity and several classes of many-valued accessibility frames. It addresses missing axiomatizations, especially when the normality axiom K fails, by expanding non-modal axiomatizations under specified assumptions.

  • Motivation: Many-valued modal logic combines modal semantics with non-classical truth values and has applications including fuzzy description logics, belief reasoning, and similarity-based reasoning.
  • Problem setting: The paper focuses on minimum modal logics, which use the largest class of Kripke frames with accessibility values in the residuated lattice rather than only 0 and 1.
  • Problem setting: When the normality axiom K fails, existing axiomatizations may be unavailable and the appropriate axiomatization becomes unclear, including for finite MV chains.
  • Contributions: The article expands axiomatizations of finite residuated lattices into minimum modal logics for finite lattices with canonical constants and finite MV chains without them.
  • Contributions: It treats full, idempotent, and crisp frames; the idempotent case is axiomatized generally with canonical constants, while the crisp case requires a unique coatom.
  • Method: The semantics uses necessity only and interprets □ϕ through many-valued accessibility, corresponding to the first-order formula ∀y(Rxy → Py) under the stated semantics.

2 Non-modal preliminares

The section develops the semantic and proof-theoretic framework for many-valued modal logics over residuated lattices, focusing on full, idempotent, crisp, and Boolean frames. It establishes validity, definability, comparison, and consequence-relation results that support later axiomatizations.

  • Framework: The paper assumes an axiomatization of the non-modal logic Λ(A) and explains how to expand it into modal logics over A.With canonical constants, Λ(Ac) is a conservative expansion of Λ(A), and the modal development likewise assumes a fixed axiomatization of Λ(Ac).
  • Framework: For complete residuated lattices, the minimum modal logic is defined using the full class of Kripke frames, alongside idempotent and crisp frame classes.The semantics interprets □ through many-valued accessibility, corresponding to the first-order formula ∀y(Rxy → Py).
  • Validity and definability: The idempotent-frame class is modally definable by (K), by meet-distributivity, or by the square-formula schema, without canonical constants.These equivalent characterizations identify IFr through formulas such as □(p → q) → (□p → □q) and (□p ⊙ □p) → □(p ⊙ p).
  • Validity and definability: Normality axiom (K) is valid in full frames exactly when A is a Heyting algebra, equivalently when full and idempotent frames coincide.A three-element MV-chain counterexample shows that (K) can fail in the minimum logic; a weaker MTL-related schema remains valid.
  • Frame comparisons: Boolean and crisp frames validate the same modal formulas over finite residuated lattices, and Boolean frames admit equivalent characterizations using distributive elements or coatoms.The equivalence is established even when canonical constants are allowed; the frame conditions are expressed by families of formulas involving □(a ∨ p).
  • Local and global logics: The section relates local and global consequence relations through closure properties, canonical-frame results, and an equivalence between consequence and derivability from the modal logic.For K ∈ {Fr, IFr, CFr}, theorems are characterized by derivability from Γ together with Λ(K,A), or from Γ together with Λ(K,Ac) when canonical constants are present.

4 Completeness of the modal logic when there are canonical constants and A is finite

For finite residuated lattices with canonical constants, the paper uses canonical-model constructions to obtain completeness results for several classes of many-valued Kripke frames, with additional assumptions for crisp frames. It also identifies open cases and explains the expressive role of canonical constants.

  • Scope and strategy: The paper expands axiomatizations of the underlying logic into complete axiomatizations for full, idempotent, and crisp frame classes.For crisp frames, the construction additionally assumes that the finite residuated lattice has a unique coatom.
  • Scope and strategy: Finiteness ensures that the underlying consequence relation is finitary, while canonical constants support the completeness proofs.The paper states that canonical constants are an assumption in the completeness proofs, except for the later Łukasiewicz-chain treatment.
  • Benefits of canonical constants: Canonical constants increase expressive power by allowing certain rules about accessibility values to be represented inside the formal language.For finite subsets X of the lattice, the paper gives a rule valid when accessibility values lie in X.
  • Full frames: For full frames, the canonical construction yields the minimum modal logic and axiomatizes its local consequence relation over the finite lattice.The result identifies L with Λ(Fr, Ac) and derives the local consequence relation from L together with the underlying axiomatic basis.
  • Idempotent frames: For idempotent frames, adding (□ϕ ⊙□ϕ) →□(ϕ ⊙ϕ) characterizes the corresponding modal logic through its canonical model.The canonical frame is shown to be idempotent, and the resulting local logic is axiomatized using the added schema and the basis for Λ(Ac).
  • Crisp frames: For crisp frames, completeness is obtained when the lattice has a unique coatom, and the global logic is axiomatized by Table 4.The construction also supports replacing suitable models with crisp submodels using formulas of the form □(k ∨ϕ) →(k ∨□ϕ).
  • Crisp frames: The crisp-frame results include a complete local and global axiomatization, with the normality axiom and Necessity rule providing an alternative presentation.The paper states that the global logic is the smallest extension of the local logic closed under Necessity, and that K plus Necessity can replace Monotonicity.

5 Completeness of the modal logic given by a finite MV chain

For finite MV chains without canonical constants, the paper develops axiomatizations of the minimum modal logic and of logics determined by crisp frames. Completeness is obtained through canonical Kripke models and truth lemmas, with additional axioms characterizing crisp-frame behavior.

  • Scope: The section studies modal logic over a fixed finite MV chain Ln with n ≥ 3, without canonical constants; ♦ is definable as ¬□¬.The completeness proofs build on earlier arguments that used canonical constants.
  • Minimum logic: Table 5 supplies an axiomatization of the minimum modal logic over Ln through the lattice axioms, normality principles, Modus Ponens, Monotonicity, and rules (Ra).The rules (Ra) rewrite corresponding non-modal rules for formulas under □.
  • Rule independence: The rules (R0.5) and (R1) are independent of the other axioms and rules in Table 5, as shown by separate matrix countermodels.The paper gives matrices satisfying all remaining axioms and rules while respectively failing (R0.5) or (R1).
  • Full frames: The canonical model Mcan(L) satisfies the Truth Lemma Vcan(ϕ, v) = v(ϕ), enabling the equivalence between semantic valuations and points of the canonical model.This yields the axiomatization of the local logic for full Kripke frames by the smallest modal logic set over Ln.
  • Crisp-frame extension: The normality axiom (K) alone is strictly weaker than the crisp-frame logic, while the added ηa principles provide the formulas needed beyond the full-frame minimum logic.A non-crisp model validates (K) but refutes (□p ⊕□p) ↔□(p ⊕p), and the paper explicitly identifies the ηa principles as the required additions.
  • Crisp frames: For crisp frames, adding ηa(□ϕ) →□ηa(ϕ) for every nonzero a ∈ Ln makes the canonical frame crisp and supports completeness.The resulting system axiomatizes both the local and global logics, with Modus Ponens and, for the global logic, Necessity.

6 Concluding Remarks

The concluding remarks identify open problems in extending and comparing many-valued modal logics, while recording decidability results and possible routes toward simpler axiomatizations for finite MV chains.

  • Open problems: The authors frame the study as an early investigation with many open questions about minimum modal logics over residuated lattices.The open problems include axiomatization, computational complexity, frame-class comparisons, and extensions beyond the present framework.
  • Future scope: The authors also leave simultaneous □ and ◇, classes of residuated lattices, and comparisons between different lattices for future study.These frameworks are explicitly identified as not yet studied in the article.
  • Known results: Finite residuated lattices yield decidable sets Λ(Fr, A) and Λ(Fr, Ac) via a filtration method.The paper contrasts this with the known Pspace-completeness of Λ(Fr, [0, 1]G).
  • Open problems: The standard Łukasiewicz algebra remains difficult because the finite-MV-chain proof does not adapt straightforwardly to its lack of strongly characterizing formulas.The authors identify additional difficulties involving valid rules and the non-finitarity of the non-modal logic.
  • Possible strategies: A possible simplification of Λ(Fr, Ln) represents a many-valued accessibility relation as a non-increasing sequence of crisp relations Ra indexed by nonzero lattice values.This yields a canonically associated multimodal logic with modalities □a interpreted through the crisp relations Ra.

A.1 The (non-modal) logic of a residuated lattice

This appendix reviews algebraic and proof-theoretic properties of the non-modal logic Λ(A), emphasizing when finitary deduction, local deduction, and axiomatization by Modus Ponens are available.

  • Algebraic properties: Λ(A) is algebraizable, and its theorems, finitary deductions, and full logic are characterized by algebraic closures of A and related structures.The corresponding criteria involve varieties, quasivarieties, and closures under I, S, and reduced products.
  • Deduction properties: For finite A, Λ(A) is finitary, while proofs by cases are available when 1 is join irreducible.These properties are stated independently of whether the logic has a single-rule axiomatization.
  • Limitations: The Local Deduction Theorem can fail for finite residuated lattices, as shown by the weak nilpotent minimum algebra.In that example, ¬¬p ⊢A p holds, but no finite power of ¬¬p yields the corresponding theorem.
  • Axiomatization: Finite BL chains and complete BL chains have Q(A) as a variety, so Λ(A) can be axiomatized using Modus Ponens as its only rule.The finite-chain result is stated separately from the complete-chain result.
  • Axiomatization: There is no general finite Hilbert axiomatization for every finite residuated lattice, although finite subdirectly irreducible lattices are finitely axiomatizable.The appendix also notes that recursive axiomatizability holds for every finite residuated lattice.

A.2 Adding canonical constants to the non-modal logic

The appendix studies Λ(Ac), the non-modal logic obtained by adding canonical constants, and gives algebraic criteria and axiomatization methods for important finite residuated lattices.

  • Consequences of constants: Adding canonical constants produces a conservative expansion of Λ(A), but can cause the Local Deduction Theorem and proofs by cases to fail.These failures are linked to the derivability of 0 from every non-top canonical constant.
  • Structural criteria: For finite A, the Local Deduction Theorem, Q(Ac) being a variety, simplicity of A, and having only 0 and 1 as idempotents are equivalent.The appendix presents these implications generally and states equivalence in the finite case.
  • Axiomatization: For finite simple A, Λ(Ac) is axiomatized using the witnessing and book-keeping axioms together with Modus Ponens.The appendix also gives the corresponding one-rule consequence for the unique-coatom case.
  • Algebraic presentation: The variety generated by Ac is axiomatized by an equational presentation of A plus witnessing and book-keeping axioms.This result is established through a subdirect-irreducibility argument and homomorphic representation.
  • Unique-coatom case: When A has a unique coatom k, the quasivariety generated by Ac additionally requires k ∨x ≈1 ⇒x ≈1.The appendix shows that replacing this quasiequation with a weaker-looking version is insufficient, using G3 as a counterexample.

B The non-modal companion method

The non-modal companion method translates modal formulas into non-modal formulas to test validity and derive modal consequences across full, idempotent, and crisp frame classes.

  • Scope: The method is not complete for every invalid formula, as shown by a formula whose companion is provable although it fails on crisp frames.Its usefulness is therefore strongest as a simple validity-discarding method in cases where the translation applies.
  • Definition: The non-modal companion π(ϕ) replaces each □-subformula with rn →ϕ, using a fresh variable indexed by modal depth.This translation provides a non-modal representation of modal formulas for the appendix’s validity arguments.
  • Normality axiom: For the normality axiom K, validity on all frames would force every element of A to be idempotent, so K is generally invalid outside Heyting algebras.The non-modal companion makes this restriction explicit through the algebraic identity a = a ⊙a.
  • Rule generation: The method can derive modal principles from non-modal implications involving a common antecedent variable r.Proposition B.4 and Corollary B.5 formalize this transfer for monotone and expanding formulas.
  • Validity transfer: If a formula is valid on full frames, its non-modal companion is valid in Ac; analogous translations hold for idempotent and crisp frames with additional constraints.For idempotent frames the constraints enforce idempotence of rn, while crisp frames use substitutions into 0 and 1.
Loading 0811.2107v2…