Marco Abbadini (University of Birmingham) will give a talk on
Quantifier-free fragments and quantifier alternation depth in Boolean doctrines
Abstract:
Step-by-step methods in algebraic logic are used to get results on the Lindenbaum-Tarski algebras with an induction on the depth of nesting of the “difficult’’ logical symbols; e.g. implications in intuitionistic propositional logic, or modalities in propositional modal logic. Step-by-step methods can be used to construct algebras satisfying a given specification in a piece-by-piece manner, understand free algebras as directed colimits of simpler partial algebras, get decidability results and normal forms.
Some of the main developments of step-by-step methods have been in intuitionistic propositional logic and propositional modal logic, where “step-by-step” refers to nesting of implications and modalities, respectively.
Our aim is to extend this approach to classical first-order logic, with “step-by-step” referring to nestings of quantifiers. This means understanding the Lindenbaum-Tarski algebras made up of only those formulas whose quantifier alternation depth is less than or equal to a fixed natural number, and understanding how to freely add one layer of quantifier alternation to such an algebra. I will present the first steps towards this aim.
This talk is based on a joint work with Francesca Guffanti.