Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Class of Generalised Quantifiers for k-Variable Logics

Janek Härtter, Martin Otto

TL;DR

This work develops a framework of $k$-quantifier logics that quantify over $k$-tuples through flexible witness sets, unifying FO$^k$, modal, and neighbourhood-style logics. It builds a robust meta-theory: (i) a natural $\mathcal{L}^{\mathcal{Q}}$-bisimulation notion and two back-and-forth games, (ii) an Ehrenfeucht–Fraïssé theorem linking $q$-rank indistinguishability to $\sim_{\mathcal{L}^{\mathcal{Q}}}^q$-bisimilarity, and (iii) a Hennessy–Milner theorem under saturation, ensuring equivalence implies bisimilarity in suitable models. The Łoś property is shown to constrain these logics to be fragments of first-order logic, and a Lindström-style maximality theorem is established for $\mathcal{L}^{\mathcal{Q}}$, yielding a uniform translation to FO and a principled maximality characterization. Overall, the paper advances a principled, highly expressive yet controlled family of logics with potential applications to modal, neighbourhood, and related relational semantics, while highlighting remaining open questions about weakening assumptions and further connections to established semantic frameworks.

Abstract

We introduce k-quantifier logics -- logics with access to k-tuples of elements and very general quantification patterns for transitions between k-tuples. The framework is very expressive and encompasses e.g. the k-variable fragments of first-order logic, modal logic, and monotone neighbourhood semantics. We introduce a corresponding notion of bisimulation and prove variants of the classical Ehrenfeucht-Fraisse and Hennessy-Milner theorem. Finally, we show a Lindstrom-style characterisation for k-quantifier logics that satisfy Los' theorem by proving that they are the unique maximally expressive logics that satisfy Los' theorem and are invariant under the associated bisimulation relations.

A Class of Generalised Quantifiers for k-Variable Logics

TL;DR

This work develops a framework of -quantifier logics that quantify over -tuples through flexible witness sets, unifying FO, modal, and neighbourhood-style logics. It builds a robust meta-theory: (i) a natural -bisimulation notion and two back-and-forth games, (ii) an Ehrenfeucht–Fraïssé theorem linking -rank indistinguishability to -bisimilarity, and (iii) a Hennessy–Milner theorem under saturation, ensuring equivalence implies bisimilarity in suitable models. The Łoś property is shown to constrain these logics to be fragments of first-order logic, and a Lindström-style maximality theorem is established for , yielding a uniform translation to FO and a principled maximality characterization. Overall, the paper advances a principled, highly expressive yet controlled family of logics with potential applications to modal, neighbourhood, and related relational semantics, while highlighting remaining open questions about weakening assumptions and further connections to established semantic frameworks.

Abstract

We introduce k-quantifier logics -- logics with access to k-tuples of elements and very general quantification patterns for transitions between k-tuples. The framework is very expressive and encompasses e.g. the k-variable fragments of first-order logic, modal logic, and monotone neighbourhood semantics. We introduce a corresponding notion of bisimulation and prove variants of the classical Ehrenfeucht-Fraisse and Hennessy-Milner theorem. Finally, we show a Lindstrom-style characterisation for k-quantifier logics that satisfy Los' theorem by proving that they are the unique maximally expressive logics that satisfy Los' theorem and are invariant under the associated bisimulation relations.
Paper Structure (8 sections, 14 theorems, 39 equations, 1 figure)

This paper contains 8 sections, 14 theorems, 39 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Abstract $k$-Logics
  3. Bisimulation
  4. An Ehrenfeucht--Fraïssé Theorem
  5. A Hennessy--Milner Theorem
  6. The Łoś Property and First-Order Logic
  7. A Lindström theorem
  8. Summary and Outlook

Key Result

Theorem 4.1

Let $\sigma$ be a finite signature and $\mathcal{L} :=\mathcal{L}^{\mathcal{Q}}$ a $k$-quantifier logic with finitely many quantifiers in $\mathcal{Q}_{\sigma}$. For any $q \in \mathbb{N}$ and pair of pointed $\sigma$-structures $(\mathfrak{A}, \alpha)$, $(\mathfrak{B}, \beta)$, the following are eq

Figures (1)

  • Figure 1: The structures $(\mathfrak{A}, a)$ and $(\mathfrak{B}, b)$ have the same $\operatorname{ML}$-theory, but they are not $\operatorname{ML}$-bisimilar.

Theorems & Definitions (40)

  • Definition 2.1: abstract logics
  • Definition 2.2: $k$-quantifiers
  • Definition 2.3: $k$-quantifier logics
  • Definition 2.5: quantifier rank
  • Definition 2.6: $\mathcal{L}^{\mathcal{Q}}$-elementary equivalence
  • Definition 2.7: $\mathcal{L}$-theories
  • Example 2.8: modal quantifiers as 1-quantifiers
  • Example 2.9: monotonic neighbourhood semantics versus $1$-quantifiers
  • Example 2.10: first-order and counting quantifiers
  • Definition 3.1: $\mathcal{L}^{\mathcal{Q}}$-bisimulation
  • ...and 30 more