Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Quantifier-free formulas and quantifier alternation depth in doctrines

Marco Abbadini, Francesca Guffanti

TL;DR

The paper integrates quantifier-free formulas and quantifier-alternation depth modulo a theory into a categorical framework of Boolean doctrines, using Lawvere-style hyperdoctrines. It defines a quantifier-free fragment and a QA-stratified Boolean doctrine, proving a tight equivalence between these two notions and relating them to first-order Boolean doctrines. A central result shows that, under a smallness assumption, quantifier-free fragments of FO doctrines are precisely Boolean doctrines, and that every Boolean doctrine embeds into its quantifier completion, yielding a universal construction $(\mathbf{P},\mathbf{P}^{\forall\exists})$ with a universal property. The treatment of equality via fibered equalities demonstrates that quantifier completion preserves elementary structure, and the framework is poised for a step-by-step, layer-by-layer description of quantifier addition. Overall, the work offers a principled, algebraic pathway to quantify the quantifier alternation hierarchy modulo a theory within a DOCTRINAL (Lawvere) setting, with potential for constructive layer-by-layer expansions and duality descriptions.

Abstract

This paper aims to incorporate the notion of quantifier-free formulas modulo a first-order theory and the stratification of formulas by quantifier alternation depth modulo a first-order theory into the algebraic treatment of classical first-order logic. The set of quantifier-free formulas modulo a theory is axiomatized by what we call a quantifier-free fragment of a Boolean doctrine with quantifiers. Rather than being an intrinsic notion, a quantifier-free fragment is an additional structure on a Boolean doctrine with quantifiers. Under a smallness assumption, the structures occurring as quantifier-free fragments of some Boolean doctrine with quantifiers are precisely the Boolean doctrines (without quantifiers). In particular, every Boolean doctrine over a small category is a quantifier-free fragment of its quantifier completion. Furthermore, the sequences obtained by stratifying an algebra of formulas by quantifier alternation depth modulo a theory are axiomatized by what we call QA-stratified Boolean doctrines. While quantifier-free fragments are defined in relation to an "ambient" Boolean doctrine with quantifiers, a QA-stratified Boolean doctrine requires no such ambient doctrine, and it consists of a sequence of Boolean doctrines (without quantifiers) with connecting axioms. QA-stratified Boolean doctrines are in one-to-one correspondence with pairs consisting of a Boolean doctrine with quantifiers and a quantifier-free fragment of it.

Quantifier-free formulas and quantifier alternation depth in doctrines

TL;DR

The paper integrates quantifier-free formulas and quantifier-alternation depth modulo a theory into a categorical framework of Boolean doctrines, using Lawvere-style hyperdoctrines. It defines a quantifier-free fragment and a QA-stratified Boolean doctrine, proving a tight equivalence between these two notions and relating them to first-order Boolean doctrines. A central result shows that, under a smallness assumption, quantifier-free fragments of FO doctrines are precisely Boolean doctrines, and that every Boolean doctrine embeds into its quantifier completion, yielding a universal construction with a universal property. The treatment of equality via fibered equalities demonstrates that quantifier completion preserves elementary structure, and the framework is poised for a step-by-step, layer-by-layer description of quantifier addition. Overall, the work offers a principled, algebraic pathway to quantify the quantifier alternation hierarchy modulo a theory within a DOCTRINAL (Lawvere) setting, with potential for constructive layer-by-layer expansions and duality descriptions.

Abstract

This paper aims to incorporate the notion of quantifier-free formulas modulo a first-order theory and the stratification of formulas by quantifier alternation depth modulo a first-order theory into the algebraic treatment of classical first-order logic. The set of quantifier-free formulas modulo a theory is axiomatized by what we call a quantifier-free fragment of a Boolean doctrine with quantifiers. Rather than being an intrinsic notion, a quantifier-free fragment is an additional structure on a Boolean doctrine with quantifiers. Under a smallness assumption, the structures occurring as quantifier-free fragments of some Boolean doctrine with quantifiers are precisely the Boolean doctrines (without quantifiers). In particular, every Boolean doctrine over a small category is a quantifier-free fragment of its quantifier completion. Furthermore, the sequences obtained by stratifying an algebra of formulas by quantifier alternation depth modulo a theory are axiomatized by what we call QA-stratified Boolean doctrines. While quantifier-free fragments are defined in relation to an "ambient" Boolean doctrine with quantifiers, a QA-stratified Boolean doctrine requires no such ambient doctrine, and it consists of a sequence of Boolean doctrines (without quantifiers) with connecting axioms. QA-stratified Boolean doctrines are in one-to-one correspondence with pairs consisting of a Boolean doctrine with quantifiers and a quantifier-free fragment of it.
Paper Structure (13 sections, 25 theorems, 54 equations)

This paper contains 13 sections, 25 theorems, 54 equations.

Table of Contents

  1. Introduction
  2. Preliminaries on doctrines
  3. Doctrines as many-sorted algebras
  4. The universal property of the syntactic doctrine
  5. Quantifier-free formulas and quantifier alternation depth for doctrines
  6. Quantifier-free fragments
  7. QA-stratified Boolean doctrines
  8. Boolean doctrines characterize quantifier-free fragments
  9. Quantifier completion of a Boolean doctrine
  10. The case with equality
  11. Future work
  12. Classical first-order sequent calculus (with contexts)
  13. A doctrine without a least quantifier-free fragment

Key Result

Theorem 2.13

Let $\mathcal{T}$ be a first-order theory in a language $(\mathbb{F},\bigcup_{n\in\mathbb{N}}\mathbb{P}_n)$, with $\mathbb{P}_n$ the set of $n$-ary predicate symbols, and $\mathbf{P}\colon\mathsf{Ctx}^{\mathrm{op}}\to\mathsf{BA}$ a first-order Boolean doctrine, where $\mathsf{Ctx}$ is the category o

Theorems & Definitions (95)

  • Definition 2.2: Boolean doctrine
  • Definition 2.3: Boolean doctrine morphism
  • Definition 2.4: First-order Boolean doctrine
  • Definition 2.5: First-order Boolean doctrine morphism
  • Remark 2.6: Universality is equivalent to existentiality
  • Example 2.7: Syntactic doctrine
  • Remark 2.8
  • Example 2.9: Subset doctrine
  • Definition 2.10
  • Remark 2.11: Boolean doctrines and first-order Boolean doctrines as many-sorted algebras
  • ...and 85 more