Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Finitely accessible arboreal adjunctions and Hintikka formulae

Luca Reggio, Colin Riba

TL;DR

This work develops a general framework linking back-and-forth model comparison games to Hintikka-style formulae within finitely accessible wooded (and arboreal) adjunctions. By leveraging Gabriel–Ulmer duality and Hodges’ word-constructions, it shows that the ordinal ranks of back-and-forth positions are definable by Hintikka formulae, yielding that $\mathscr{L}_{\infty}$-equivalence on the extensional side cannot be distinguished by arboreal back-and-forth relations. The main theorem establishes a converse-type bound: under mild definability/detectability assumptions for path embeddings, $\mathscr{L}_{\infty}$-equivalence implies $R$-back-and-forth equivalence for a finite, locally presentable adjunction. The paper also develops a robust repertoire of embeddings/formulae in a variety of wooded/arboreal settings, and discusses the factorisation property, with applications to EF, pebble, modal, and hybrid tree-like games, outlining pathways to guarded logics and beyond.

Abstract

Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions. In many cases, equivalence of structures in fragments of infinitary first-order logic can be captured by transferring the bisimilarity relation along the adjunction. In most applications, the categories involved are locally finitely presentable and the adjunctions are finitely accessible. Our main result identifies the expressive power of this class of adjunctions. We show that the ranks of back-and-forth games in the arboreal category are definable by formulae à la Hintikka, and thus the relation between extensional objects induced by bisimilarity is always coarser than equivalence in infinitary first-order logic. Our approach leverages Gabriel-Ulmer duality for locally finitely presentable categories, and Hodges' word-constructions.

Finitely accessible arboreal adjunctions and Hintikka formulae

TL;DR

This work develops a general framework linking back-and-forth model comparison games to Hintikka-style formulae within finitely accessible wooded (and arboreal) adjunctions. By leveraging Gabriel–Ulmer duality and Hodges’ word-constructions, it shows that the ordinal ranks of back-and-forth positions are definable by Hintikka formulae, yielding that -equivalence on the extensional side cannot be distinguished by arboreal back-and-forth relations. The main theorem establishes a converse-type bound: under mild definability/detectability assumptions for path embeddings, -equivalence implies -back-and-forth equivalence for a finite, locally presentable adjunction. The paper also develops a robust repertoire of embeddings/formulae in a variety of wooded/arboreal settings, and discusses the factorisation property, with applications to EF, pebble, modal, and hybrid tree-like games, outlining pathways to guarded logics and beyond.

Abstract

Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions. In many cases, equivalence of structures in fragments of infinitary first-order logic can be captured by transferring the bisimilarity relation along the adjunction. In most applications, the categories involved are locally finitely presentable and the adjunctions are finitely accessible. Our main result identifies the expressive power of this class of adjunctions. We show that the ranks of back-and-forth games in the arboreal category are definable by formulae à la Hintikka, and thus the relation between extensional objects induced by bisimilarity is always coarser than equivalence in infinitary first-order logic. Our approach leverages Gabriel-Ulmer duality for locally finitely presentable categories, and Hodges' word-constructions.
Paper Structure (53 sections, 52 theorems, 140 equations, 3 figures)

This paper contains 53 sections, 52 theorems, 140 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Structures and infinitary first-order logic
  4. Cartesian theories
  5. Locally finitely presentable categories
  6. Factorisation systems
  7. Back-and-forth equivalence
  8. From concrete to abstract model comparison games
  9. Positions as pairs of embeddings
  10. Plays as structures
  11. Wooded categories and back-and-forth equivalence
  12. Paths and wooded categories
  13. Back-and-forth games in wooded categories
  14. Wooded adjunctions and $R$-equivalence
  15. Finitely accessible wooded adjunctions
  16. ...and 38 more sections

Key Result

Lemma 2.10

Let $\mathop{\mathrm{\mathscr{E}}}\nolimits$ be a cocomplete locally small category. If $\mathop{\mathrm{\mathscr{E}}}\nolimits$ admits an (essentially) small full dense subcategory $\mathscr{K}$ consisting of finitely presentable objects, then $\mathop{\mathrm{\mathscr{E}}}\nolimits$ is lfp.

Figures (3)

  • Figure 1: Hintikka formulae for the wooded category $\mathop{\mathrm{\mathscr{C}}}\nolimits$ (§\ref{['sec:hintikka:form']}).
  • Figure 2: Formulae for $\mathit{At}$-reflecting homomorphisms with finitely presentable domains (Corollary \ref{['cor:formemb']}).
  • Figure 3: Formulae for monomorphisms (Proposition \ref{['prop:emb:presh:fp-domain']}).

Theorems & Definitions (214)

  • Definition 2.1: Cartesian theory
  • Remark 2.2
  • Example 2.3: Cartesian theories of functors
  • Example 2.4
  • Remark 2.5
  • Definition 2.6
  • Example 2.7
  • Remark 2.9
  • Lemma 2.10
  • Example 2.11
  • ...and 204 more