PaperlayerView exact revision on arXiv

Source-linked AI summary

Quantified Multimodal Logics in Simple Type Theory

Christoph Benzmueller, Lawrence C. Paulson

arXiv:0905.2435v1cs.AIcs.LO

TL;DR

Quantified multimodal logic combines modal reasoning with quantification over individual and propositional variables, while simple type theory offers a well-understood semantic setting. The paper embeds these logics in simple type theory and proves soundness and completeness for QKπ semantics. It also identifies a boundary: weaker QKπ− models do not correspond naturally to Henkin models.

  • Problem

    The paper studies how quantified multimodal logics can be represented and analyzed within simple type theory, whose semantics are well understood.

    Source: §1 · p. 4, §3 · p. 10

  • Method

    It embeds quantified multimodal formulas as simple-type-theory terms, using a type for possible worlds and higher-order quantification.

    Source: §2.1 · p. 5, §3 · p. 10

  • Results

    The embedding is sound and complete for QKπ semantics, while weaker QKπ− models do not correspond to Henkin models.

    Source: §6 · p. 17

  • Takeaways & Limitations

    Normal multimodal logics can be viewed as fragments of simple type theory, and the embedding may help characterize computationally interesting fragments for proof tactics.

    Source: §6 · p. 17

    The proposal for higher-order modal logic does not yet address intensionality, and the authors identify scaling to more challenging problems as future work.

    Source: §5 · p. 16, §6 · p. 17

Abstract

from arXiv · show

We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of possible worlds. We present simple experiments, using existing higher-order theorem provers, to demonstrate that the embedding allows automated proofs of statements in these logics, as well as meta properties of them.

1 Motivation

Automated modal reasoning can use dedicated calculi or translate formulas into a logic with existing tools. This paper extends a simple-type-theory embedding to quantified multimodal logic, motivated by its semantic and automation possibilities.

1 Motivation

  • The translational approach transforms modal formulas into first-order logic for use with standard tools, unlike approaches that develop specific calculi and tools.Source: §1 · p. 4
  • The paper extends an embedding of multimodal logic in simple type theory to quantified multimodal logics, including quantification over propositional and first-order variables.The authors contrast their translational approach with Fitting’s work.Source: §1 · p. 4
  • Simple type theory’s established semantics can help study semantic issues, while its existing automated provers can be applied to quantified multimodal logics and their meta-properties.The authors also suggest that studying embeddings may identify computationally interesting fragments and inform proof tactics.Source: §1 · p. 4

2 Preliminaries

The preliminaries define simple type theory and the quantified multimodal logics considered in the paper, including their models, assignments, and validity.

2.1 Simple Type Theory

  • Simple type theory uses typed λ-terms built from constants and variables by abstraction and application, with connectives and quantification among its logical operators.The paper adds µ as a base type for possible worlds alongside o for Booleans and ι for individuals.Source: §2.1 · p. 5
  • Henkin semantics interprets typed terms over domains, with functions for function types and a valuation determined by the interpretation and variable assignment.Every term denotes, and terms equal under βη conversion have the same valuation.Source: §2.1 · p. 5

2.2 Quantified Multimodal Logic

  • The paper studies quantified multimodal logic over constant individual domains and the modal context K, rather than Fitting’s S5 structures.Its syntax includes predicate symbols, propositional variables, quantification, and multiple accessibility-indexed modal operators.Source: §2.2 · p. 6
  • A QKπ− model specifies worlds and accessibility relations, an individual domain, a propositional domain, and world-specific interpretations of relation symbols.Assignments map individual variables to domain elements and propositional variables to sets of worlds.Source: §2.2 · p. 6
  • Individual and propositional quantifiers range over their respective domains, while ✷r holds at a world when its formula holds at every r-accessible world.Source: §2.2 · p. 7
  • QKπ validity requires truth at every world and under every variable assignment in every model of the specified class.QKπ− and QKπ+ validity are defined analogously; QKπ+ models additionally require each world to belong to an atom of the propositional domain.Source: §2.2 · p. 7

3 Embedding Quantified Multimodal Logic in ST T

The embedding represents multimodal formulas as simple-type-theory terms evaluated over possible worlds, with modal and quantified operators defined as λ-terms. It supports theorem-prover reasoning through definitions and rewriting.

3 Embedding Quantified Multimodal Logic in ST T

  • The embedding represents individuals, truth values, and possible worlds using types ι, o, and µ, respectively, and modal formulas as terms of type µ → o.Negation, disjunction, and the box operator are defined as typed λ-terms over world-indexed formulas.Source: §3 · p. 8
  • Individual and propositional quantification are encoded with higher-order quantifiers over individuals and world-dependent propositions.The encoding also omits a restriction on subterms that the authors used in previous work; they state that this does not affect soundness or completeness.Source: §3 · p. 8
  • The paper notes that further operators, including difference, global modality, nominals, and @, could extend the embedding toward quantified hybrid logic.The authors identify such an extension as possible future work.Source: §3 · pp. 8–9
  • The QMLSTT-proposition grammar includes propositional variables, predicate applications, Boolean connectives, accessibility-indexed modalities, and both kinds of quantification.Source: §3 · p. 9
  • Because the operator definitions are simple type theory formulas, proof problems can be expressed in quantified multimodal syntax and reduced by rewriting to basic simple-type-theory connectives.The stated basic connectives include negation, disjunction, equality, and quantification over individuals and propositions.Source: §3 · p. 9

4 Soundness and Completeness of the Embedding

The embedding represents quantified multimodal logic in simple type theory and preserves validity in both directions for QKπ semantics. The paper proves this correspondence and extends the soundness and completeness results to several fragments.

4 Soundness and Completeness of the Embedding

  • Worlds, individuals, propositions, and accessibility relations are represented respectively by Dµ, Dι, Dµ→o, and typed world-pair predicates.The construction maps each QKπ model to a Henkin model.Source: §4 · pp. 11–12
  • Lemma 4.3 establishes that a QML formula is true at a world exactly when its translation evaluates to true there in the constructed Henkin model.This truth-preservation result is used to establish soundness.Source: §4 · pp. 11–12
  • If the translated proposition is valid in simple type theory, then the original proposition is QKπ-valid.The soundness proof uses the correspondence between QKπ models and Henkin models.Source: §4 · pp. 12–13
  • The reverse construction from Henkin models yields QKπ models, so QKπ-validity of a proposition implies validity of its translation in simple type theory.The construction first yields QKπ− models, and Lemma 4.8 establishes that these are also QKπ models.Source: §4 · pp. 13–14
  • The embedding is also sound and complete for propositional quantified, first-order, and propositional multimodal logic fragments.These fragments restrict quantification to propositional variables, individual variables, or disallow quantification, respectively.Source: §4 · p. 14

5 Applying the Embedding in Practice

Experiments apply off-the-shelf simple-type-theory reasoners to quantified multimodal logic examples and a meta-property. The reported outcomes include proofs, a model-finding result, and confirmation of constant-domain quantification.

5 Applying the Embedding in Practice

  • 0.6 seconds: IsabelleM found a model for the equations that LEO-II and IsabelleP tried to refute.IsabelleM uses the SAT solver zChaff.Source: §5 · p. 15
  • IsabelleP proved Example 3.5 in 1.0 seconds, LEO-II in 0.0 seconds, and TPS in 0.3 seconds; IsabelleM found no model.The passage reports that IsabelleM also found no model for the examples below.Source: §5 · p. 15
  • For BF and BF −1, IsabelleP proved the formulas in 0.7 seconds, LEO-II and LEO-IIP in 0.0 seconds, and TPS in 0.2 seconds.The authors say these results confirm that first-order quantification is constant domain.Source: §5 · p. 15
  • For the axiom and its (i, j, k, l)-confluence property, the reported results were IsabelleP: +/3.7, LEO-II: +/0.3, and TPS: +/0.2.The passage identifies these as results for the correspondence between the axiom and the confluence property.Source: §5 · p. 16

6 Conclusion

The embedding is sound and complete for QKπ semantics, and the paper distinguishes QKπ models from weaker QKπ− models. It presents quantified and non-quantified normal multimodal logics as fragments of simple type theory, while identifying further extensions as future work.

6 Conclusion

  • The embedding is sound and complete for QKπ semantics, but weaker QKπ− models do not correspond naturally to Henkin models.The paper formally explores the correspondence between QKπ models and Henkin models and reports that it does not hold for QKπ− models.Source: §6 · p. 17
  • Quantified and non-quantified normal multimodal logics can be treated as fragments of simple type theory, except for weak notions such as QKπ− models.Their semantics can be studied from the perspective of simple type theory’s well-understood semantics.Source: §6 · p. 17
  • The embedding may characterize computationally interesting fragments of simple type theory that could support powerful proof tactics for higher-order proof assistants.The paper presents this as a possible consequence, not a demonstrated result.Source: §6 · p. 17
  • Future work includes extending the embedding to quantified hybrid logics and full higher-order modal logics.A prior proposal toward higher-order modal logics does not yet address intensionality; combining it with non-extensional models for simple type theory is described as promising.Source: §6 · p. 17

A THF Formalization of Quantified Multi-Modal Logic in Simple Type Theory

The THF formalization defines quantified multimodal operators over possible worlds, including individual and propositional quantification, disjunction, box, and validity.

A THF Formalization of Quantified Multi-Modal Logic in Simple Type Theory

  • The formalization uses a base type mu and defines universal quantification over individuals and propositional variables at a world.The individual quantifier ranges over X of type mu; the proposition quantifier ranges over P of type $i > $o.Source: A THF Formalization of Quantified… · p. 21
  • Disjunction is defined by evaluating either proposition at the current world.The definition applies Phi and Psi to W and joins their truth values with disjunction.Source: A THF Formalization of Quantified… · p. 21
  • The box operator makes a proposition hold at every world accessible from the current world under relation R.Its definition quantifies over V and requires Phi at V whenever R relates W to V.Source: A THF Formalization of Quantified… · p. 21
  • Validity is defined by requiring the formula to hold at every possible world.The formalization universally quantifies over W.Source: A THF Formalization of Quantified… · p. 22

B THF Example: In all Worlds exists Truth

The example formalizes a conjecture that every world satisfies a box-modality claim involving existential propositional quantification over accessible worlds.

B THF Example: In all Worlds exists Truth

C THF Example: Confluence Property of Accessibility Relations

The example encodes an equivalence between a modal formula and a confluence property of four accessibility relations.

C THF Example: Confluence Property of Accessibility Relations

  • The conjecture equates the formula “◇i□jP implies □k◇lP” with confluence of relations i, j, k, and l.The passage defines the confluence property and states the equivalence as a conjecture.Source: C THF Example: Confluence Property of… · p. 24
Loading 0905.2435v1…