ABSTRACT. Extensional ESO is a fragment of existential second-order logic (ESO) that captures the following family of problems. Given a fixed ESO sentence $\Psi$ and an input structure $\mathbb A$ the task is to decide whether there is an \emph{extension} $\mathbb B$ of $\mathbb A$ that satisfies the first-order part of $\Psi$, i.e., a structure ${\mathbb B}$ such that $R^{\mathbb A}\subseteq R^{\mathbb B}$ for every existentially quantified predicate $R$ of $\Psi$, and $R^{\mathbb A} = R^{\mathbb B}$ for every non-quantified predicate $R$ of $\Psi$. In particular, extensional ESO describes all pre-coloured finite-domain constraint satisfaction problems (CSPs). In this paper we study the computational power of extensional ESO; we ask, \emph{for which problems in NP is there a polynomial-time equivalent problem in extensional ESO?} One of our main results states that extensional ESO has the same computational power as \emph{hereditary first-order logic}. We also characterize the computational power of the fragment of extensional ESO with monotone universal first-order part in terms of finitely bounded CSPs. These results suggest a rich computational power of this logic, and we conjecture that extensional ESO captures NP-intermediate problems. We further support this conjecture by showing that extensional ESO can express current candidate NP-intermediate problems such as Graph Isomorphism, and Monotone Dualization (up to polynomial-time equivalence). On the other hand, another main result proves that extensional ESO does not have the full computational power of NP: there are problems in NP that are not polynomial-time equivalent to a problem in extensional ESP (unless E=NE).

ABSTRACT. The logic MMSNP is a well-studied fragment of Existential Second- Order logic that, from a computational perspective, captures ex- actly finite-domain Constraint Satisfaction Problems (CSPs) modulo polynomial-time reductions. At the same time, MMSNP contains many problems that are expressible as 𝜔-categorical CSPs but not as finite-domain ones. We initiate the study of Promise MMSNP (PMMSNP), a promise analogue of MMSNP. We show that every PMMSNP problem is poly- time equivalent to a (finite-domain) Promise CSP (PCSP), thereby extending the classical MMSNP-CSP correspondence to the promise setting. We then investigate the complexity of PMMSNPs aris- ing from forbidding monochromatic cliques, a class encompassing promise graph colouring problems. For this class, we obtain a full complexity classification conditional on the Rich 2-to-1 Conjecture, a recently proposed perfect-completeness surrogate of the Unique Games Conjecture. As a key intermediate step which may be of independent interest, we prove that it is NP-hard (under the Rich 2-to-1 Conjecture) to properly colour a uniform hypergraph even if it is promised to admit a colouring satisfying certain technical conditions. This proof is an extension of the recent work of Braverman, Khot, Lifshitz and Minzer (Adv. Math. 2025). To illustrate the broad applicability of this theorem, we show that it implies most of the linearly-ordered colouring conjecture of Barto, Battistelli, and Berg (STACS ’21).

ABSTRACT. The Bodirsky-Pinsker conjecture asserts a P vs. NP-complete dichotomy for the computational complexity of Constraint Satisfaction Problems (CSPs) of first-order reducts of finitely bounded homogeneous structures. Prominently, two structures in the scope of the conjecture have log-space equivalent CSPs if they are pp-bi-interpretable, or equivalently, if their polymorphism clones are topologically isomorphic. The latter gives rise to the algebraic approach which regards structures with topologically isomorphic polymorphism clones as equivalent and seeks to identify structural reasons for hardness or tractability in topological clones. We establish that the equivalence relation of pp-bi-interpretability underlying this approach is reasonable: On the one hand, we show that it is decidable under mild conditions on the templates; this improves a theorem of Bodirsky, Pinsker and Tsankov (LICS'11) on decidability of equality of polymorphism clones. On the other hand, we show that within the much larger class of transitive $\omega$-categorical structures without algebraicity, the equivalence relation is of lowest possible complexity in terms of descriptive set theory: namely, it is smooth, i.e., Borel-reduces to equality on the real numbers. On our way to showing the first result, we establish that the model-complete core of a structure that has a finitely bounded Ramsey expansion (which might include all structures of the Bodirsky-Pinsker conjecture) is computable, thereby providing a constructive alternative to previous non-constructive proofs of its existence.

ABSTRACT. In this paper, we propose a unifying algebraic framework which allows us to connect circuit complexity classes to the properties of finite algebraic structures. Our work is inspired by branching programs and nonuniform deterministic automata introduced by Barrington, as well as by their generalization proposed by Idziak et al. In particular, we characterize language classes recognized by circuits over simple algebras and over algebras from congruence modular varieties.

ABSTRACT. Simplicial type theory (STT) was introduced by Riehl and Shulman to leverage homotopy type theory to prove results about $(\infty,1)$-categories. Initial work on simplicial type theory focused on "formal" arguments in higher category theory and, in particular, no non-trivial examples of $\infty$-category theory were constructible within STT. More recent work has changed this state of affairs by applying techniques developed initial for cubical type theory to construct the $\infty$-category of spaces. We complete this process by constructing the $\infty$-category of $\infty$-categories, recovering one of the main foundational results of $\infty$-category theory (straightening--unstraightening) purely type-theoretically. We also show how this construction enables new examples of the directed version of the structure identity principle, the structure homomorphism principle.

ABSTRACT. In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable, or undecidable". We work in homotopy type theory and use Brouwer ordinals to specify the level of decidability of a property. In this framework, we express the property that a proposition is α-decidable, for a Brouwer ordinal α, and show that it generalizes decidability and semidecidability. Further generalizing known results, we show that α-decidable propositions are closed under binary conjunction, and discuss for which α they are closed under binary disjunction. We prove that if each P(i) is semidecidable, then the countable meet ∀i∈ℕ.P(i) is ω²-decidable, and similar results for countable joins and iterated quantifiers. We also discuss the relationship with countable choice. All our results are formalized in cubical Agda.

ABSTRACT. Cubical type theories are designed around an abstract unit interval from which types of paths are defined; varying the operations available on this interval yields different type theories. A reversal is an involutive unary operator on the interval that swaps its two endpoints. We show that for cubical type theories with self-dual interval theories, such as the minimal theory of two endpoints or the theory of a bounded distributive lattice, the extension of the theory with a reversal that internalizes the duality is a conservative extension. The key observation is that the product of an interval and its dual is again an interval with a reversal given by swapping coordinates. Our conservativity result applies to "idealized" cubical type theories without equations for evaluating the filling operator at concrete type formers. Using the same basic observation, however, we also construct models of full cubical type theories with reversals in categories of cubical sets without reversals. In so doing, we give the first models of these theories whose homotopy theory corresponds to that of topological spaces.

ABSTRACT. We give a new syntax-independent account of finitely-presented generalized algebraic theories (GATs) as finite cell complexes in the category of categories with families (CwFs), in which GATs are constructed by successive pushouts along the CwF morphisms generically postulating a sort, an operation, or an equation. Inspired by the fat small object argument of Makkai, Rosick\'{y}, and Vok\v{r}\'{i}nek, we introduce fat GAT presentations, thereby allowing infinite presentations with non-linear dependency structure. Then, motivated by wanting our GATs to self-describe, we extend presentations to admit infinitary arities, including infinitely deep dependency chains. Finally, we verify that these generalized GATs satisfy expected semantic properties including Frey's Gabriel–Ulmer duality.

ABSTRACT. We start a systematic investigation of the size of Craig interpolants, uniform interpolants, and strongest implicates for (quasi-)normal modal logics. Our main upper bound states that for tabular modal logics, the computation of strongest implicates can be reduced in polynomial time to uniform interpolant computation in classical propositional logic. Hence they are of polynomial dag-size iff NP is included P/poly. The reduction also holds for Craig interpolants if the tabular modal logic has the Craig interpolation property. Our main lower bound shows an unconditional exponential lower bound on the size of Craig interpolants and strongest implicates covering almost all non-tabular standard normal modal logics. For normal modal logics contained in or containing S4 or Goedel-Loeb logic GL we obtain the following dichotomy: tabular logics have "propositionally sized" interpolants while for non-tabular logics an unconditional exponential lower bound holds.

ABSTRACT. Recent research has established complexity results for the problem of deciding the existence of interpolants in logics lacking the Craig Interpolation Property (CIP). The proof techniques developed so far are non-constructive, and no meaningful bounds on the size of interpolants are known. Hybrid modal logics (or modal logics with nominals) are a particularly interesting class of logics without CIP: in their case, CIP cannot be restored without sacrificing decidability and, in applications, interpolants in these logics can serve as definite descriptions and separators between positive and negative data examples in description logic knowledge bases. In this contribution we show, using a new hypermosaic elimination technique, that in many standard hybrid modal logics Craig interpolants can be computed in quadruple exponential time, if they exist. On the other hand, we show that the existence of uniform interpolants is undecidable, which is in stark contrast to modal or intuitionistic logic where uniform interpolants always exist.

ABSTRACT. We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following reductions: (i) a polynomial-time reduction from the satisfiability problem for GNTC to the satisfiability problem for the unary negation fragment UNTC of GNTC, and (ii) a direct exponential-time reduction from the satisfiability problem for UNTC to the non-emptiness problem for 2-way alternating parity tree automata. Furthermore, we show that the model checking problem for GNTC is $P^{NP[O(log^2 n)]}$-complete in combined complexity. Our result implies $P^{NP[O(log^2 n)]}$-completeness for both UNTC and UNFO^{reg}, which were left open in previous works.

ABSTRACT. We study the Guarded Fragment of first-order logic over models that interpret a family of distinguished binary predicates $E_1,E_2,\dots$ as nested equivalence relations, that is, such that $E_{k+1}$ is coarser than $E_k$ for all $k \geq 1$. We show that the equality-free Guarded Fragment with nested equivalence relations retains the finite model property and that its satisfiability problem is decidable, albeit of non-elementary complexity. When the number of distinguished predicates is fixed to~$K$, the complexity becomes $(K{+}2)$-\ExpTime{}-complete. In contrast, we show that decidability is lost as soon as the nesting condition is dropped or equality is admitted.

ABSTRACT. There have recently been several developments in synthetic mathematics, using extensions of dependent type theory with univalence: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. The goal of this paper is to provide a foundation of constructive higher sheaf models of type theory in a constructive meta theory, and in particular, to build constructive models of these formal systems. The main technical tools are the use of internal language for simplifying proofs of intermediate lemmas and the notion of descent data operations, which already played an important role in models of directed univalence. Even classically, we think this work can be interesting, since these models are developed in a proof theoretically weak meta theory (in particular it is predicative).

ABSTRACT. Under the homotopy hypothesis, higher dimensional groups are defined as pointed homotopy types whose homotopy groups vanish outside a certain range. In particular, a 2-group is a pointed connected homotopy 2-type. Classically, 2-groups have two equivalent algebraic descriptions: one in terms of weak monoidal categories and the other in terms of group cohomology. We present these two classifications of pointed connected 2-types in homotopy type theory, thereby providing internal, constructive counterparts to the traditional classifications of 2-groups. Our first classification (in terms of monoidal categories) takes the form of a bicategorical equivalence, while our second is a type equivalence that extends to n-groups for all n >= 2. We have mechanized our results in Agda.

ABSTRACT. In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Due to their good categorical properties, CW complexes have become the main object of interest in algebraic topology. Although their quasi-combinatorial nature suggests that a constructive treatment is possible, there seems to be little literature on the subject -- perhaps because of the important role played by the axiom of choice in the classical theory of CW complexes. In this paper, we present a synthetic and constructive account of the theory of CW complexes in homotopy type theory. Our first main result is a finitary version of the cellular approximation theorem which, among other things, allows us to construct a cellular homology functor without needing the axiom of choice or relying on a pre-existing notion of homology. Our second main result is a theorem (the `Hurewicz approximation theorem') which shows that a classical definition of $n$-connected CW complexes agrees with the, in HoTT, usual definition of $n$-connected types -- a theorem which is far from obvious from a constructive point of view. As a corollary, we give a new proof of the Hurewicz theorem for CW complexes, which relates the first non-vanishing homotopy group of a CW complex with the corresponding homology group. All key theorems presented in this paper have been mechanised in Cubical Agda.

ABSTRACT. Few constructions in mathematics are as elusive as the homotopy groups of spheres. These groups, which intuitively measure n-dimensional loops on m-dimensional spheres, appear to be almost completely random---an unfortunate fact, seeing as they constitute one of the fundamental building blocks of algebraic topology and homotopy theory. However, the situation is not completely hopeless: in 1953, Serre proved his celebrated finiteness theorem, which says that these groups are almost always finite abelian groups, except in two classes of special cases when they also contain copies of the integers. In a recent paper, Barton and Campion proved a variation of this result in homotopy type theory (HoTT)---an extension of Martin-Löf type theory, particularly suitable for reasoning about and formalising algebraic topology and homotopy theory. Their result shows that the homotopy groups of spheres are all finitely presented -- and constructively so. Prior to this proof, HoTT had only had been used to compute low-dimensional homotopy groups of spheres. This made it a major breakthrough for HoTT as a foundation and, as such, the immediate target of a full-scale formalisation project. In this paper, we present the outcome of this project: a complete formalisation of Barton and Campion's proof of the Serre finiteness theorem in Cubical Agda, a constructive proof assistant implementing a cubical flavor of HoTT. In the light of the constructivity of Cubical Agda, we discuss the prospect of running the algorithm provided by our formalisation in order to compute concrete homotopy groups of spheres.

ABSTRACT. Fixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructions (AIC) - a purely algebraic approach to reasoning about fixed point iterations of continuous endomaps on complete lattices. AIC allows derivations of constructive fixed point theorems via equational logic and avoids explicit computations with indices. We demonstrate the applicability of AIC by providing algebraic proofs of several well- and less-well-known fixed point theorems: Among others, we prove the Tarski-Kantorovich principle - a generalization of the Kleene fixed point theorem - as well as a fixed point-theoretic generalization of $k$-induction, which is used in software verification. We moreover improve upon a recent generalization of the Tarski-Kantorovich principle due to Olszewski for obtaining pre- and postfixed points from lattice-theoretic limit inferiors and limit superiors of suitably seeded fixed point iterations: We identify sufficient continuity conditions on the endomaps so that these limits become proper fixed points. We have mechanized our algebra in Isabelle/HOL. Isabelle's sledgehammer tool is able to find proofs of the above fixed point theorems fully automatically. Finally, we investigate the completeness of our axiomatization of AIC. We prove that our finite set of finitary axioms is (a) sound but incomplete for standard models of AIC (sequences of elements from a complete lattice) and that (b) a different finite set of infinitary axioms is complete. We also prove that infinitary axioms are unavoidable: there exists no finite complete axiomatization of sequence models given by finitary axioms.

ABSTRACT. We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. In particular, we focus on the question of which formal theories and proof systems can efficiently prove algebraic circuit lower bounds, as follows. - **Formalization of Rank Method** Typically, algebraic circuit lower bounds are shown using the ``rank method", i.e., by exploiting non-trivial upper bounds on the rank of matrices derived from the monomial coefficients of polynomials computable by small algebraic circuits. A recent prominent application of this method is in the constant-depth algebraic circuit lower bounds by Limaye, Srinivasan and Tavenas~\cite{LST25} for the determinant and iterated matrix multiplication over fields of characteristic zero, and the finite field analogue of these results by Forbes~\cite{For24}. We show that these rank-based arguments can be formalized in the bounded arithmetic theory VNC2, which captures ``reasoning with NC2 concepts''. This complements the work of Tzameret and Cook \cite{TC21}, who showed that basic structural \emph{upper} bounds in algebraic circuit complexity can be formalized in \VNCTwo. Moreover, it offers a unified proof-theoretic framework in which to formulate and study barriers for current algebraic complexity methods (complementing specific barriers discovered by Efremenko, Garg, Oliveira, and Wigderson~\cite{EGOW18} and Garg, Makam, Oliveira, and Wigderson~\cite{GMOW19}). - **Unconditional PCR lower bounds** We show that Polynomial Calculus Resolution PCR cannot efficiently prove superpolynomial algebraic circuit lower bounds for any family of polynomials. Moreover, PCR cannot efficiently prove exponential constant-depth circuit lower bounds for any family of polynomials. - **Conditional constant-depth IPS lower bounds** We introduce the Tensor Rank Principle and demonstrate it is hard for PCR. We show that if this principle is hard against constant-depth Ideal Proof System IPS then constant-depth IPS cannot efficiently prove constant-depth algebraic circuit lower bounds.

ABSTRACT. Dynamical systems provide rigorous models of movement or evolution over time. Due to their abstract nature, they may be naturally employed for modelling e.g. physical, biological, or financial phenomena. Specifically in the context of Computer Science, computational processes, machine learning algorithms, and multi-agent systems may be regarded as dynamical systems. This wide range of applicability has sparked interest in designing formal specification languages for dynamical systems which may be amenable to automated or computer-assisted deduction, leading to the introduction of *dynamic topological logic* (DTL). When space is continuous but time is discrete, it is known that a sound and complete deductive calculus for DTL exists. However, discrete spaces are oftentimes more suitable for representing phenomena arising from CS, and in this setting, whether such a calculus exists even in principle has been an open question for more than two decades. More precisely, it was unknown whether the DTL of Alexandrov spaces is computably enumerable. In this paper, we use model-search techniques to provide an affirmative answer.

ABSTRACT. A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates---used to establish semantic termination arguments---to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, and two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof term constructed in the definitional variant of the theory can be soundly embedded into the propositional variant, while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.

ABSTRACT. Motivated by applications in computable analysis, we study fixpoints of certain endofunctors over categories of containers. More specifically, we focus on fibred endofunctors over the fibrewise opposite of the codomain fibration that can be themselves be represented by families of polynomial endofunctors. In this setting, we show how to compute initial algebras, terminal coalgebras and another kind of fixpoint $\zeta$. We then explore a number of examples of derived operators inspired by Weihrauch complexity and the usual construction of the free polynomial monad. We introduce $\zeta$-expressions as the syntax of $\mu$-bicomplete categories, extended with $\zeta$-binders and parallel products, which thus have a natural denotation in containers. By interpreting certain $\zeta$-expressions in a category of type-2 computable maps, we are able to capture a number of meaningful Weihrauch degrees, ranging from closed choice on $\{0,1\}$ to determinacy of infinite parity games, via an ``answerable part'' operator.

ABSTRACT. Completeness and representation theorems in abstract algebra, lattice theory, and theoretical computer science are tied to the existence of ideal objects, and thus to transfinite methods such as Zorn's lemma. Yet many concrete uses of such theorems appeal to finite approximations only, which carry a clear computational meaning. In this paper, we introduce co-coverages on complete lattices as a uniform way to specify ideal elements, and associate to each co-coverage a canonical closure operator with a folding property reminiscent of the covering principles at work in constructive algebra. This yields finitary, choice-free alternatives for arguments in which ideal objects are employed to reduce a computational problem to subcases. In a classical setting, our closure operators admit bases which allow to recover a host of primality principles such as the universal Krull–Lindenbaum theorem and Henkin’s lemma.