A Class of Generalised Quantifiers for k-Variable Logics

TL;DR

This paper introduces k-quantifier logics that extend traditional logical frameworks by allowing quantification over k-tuples, unifying various existing logics and establishing foundational theorems about their expressiveness and invariance.

Contribution

It defines a new class of k-quantifier logics, introduces bisimulation notions, and proves key theorems including Ehrenfeucht-Fraisse, Hennessy-Milner, and a Lindström-style characterization.

Findings

The framework encompasses k-variable fragments, modal logic, and neighborhood semantics.

Established bisimulation invariance and classical logical theorems for k-quantifier logics.

Characterized the maximal expressive power satisfying Los' theorem.

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.