Freely adding one layer of quantifiers to a Boolean doctrine

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Abbadini, Marco, Guffanti, Francesca
Format: Preprint
Published: 2024
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866918177972158464
author Abbadini, Marco
Guffanti, Francesca
author_facet Abbadini, Marco
Guffanti, Francesca
contents We describe the layer of quantifier alternation depth at most one of the quantifier completion of a Boolean doctrine over a small category. This amounts to a doctrinal version of Herbrand's theorem for formulas with quantifier alternation depth at most one modulo a universal theory. The resulting construction satisfies a universal property that makes it the free QA-one-step Boolean doctrine. To achieve this version of Herbrand's theorem, we characterize, within the doctrinal setting, the classes $A$ of quantifier-free formulas for which there is a model $M$ such that $A$ is precisely the class of formulas whose universal closure is valid in $M$.
format Preprint
id arxiv_https___arxiv_org_abs_2410_16328
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Freely adding one layer of quantifiers to a Boolean doctrine
Abbadini, Marco
Guffanti, Francesca
Logic
Category Theory
Primary: 03G30. Secondary: 03B10, 18C10, 08B20
We describe the layer of quantifier alternation depth at most one of the quantifier completion of a Boolean doctrine over a small category. This amounts to a doctrinal version of Herbrand's theorem for formulas with quantifier alternation depth at most one modulo a universal theory. The resulting construction satisfies a universal property that makes it the free QA-one-step Boolean doctrine. To achieve this version of Herbrand's theorem, we characterize, within the doctrinal setting, the classes $A$ of quantifier-free formulas for which there is a model $M$ such that $A$ is precisely the class of formulas whose universal closure is valid in $M$.
title Freely adding one layer of quantifiers to a Boolean doctrine
topic Logic
Category Theory
Primary: 03G30. Secondary: 03B10, 18C10, 08B20
url https://arxiv.org/abs/2410.16328