Algebraizing first-order logics

JUNIOR STAR - GACR GM26-23128M [Registered results] 2026 - 2030

Principal Investigator: Mgr. Adam Přenosil, Ph.D.

The last 50 years saw the introduction of many logical systems going beyond clasical two-valued logic, with motivations coming from fields such as computer science, philosophy, game theory, and linguistics. In response to this multitude of logics, a general algebraic theory of non-classical propositional logics called abstract algebraic logic (AAL) was gradually developed.

However, no satisfactory algebraic theory of comparable strength and generality exists at the first-order level. The main reason is that first-order quantifiers are cumbersome to handle using the standard methods of universal algebra.

The aim of the project is to develop such a general theory by combining the methods of AAL with an analysis of quantification based on so-called nominal algebras, and to apply this theory to settle open questions about interpolation and Beth definability in non-classical first-order logics. Algebraizing first-order quantification in this way will also enable us to apply profinite methods from algebraic automata theory in the finite model theory of classical and non-classical logics.