Quantifier-free formulas and quantifier alternation depth in doctrines

Lawvere’s hyperdoctrines; Quantifier completion; Nested quantifiers; Quantifier-free fragment; Quantifier alternation depth; Algebraic logic; Categorical logic; First-order logic

Abstract :

[en] 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.

Disciplines :

Mathematics

Author, co-author :

Abbadini, Marco

GUFFANTI, Francesca ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > PCOG

External co-authors :

yes

Language :

English

Title :

Quantifier-free formulas and quantifier alternation depth in doctrines

Publication date :

2025

Journal title :

Journal of Pure and Applied Algebra

ISSN :

0022-4049

eISSN :

1873-1376

Publisher :

Elsevier, Netherlands

Peer reviewed :

Peer Reviewed verified by ORBi

Available on ORBilu :

since 13 March 2025

Statistics

Number of views

115 (1 by Unilu)

Number of downloads

141 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenAlex citations

Bibliography

Abbadini, M., Guffanti, F., Freely adding one layer of quantifiers to a Boolean doctrine. Preprint at https://arxiv.org/abs/2410.16328.
Adámek, J., Rosický, J., Vitale, E.M., A categorical introduction to general algebra. Algebraic Theories Cambridge Tracts in Mathematics, vol. 184, 2011, Cambridge University Press, Cambridge With a foreword by F. W. Lawvere.
Berta, C., Meloni, G., Dottrine con comprensione e logiche libere. Ferro, R., Zanardo, A., (eds.) Atti degli Incontri di Logica Matematica, vol. 3, 1987, 177–185.
Bezhanishvili, N., Gehrke, M., Finitely generated free Heyting algebras via Birkhoff duality and coalgebra. Log. Methods Comput. Sci., 2, 2011, 9.
Birkhoff, G., Lipson, J.D., Heterogeneous algebras. J. Comb. Theory 8 (1970), 115–133.
Cohen, R.S., Brzozowski, J.A., Dot-depth of star-free events. J. Comput. Syst. Sci. 5 (1971), 1–16.
Coumans, D.C.S., van Gool, S.J., On generalizing free algebras for a functor. J. Log. Comput. 23:3 (2013), 645–672.
Emmenegger, J., Pasquali, F., Rosolini, G., Elementary doctrines as coalgebras. J. Pure Appl. Algebra, 224, 2020.
Gehrke, M., Stone duality for logic with quantifiers. Invited talk at the conference “Category Theory 20→21”. Genoa, Italy. Recording of the talk available at: https://www.youtube.com/watch?v=yn5dH5fYWwY, 1 September 2021 Notes of the talk available at: https://drive.google.com/file/d/1YZY1etlrJehIneqAOVdkkkAT1CV7bFfq/view.
Gehrke, M., Jakl, T., Reggio, L., A Cook's tour of duality in logic: from quantifiers, through Vietoris, to measures. Samson Abramsky on Logic and Structure in Computer Science and Beyond Outst. Contrib. Log., vol. 25, 2023, Springer, Cham, 129–158.
Gehrke, Mai, Canonical extensions: an algebraic approach to stone duality. Algebra Univers., 79(3), 2018, 63.
Ghilardi, S., Free Heyting algebras as bi-Heyting algebras. C. R. Math. R. Acad. Sci. Can. 14:6 (1992), 240–244.
Ghilardi, S., An algebraic theory of normal forms. Ann. Pure Appl. Log. 71:3 (1995), 189–245.
Ghilardi, S., Continuity, freeness, and filtrations. J. Appl. Non-Class. Log. 20:3 (2010), 193–217.
Halmos, P.R., Algebraic logic. II. Homogeneous locally finite polyadic Boolean algebras of infinite degree. Fundam. Math. 43 (1956), 255–325.
Henkin, L., Monk, J.D., Tarski, A., Cylindric Algebras. Part I. With an introductory chapter: General theory of algebras Studies in Logic and the Foundations of Mathematics, vol. 64, 1971, North-Holland Publishing Co., Amsterdam-London.
Higgins, P.J., Algebras with a scheme of operators. Math. Nachr. 27 (1963), 115–132.
Hofstra, P.J.W., All realizability is relative. Math. Proc. Camb. Philos. Soc. 141:2 (2006), 239–264.
Joyal, A., Polyadic spaces and elementary theories. Not. Am. Math. Soc., 18(3), 1971, 563.
Lambek, J., Scott, P.J., Introduction to Higher-Order Categorical Logic, vol. 7. 1988, Cambridge University Press.
Lawvere, F.W., Adjointness in foundations. Dialectica 23:3/4 (1969), 281–296.
Lawvere, F.W., Equality in hyperdoctrines and comprehension schema as an adjoint functor. Appl. Categ. Algebr. 17 (1970), 1–14.
Maietti, M., Rosolini, G., Elementary quotient completion. Theory Appl. Categ., 27, 2013.
Maietti, M., Rosolini, G., Unifying exact completions. Appl. Categ. Struct. 23:1 (2015), 43–52.
Maietti, M.E., Pasquali, F., Rosolini, G., Triposes, exact completions, and Hilbert's ε-operator. Tbil. Math. J. 10:3 (2017), 141–166.
Maietti, M.E., Rosolini, G., Quotient completion for the foundation of constructive mathematics. Log. Univers. 7:3 (2013), 371–402.
Maietti, M.E., Trotta, D., A characterization of generalized existential completions. Ann. Pure Appl. Log., 174(4), 2023, 37 No. 103234.
Marquès, J., Categorical logic from the perspective of duality and compact ordered spaces. PhD thesis, 2023, Université Côte d'Azur.
nLab, authors, Sequent calculus. Accessed online on the 7th of February 2025 from. https://ncatlab.org/nlab/show/sequent+calculus.
Pasquali, F., A co-free construction for elementary doctrines. Appl. Categ. Struct. 23:1 (2015), 29–41.
Straubing, H., A generalization of the Schützenberger product of finite monoids. Theor. Comput. Sci. 13:2 (1981), 137–150.
Tarlecki, A., Some nuances of many-sorted universal algebra: a review. Bull. Eur. Assoc. Theor. Comput. Sci. 104 (2011), 89–111.
Thérien, D., Classification of finite monoids: the language approach. Theor. Comput. Sci. 14:2 (1981), 195–208.
Trotta, D., The existential completion. Theory Appl. Categ. 35 (2020), 1576–1607 Paper No. 43.
van Gool, S., Marquès, J., On duality and model theory for polyadic spaces. Ann. Pure Appl. Log., 175(2), 2024, 50 Paper No. 103388.
Wechler, W., Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science., vol. 25, 1992, Springer-Verlag, Berlin.