April 10, 2018: Alex Simpson: A family of atomic toposes
The atomic coverage (Grothendieck topology) is defined on any category that satisfies the property that every cospan completes to a commuting square. This property is sometimes called the right Ore condition. It is trivially satisfied by any category with pullbacks. More generally, even in the absence of pullbacks, there is often a "universal" way of completing cospans to commuting squares. In the talk I shall present examples of this situation, and I shall discuss special properties of atomic toposes that arise from sites of this nature.
April 10, 2018: Joost Joosten: Münchhausen provability
We present a series of provability notions of ever increasing strength along a given representable ordinal. Since the stronger notions of provability allow statements about the weaker ones as oracles we use, adopting the characteristic Utrecht-style terminology, the name of Münchhausen provability. We prove various desirable properties of Münchhausen provability. Most notably, we will see that under some rather general conditions the notion provides a sound and complete interpretation of the transfinite polymodal provability logic GLP. Furhter we will see that the provability notions coincide in a certain sense with the Turing degrees. For this reason, Münchhausen provability is outside Utrecht often referred to as The Turing Jump interpretation of transfinite polymodal provability logic.
May 14, 2018: Zlatan Damnjanovic: On Weak Fragments of Set Theory and Arithmetic
An elementary theory of concatenation, QT+, is introduced and used to establish mutual interpretability of Robinson arithmetic, Minimal Predicative Set Theory of Montagna and Mancini, quantifier-free part of Kirby's finitary set theory, and Adjunctive Set Theory, with or without extensionality.
May 24, 2018: Sven Bosman: Stability Theory
Stabiltity theory is a topic in mathematical logic that grew from classical model theory in the 1970's, as a tool to prove a strong result on the number of models that a first-order theory can have. It has grown into an active area of research in mathematical logic, and has applications not only in classical model theory, but also in algebraic geometry. In this presentation, we will see the definition of a stable theory, and consider some examples and nonexamples. We will also treat several important concepts in stability theory, such as the forking calculus. We will conclude with a small look at an application of stability theory to algebraic geometry.
May 29, 2018: Jetze Zoethout: Provability Logic and the Completeness Principle
Ever since Kurt Gödel proved his celebrated incompleteness theorems, we know that arithmetical theories can talk about their own notion of provability. In provability logic, one tries to answer the question: what does a theory prove about its own notion of provability? For many classical theories, this question was answered by Robert Solovay in 1976. In this talk, we will have a look at constructive theories, that is, theories that are not equipped with the law of the excluded middle. For such theories, provability logic turns out to be far more complicated than it is in the classical case. We will present a new variant of Solovay's argument that can be used to obtain provability logics of certain constructive theories. (This is joint work with Albert Visser.)
June 25, 2018: Menno de Boer: The Gluing Construction for Path Categories
In their book Introduction to Higher Order Categorical Logic, Lambek and Scott showed that the Freyd Cover for Toposes is a useful tool in establishing canonicity results for higher order categorical logic. An example of such a result was showing that each term of the natural numbers type is equal to a term of the form S^k(0), where k is some natural number. The Freyd Cover is an example of a more general construction called the gluing construction. One of the goals of my thesis was to show that this gluing construction is also possible for a different kind of categories called path categories. These were first introduced in a paper by Benno van den Berg and Ieke Moerdijk and are a categorical model for homotopy type theory with propositional identity types. The motivation behind this is, that it will hopefully lead to proving canonicity results about this form of homotopy type theory. In my talk I will give an introduction to path categories and present the gluing construction for them. We will also look at a special kind of objects that path categories can possess called homotopy exponentials. These differ from usual exponentials in that the universal properties hold only up to homotopy. We can then explore when the gluing construction can have these homotopy exponentials.
June 28, 2018: Tom de Jong: Realizability with Scott's Graph Model
A partial combinatory algebra (pca) is an abstract models of computation. Given a pca, one can construct a topos: the realizability topos. An example of a pca is Scott's graph model. In my master's thesis, I study its realizability topos. In the talk, I will introduce pcas and we will study Scott's graph model in some detail. We will investigate its realizability topos from three perspectives. Firstly, we will look at arithmetic in the topos. Then, I will introduce some concepts from synthetic domain theory and give examples for our specific topos. I will finish by presenting a (Quillen) model structure on a full subcategory of the topos.
June 28, 2018: Mark Kamsma: Classifying Topoi and Model Theory
A classifying topos contains a lot of information about the theory it classifies. In general classifying topoi work with geometric logic. When trying to extend this to first-order logic, one may run into trouble. We will look at the exact problems that arise in the first-order setting and how to solve them. In particular, we will characterize when a first-order classifying topos exists. To find connections with Model Theory, we will also want to consider classical logic instead of the intuitionistic logic of topoi. To this end, we introduce the concept of a Boolean classifying topos. We will then obtain a similar characterization of when such a Boolean classifying topos exists, as we did for first-order classifying topoi.