Research

We have generalised the notion of categorical theory in model theory to the context of coherent theories. We prove a duality result between the full sub-2-category of pretopoi which are categorical, and the 2-category of profinite monoids. We also study the geometry of profinite monoids via the classifying topos construction, and show it identifies them as a full sub-2-category of the 2-category of topoi.

This paper shows that the sheaf representation of finitely presented Heyting algebras constructed by Ghilardi and Zawadowski is, from an algebraic perspective, equivalent to the construction of profinite completion. We show that the dual category of profinite Heyting algebras is an infinitary extensive regular category, and its ex/reg-completion is exactly the aforementioned sheaf topos, which we refer to as the K-topos. We show how certain properties of uniform interpolation can be generalised to the context of arbitrary profinite Heyting algebras, and are consequences of the internal logic of the K-topos. Along the way we also establish various topos-theoretic properties of the K-topos.

Constructed a coherent theory of arithmetic, whose syntactic category is the initial coherent category with a parametrised natural number object. Applied it to characterise provably total recursive functions in IΣ1, and study other proof-theoretic properties of arithmetic.

Defined uniform diagonal operators and studied naming relations on syntax of arithmetic. They are used to distinguish functional and accidental self-reference. Applied them to the study of Henkin sentences, as well as other self-referential sentences in meta-mathematics.

Established a unified framework via topological categories encapsulating various existing semantics of modal logic. Obtained exact correspondence between fibrational structures of topological categories and syntactic features of modal logic. Based on my Bachelor thesis.

The main idea of this paper is that, from a jointly consistent relation, one can define and recover all the usual logical connectives and their universal properties. This is inspired by the independence relation that is widely used in quantum logic.

Concretely, we show that the free Heyting algebra on two generators, hence also on N generators for every N greater than 2, cannot be such a Heyting algebra. The mathematical results in this document were obtained with the help of ChatGPT 5.6 Sol, although the document itself was written entirely by us, and we take full responsibility for its contents.

In domains, categories, and toposes, the Sierpiński cone construction glues onto a space a universal closed point lying below all the other points. Although this is a lax colimit, it also enjoys a well-known right-handed universal property: the Sierpiński cone classifies partial maps defined on an open subspace. The situation proves more subtle in synthetic models of space based on extending homotopy type theory with an interval, as in several recent approaches to synthetic higher categories and domains: although globally it may well be the case that the Sierpiński cone classifies partial maps, this property cannot hold of all parameterised types without degenerating the theory. On the other hand, there are reflective subuniverses within which the classifying property nonetheless holds.
We show that the largest subuniverse in which the Sierpiński cone classifies partial maps is the accessible localisation at a family of embeddings parameterised in the interval, and this subuniverse is contained within the Segal types; this containment is moreover strict in the sense that when the interval is non-trivial, it is not possible for all Segal types to lie in the subuniverse. We finally extend these results from Sierpiński cones to mapping cylinders, providing a new right-handed universal property for the latter.

We explore the notion of conceptual completeness for a fragment of geometric logic in the framework developed by the first and third author. Unlike its traditional interpretation as a reconstruction of syntax from semantics, in this paper we characterise conceptual completeness of a fixed fragment in terms of a duality between theories and topoi. We then show that conceptually complete fragments are conservatively embedded in full geometric logic, thus casting conceptual completeness in a new proof-theoretic light. We give a new proof of conceptual completeness for coherent logic, and we also show that regular, disjunctive, and essentially algebraic logic with falsum are conceptually complete. Finally, we show that our notion is equivalent to a traditional reconstruction result under the assumption of completeness with respect to set-based models: in the coherent case, we thus recover Makkai’s original reconstruction theorem via ultracategories.

We show that a vast class of finitary fragments of geometric logic admits a form of Craig interpolation property. In doing so, we provide a new dictionary to import technology from algebraic logic to categorical logic.

We use Kan injectivity to axiomatise concepts in the 2-category of topoi. We showcase the expressivity of this language through many examples. We use this technology to introduce fragments of geometric logic, and we accommodate essentially algebraic, disjunctive, regular, and coherent logic in our framework, together with some more exotic examples. We show that each fragment H in our sense identifies a lax-idempotent (relative) pseudomonad 𝖳 on 𝗅𝖾𝗑, the 2-category of finitely complete categories. We show that the algebras for 𝖳 admit a notion of classifying topos, for which we deliver several Diaconescu-type results. The construction of classifying topoi allows us to define conceptually complete fragments of geometric logic.

We explore a new connection between synthetic domain theory and Grothendieck topoi related to the distributive lattice classifier. In particular, all the axioms of synthetic domain theory (including the inductive fixed point object and the chain completeness of the dominance) emanate from a countable version of the synthetic quasi-coherence principle that has emerged as a central feature in the unification of synthetic algebraic geometry, synthetic Stone duality, and synthetic category theory. The duality between quasi-coherent algebras and affine spaces in a topos with a distributive lattice object provides a new set of techniques for reasoning synthetically about domain-like structures, and reveals a broad class of (higher) sheaf models for synthetic domain theory.

We develop a general framework to lift the pushout-product axioms in classical homotopy theory to the structured context of algebraic weak factorisation systems. The outcome is a notion of an algebraic monoidal model category. Within this framework, we are able to formulate and prove a structured analogue of Joyal-Tierney calculus, with the help of which we put an algebraic monoidal structure on effective Kan fibrations.

Effective Kan fibration is a new notion of fibration to develop a constructive model of homotopy type theory on simplicial sets. We show there is a path category structure on the full subcategory of effective Kan fibrations over any object, using the algebraic monoidal structure constructed earlier. This brings us closer to showing the existence of a full model structure. Finally, we also identify a key semantic property, which we refer to as Moore equivalence extension. We are able to show that if simplicial sets satisfy this property, then there exists a full algebraic monoidal model category structure for effective Kan fibrations.

The thesis gives a structural study of the “landscape of information”. The general type of information structures we consider are those supporting the interpretation of certain (extensions of) modal systems. The project provides a precise description of the common mathematical background for all such types of models, and studies interactions between all these different types of semantics by considering functorial transformations between them.

This is the first of a series of papers on stack representation of finitely presented Heyting pretoposes. We have provided the first step by constructing a (2, 1)-site, which can be thought of as the site of finite Kripke frames, such that the (2,1)-category of finitely presented Heyting pretoposes contravariantly embeds into the (2,1)- topos of stacks on this (2, 1)-site.

There are many “counterexamples” of second incompleteness theorem. This is a document explaining how categorical logic can help pin down what exactly it means to say “PA cannot prove its own consistency”, and provide a correct proof of second incompleteness theorem.