Tag - Logic

Christian Espíndola: Categoricity in infinite quantifier theories

22nd October, 2020

Morley’s categoricity theorem states that a countable first-order theory categorical in some uncountable cardinal is categorical in all uncountable cardinals. Shelah's categoricity conjecture states that a similar eventual categoricity behaviour holds for certain infinitary theories in finite quantifier languages. In this talk we will explain the main ideas of a work in progress aiming at a version of eventual categoricity for theories in infinite quantifier languages. On the categorical side this corresponds to accessible categories, where the notion of internal size is taken instead of the cardinality of the underlying model. We will start motivating this with some examples computing the categoricity spectrum of infinite quantifier theories. Then we will study also to what extent the Generalized Continuum Hypothesis can be avoided through forcing techniques and how the use of large cardinals can replace model-theoretic assumptions like directed colimits or amalgamation. Our ultimate goal is to determine whether large cardinals are really needed for these latter assumptions or whether they just follow instead from categoricity.

Taichi Uemura: The universal exponentiable arrow

15th October, 2020

Cartmell showed that the category of generalized algebraic theories is equivalent to the category of contextual categories. This implies that the theory of generalized algebraic theories is essentially algebraic. We characterize the essentially algebraic theory of generalized algebraic theories as the free category with finite limits and with an exponentiable arrow.

Raffael Stenzel: (∞,1)-comprehension schemes

24th September, 2020

Comprehension schemes arose as crucial notions in the early work on the foundations of set theory, and hence they found expression in a considerable variety of foundational settings for mathematics. Particularly, they have been introduced to the context of categorical logic first by Lawvere and then by Benabou in the 1970s.

In this talk we define and study a theory of comprehension schemes for fibered ∞-categories, generalizing Johnstone’s respective notion for ordinary categories. This includes natural generalizations of all the fundamental instances originally defined by Benabou, and their application to Jacob's comprehension categories. Thereby, we can characterize

  • numerous categorical structures arising in higher topos theory,
  • the notion of univalence,
  • internal ∞-categories,

in terms of comprehension schemes, while some of the 1-categorical counterparts fail to hold in ordinary category theory. As an application, we can show that the universal cartesian fibration is represented via externalization by the "freely walking chain" in the ∞-category of small ∞-categories.

In the end, if my time management permits, we take a look at the externalization construction of internal ∞-categories from a model categorical perspective and review some examples from the literature in this light.

Christopher Dean: Globular Multicategories with Homomorphism Types

28th May, 2020

We introduce structures called globular multicategories with homomorphism types. We discuss how various collections of "higher category-like" objects can be used to to construct these globular multicategories. We show how to obtain a number of higher categorical structures using this data. We will see that in this setting there is a precise sense in which:

  • types are higher categories,
  • dependent types are profunctors,
  • terms are higher functors,
  • terms in a dependent context are higher transformations,
  • there is a higher category of all types and terms.

Axel Osmond: Towards a 2-dimensional spectral construction

21st May, 2020

Many prominent dualities in mathematics are instances of a common construction centered on the notion of spectral functor. Roughly stated, one starts with a locally finitely presentable category, equipped with a subcategory of distinguished local objects encoding point-like data and a factorization system (Étale maps, Local maps) where the etale maps behave as duals of distinguished continuous maps. Several manners of axiomatizing the correct relation between those ingredients have been proposed, either through topos theoretic methods by "localizing" local objects with a Grothendieck topology generated by étale maps, or in an alternative (though tightly related) way based on the notion of local right ajoint (or equivalently stable functor). Then the spectrum of a given object is constructed as a topos classifying etale maps under this given object toward local objects, equipped with a structural sheaf playing the role of the "free local object" under it. This defines a spectral functor from the ambient locally finitely presentable category to a category of locally structured toposes, forming an adjunction with a corresponding global section functor. This construction provide a convenient template for several prominent 1-categorical examples, as dualities for rings in algebraic geometry, or also Stone-like dualities for different classes of propositional algebras. The strong analogy between those dualities and their corresponding first order syntax-semantics dualities suggests the later could be understood as instances of a convenient 2-dimensional spectral construction. In this talk we will expose the ongoing work devoted to concretize this intuition.

After recalling the 1-dimensional version of the construction and the details of some prominent Stone-like examples, we introduces a notion of stable 2-functor and provide a method to construct an associated notion of spectral 2-sites, defining the spectrum as the associated Grothendieck 2-topos equipped with a distinguished structural stack. In particular we give a special interest in determining the local objects and the factorization system associated to doctrines corresponding to fragments of first order logics, as Lex, Reg, or Coh; in those situations, the construction simplifies as the spectral site happens to be 1-truncated so that one recover the corresponding 1-dimensional notion of classifying topos of a theory as the spectrum, and the geometry of the spectrum actually arises from the geometric properties of local toposes and étale geometric morphisms.

Christian Espíndola: Topos-theoretic completeness theorems

7th May, 2020

In this talk we will delve into the background details of the previous talk by introducing syntactic proof systems and their categorical semantics, including the construction of syntactic categories and κ-classifying toposes, as well as the role of certain properties of Grothendieck topologies and
Kripke-Joyal semantics. We will then study some topos-theoretic completeness theorems for certain infinitary logics that generalize results of Deligne and Joyal.