Simon Raßmann,
18. of Nov 2022:
Definablity of graphs with abelian colour classes in
finite-variable counting logics

Marius Tritschler,
4. of Nov 2022:
Hybrid Team Logics

Hybrid team logics are variations of team logics that use binders known from hybrid modal logics to "save" teams as relations. This has interesting connections to other team logics like inclusion or dependence logic, which in turn correspond to fragments of existential second order logic.

Jonathan Weinberger,
21. of Oct 2022:
Dialectica constructions and lenses

In the 1940s, Gödel devised the Dialectica interpretation, a proof interpretation used for relative consistency proofs in constructive logic. In her doctoral dissertation (late 1980s to early 1990s), de Paiva introduced the notion of Dialectica categories supporting various versions of the Dialectica construction. This has since been generalized to fibrations in later work by Hyland and Hofstra, leading e.g. to Dialectica models of type theory (cf. the works by von Glehn and Moss). In the talk, I will discuss work in progress concerning the connections of the (categorical or fibrational) Dialectica construction with lenses. The concept of a lens is known from database theory and it formalizes a kind of transition system that is able to receive inputs and internally convert them to a different form. Lenses can be seen as an instance of the general concept of whats called an optic. On the other hand, using (fibered) categorical language, lenses can also be seen as an instance of de Paiva's Dialectica construction. The relevant notions concerning Dialectica constructions and lenses will be introduced in the talk. This is joint work in progress with Matteo Capucci, Bruno Gavranovic;, Abdullah Malik, Francisco Rios under the direction of Valeria de Paiva as a (sub-)project of the AMS Math Research Community on Applied Category Theory 2022-2023.

Emanuele Frittaion,
5. of Aug 2022:
Iterating reflection over Heyting arithmetic

Pedro Pinto,
22. of Jul 2022:
Unwinding of proofs

Nicholas Pischke,
24. of Jun 2022:
Proof-theoretic aspects of set-valued operators and their connections with recent results in proof mining

Simon Raßmann,
10. of Jun 2022:
Finding the number of variables needed for identification of graphs

Over finite graphs, first-order logic is sufficiently expressive to be able to define every graph up to isomorphism. In particular, the graph isomorphism problem can also be phrased as the problem of deciding whether two given graphs agree on all first-order sentences. But as we do not know whether this can be checked in polynomial time, Immerman and Ladner proposed in 1990 to relax this problem and consider only sentences in some fragment of first-order logic. The most important fragments in this context are k-variable fragments enriched by counting quantifiers, for which we can decide equivalence in polynomial time. This yields polynomial-time algorithms for the graph isomorphism problem over many classes of graphs including e.g. planar graphs. We consider the computational complexity of determining how many variables are needed to define a given graph. In particular, we show that the problem of deciding whether k variables suffice is P- complete over a class of graphs including many graphs which are notoriously difficult for both theoretical and practical solvers of the graph isomorphism problem.

Davide Manca,
27. of May 2022:
Strongly normal partial order dilators

Patrick Uftring,
13. of May 2022:
Proving a finite variant of the Uniform Kruskal Theorem using false axioms

Paulo Santos,
17. of Sep 2021:
Numeral Completeness of Theories of Arithmetic

We will present a numeral completeness result that holds for weak theories of arithmetic; more precisely, we are going to prove that, starting from a true sentence, one can express the fact that the sentence is true inside the weak theory using numerals. We will obtain a numeral form of provable consistency. The third main result that we will present shows that there is a primitive recursive function (we will see that this function can also be Kalmar elementary) that outputs, for each n, a proof that n is not a proof of a contradiction in a fixed consistent theory. We will relate our result with late versions of Hilbert's Program.

Catrin Mair,
20. of Aug 2021:
Animated Condensed Sets and Their Homotopy Groups

Helen Preiß,
6. of Aug 2021:
What Replaces Diagonalisation in Boolos’ Proof of the First Incompleteness
Theorem?

Moritz Lichter,
12. of Mar 2021:
Canonization for Bounded and Dihedral Color Classes in Choiceless Polynomial
Time

In the quest for a logic capturing PTime the next natural classes of structures to consider are those with bounded color class size. We present a canonization procedure for graphs with dihedral color classes of bounded size in the logic of Choiceless Polynomial Time (CPT), which then captures PTime on this class of structures. This is the first result of this form for non-abelian color classes. The first step proposes a normal form which comprises a ``rigid assemblage''. This roughly means that the local automorphism groups form $2$-injective $3$-factor subdirect products. Structures with color classes of bounded size can be reduced canonization preservingly to normal form in CPT. In the second step, we show that for graphs in normal form with dihedral color classes of bounded size, the canonization problem can be solved in CPT. We also show the same statement for general ternary structures in normal form if the dihedral groups are defined over odd domains.

Anton Freund,
18. of Dec 2020:
Friedman's gap condition as an iteration of Kruskal's theorem

Kruskal's theorem asserts that, in any infinite set of finite trees, some tree can be embedded into another. This result is unprovable in a relatively strong axiom system (ATR_0). It witnesses that Gödel's incompleteness theorem does materialize within mathematics proper. One can make Kruskal's theorem even stronger by considering labelled trees with a certain "gap condition", which is due to Harvey Friedman. This condition can seem somewhat ad hoc: it is usually motivated in terms of ordinal notation systems. In my talk, I will present a completely different and decidedly mathematical motivation: the gap condition arises from iterated applications of Kruskal's theorem itself. My aim is to explain the main ideas on an intuitive level. Full details can be found in arXiv:2003.02714.

Jonathan Weinberger,
11. of Dec 2020:
A Yoneda Lemma for synthetic fibered infinity-categories

Familiarly, any set A is uniquely determined by its points, i.e. A can be identified with the set of all maps 1 -> A. The Yoneda Lemma, a fundamental principle in category theory, generalizes this perspective. It says that a higher order object F is uniquely determined by its "generalized points", i.e. for all generalized points I, the object F(I) can be identified with the collection of all maps I -> F. I'll present a version of the Yoneda Lemma where the higher order objects are families of infinity-categories parametrized by another infinity-category. The novelty lies in its formulation and proof using a synthetic language. The presentation will place emphasis on the geometric ideas underlying the proof. This is joint work with Ulrik Buchholtz.

Jonathan Weinberger,
6. of Nov 2020:
A synthetic language for fibered higher categories

Established by Eilenberg and Mac Lane in the 1940s, category theory has become a central tool in studying and translating between phenomena common to different areas of mathematics such as e.g. topology, geometry, algebra, logic, and theoretical computer science. Namely, a category is a structure comprised of mathematical objects together with transformations aka morphisms between them and a composition operation. Examples are given by the collection of all groups together with group homomorphisms or topological spaces with continuous maps. Also, categories themselves form a category, with an appropriate notion of morphism called functor. Despite having become a standard toolkit in areas such as algebraic topology and algebraic geometry, for certain settings in present day mathematics---prominently in homotopy theory---it is most natural to weaken the notion of a category. Roughly, in a higher-dimensional category, often called infinity-categoy, the objects and morphisms do not form well-defined sets, but rather spaces of some sort. As a consequence, composition of morphism can't be a strict operation anymore but will only be defined up to homotopy of maps (or similar higher-dimensional data). In stark contrast to the case of ordinary 1-categories, it is technically challenging to even give formal definitions of notions of infinity-categories. As a consequence, there is a proliferation of different "models" eventually capturing the same notion of infinity-category. But these models can be very different from each other in terms of "user experience" despite modeling the same kind of homotopical structure. Therefore, it is very appealing to think about a framework that allows for reasoning about infinity-categories in a more intrinsic and unified way. One approach in this direction has been developed by Riehl and Shulman in 2017. Their framework is based on Homotopy Type Theory---itself an extension of Intuitionistic Martin-Löf Type Theory---notably developed by Voevodsky from around the mid-2000s. Riehl--Shulman work in an extension of Homotopy Type Theory which makes it possible to reason synthetically about infinity-categories in a way that often resembles ordinary category theory, while at the same time admitting homotopy invariance, i.e.theorems and constructions are automatically stable under substituting homotopy-equivalent objects. In the talk, we start off with an informal introduction to Riehl–Shulman's synthetic theory for infinity-categories. Next, we present definitions and results newly devised in this setting concerning fibered infinity-categories, i.e. families of infinity-categories functorially parametrized by an indexing infinity-category. The main points are closure properties of synthetic fibered infinity-categories, characterization theorems and a 2-categorical Yoneda Lemma. Besides Riehl--Shulman's work, our approach is heavily informed by Riehl--Verity's infinity-cosmos theory, which is a different and highly developed foundation to model-independent infinity-category theory. No prior knowledge of either category theory nor type theory is assumed. This is joint work with Ulrik Buchholtz.

Nora Khayata,
23. of Oct 2020:
Statically Inferring Method Consistency Levels using Pre- and Postcondition
Analysis

Modern distributed applications like Facebook or Twitter replicate data to improve performance for users. With this, data copies are distributed on multiple servers around the globe. Managing and synchronising the replicas is a performance costly task, which is why synchronisation is kept at a minimum. However, some operations like withdrawing money from a bank account must be synchronised in order to guarantee that nonexistent money cannot be withdrawn. Modern systems thus allow developers to declare operations as "strong" when synchronisation is needed and "weak" if synchronisation can be omitted. Nonetheless, choosing which operation can be executed weakly and which one must be executed strongly is a very error-prone task. If weakly executable operations are declared to be strong, performance potential is wasted whereas if strong operations are declared weak, potentially unwanted or incorrect application behaviour is risked. In order to support Java developers with this tedious task, we present an implementation that automatically infers the correct consistency level for replicated object methods*. Given the class signature with invariants and method pre- and postcondition expressed in JML**, our tool infers when it is possible to execute an operation under weak consistency and when it is necessary to enforce strong consistency. Because our work builds on previous works on this topic, the properties that we use to infer the correct consistency level are already proven to be correct. Additionally using JML as a specification language frees developers from learning new specification languages, but enables utilising basic knowledge on Java and first order logic in order to express operation specifications and application invariants. * operations are called "methods" in object-oriented programming languages like Java, Scala, C++ ** The Java Modeling language is a specification language that allows to express first order constraints on programs using a very "Java-like" language (see http://www.openjml.org)

Joel Doat,
25. of Sep 2020:
Ballet Automaton

In my talk, I will show you a simple automaton whose language contains sequences of movements that make up warm-up routines in classical ballet. This is especially interesting in control theory to construct stylized motion that has to follow given aesthetical rules.

Pedro Pinto,
14. of Aug 2020:
Axiom of Determinacy

The objective of this talk is to introduce the Axiom of Determinacy (AD) and to discuss some of its more elementary results. We start with the notion of Gale-Stewart games. Afterwards we introduce AD and talk about its incompatibility with AC. Lastly, we discuss certain classes of determined sets.

Anton Freund,
10. of Jul 2020:
Mathematical independence without extensional invariants

I will review some known examples of mathematical theorems that are unprovable in (conservative extensions of) Peano arithmetic. These independence results can be explained in terms of extensional invariants, namely, relative computability and growth rates. By exploiting these invariants, one can establish independence without using Gödel's theorem. I will then present a new independence result of a different kind. This result does not seem to involve extensional invariants. Accordingly, the only known independence proof relies on Gödel's theorem (see arXiv:2004.06915 for details).

Andrei Sipoș,
19. of Jun 2020:
A determinant-free proof in basic commutative algebra

We give an alternative, determinant-free proof of a theorem usually proven by way of the Cayley-Hamilton theorem for finitely generated modules over a commutative ring.

Patrick Uftring,
6. of Mar 2020:
Yet another proof for the uniform continuity of terms in Gödel’s T

Sam Sanders,
28. of Feb 2020:
Plato, Brouwer, and the foundations of mathematics

Joel Doat,
21. of Feb 2020:
When bodies speak rhythmic truths

Donghyun Lim,
14. of Feb 2020:
Uniform continuity of multifunctions and a quantitative selection theorem for
encoding spaces of continuum cardinality

Anton Freund,
7. of Feb 2020:
A uniform Kruskal theorem

Kruskal's theorem shows the following: for any infinite sequence T_0,T_1,... of finite trees, there are indices i<j such that T_i can be embedded into T_j. Nash-Williams has given a particularly elegant proof of Kruskal's theorem, which uses his famous "minimal bad sequence argument". In this talk I will explain Nash-Williams' proof and discuss it from a logical perspective. It is known that Kruskal's theorem does not exhaust the full strength of the minimal bad sequence argument. In contrast, I will present a uniform version of Kruskal's theorem that does require minimal bad sequences (as it is equivalent to Pi^1_1-comprehension). This is joint work with Andreas Weiermann (Ghent) and Michael Rathjen (Leeds).

Franziskus Wiesnet,
31. of Jan 2020:
The beauty of Minlog

Pedro Pinto,
24. of Jan 2020:
The bounded functional interpretation

Felix Canavoi ,
1. of Jun 2017:
Introduction to modal characterisation theorems

Thomas Powell,
18. of May 2017:
Basic Domain Theory

Jonathan Weinberger,
27. of Apr 2017:
Introduction to Homotopy Type Theory.

Florian Steinberg,
6. of Apr 2017:
A counterexample.

Julian Bitterlich,
23. of Mar 2017:
Something about covers?

Jonathan Weinberger,
9. of Mar 2017:
An introduction to model categories

Felix Canavoi,
23. of Feb 2017:

Makoto Fujiwara,
16. of Feb 2017:
Weak logical principles and bar Induction over intuitionistic arithmetic

My current interest is in constructivism. Intuitionistic (many-sorted) arithmetic is, in general, thought to be a formal system corresponding to constructive mathematics. However, there are some principles which are not provable in standard intuitionistic arithmetic but constructive in some sense. In this talk, I would talk about the structure of weak fragments of logical principles the relation between them and weak fragments of bar induction. It is intended to discuss the criterion for acceptable principles in constructive mathematics.

Sam Sanders,
15. of Feb 2017:
Infinitesimals, klein aber oho! (Shameless propaganda of Nonstandard Analysis)

Infinitesimals are used to date in physics and engineering, and historically in mathematics until the advent of the well-known ‘epsilon delta’ framework pioneered by Weierstrass. In the 60’ies, Abraham Robinson introduced ’Nonstandard Analysis’, a logical framework which accommodates the intuitive infinitesimal calculus. I will provide a historical overview and some shameless propaganda of why everyone (and their dog) should use Nonstandard Analysis.

Angeliki Koutsoukou-Argyraki,
9. of Feb 2017:
An introduction to proof mining

A discussion on the fundamental ideas, techniques, possibilities and limitations of proof mining. An example on the extraction of computable and uniform bounds for the fixed point theory of one-parameter nonexpansive semigroups on a subset of a Banach space.

Florian Steinberg,
12. of Jan 2017:

Ulrik Buchholtz,
15. of Dec 2016:
Ulrik presented the Cayley-Dickson construction and gave a short glimpse of homotopy type theory.

Thomas Powell,
1. of Dec 2016:
Thomas gave a talk about constructing categories inspired by the dialectica translation and relations to linear logic.

Julian Bitterlich ,
17. of Nov 2016:

Florian Steinberg ,
17. of Aug 2016:

Daniel Körnlein ,
13. of Jul 2016:
Voting

,
5. of Jun 2016:

Florian Steinberg ,
13. of Oct 2015:
Weihrauch reductions and classification of operations on analytic functions

Daniel Körnlein ,
30. of Sep 2015:
On Cat(\kappa)spaces

Florian Steinberg ,
7. of Jul 2015:
on Arzela-Ascoli lemma

Hugo Férée ,
23. of Jun 2015:

Felix Canavoi ,
9. of Jun 2015:

Angeliki Koutsoukou-Argyraki ,
26. of May 2015:
Proof mining for fixed point theory

Florian Steinberg ,
12. of May 2015:

Julian Bitterlich ,
23. of Apr 2015:

Davorin Lesnik,
30. of Jun 2014:
Davorin gave a series of talks about category theory and synthetic topology, from late June 2014 till Winter 2015.

Vassilis Gregoriades ,
18. of Jun 2014:
The connection between descriptive set theory and computable analysis

Stephan Le Roux,
6. of Jun 2014:
Stephan gave a nice introduction into game theory and Nash equilibria.

Yasuyuki Tsukamoto, Julian Bitterlich ,
22. of May 2014:
Imaginary cubes, Ehrenfeucht-Fraise Games respectively

Angeliki Koutsoukou-Argyraki ,
8. of May 2014:
Modulus of Accretivity for multi-valued operators in a real Banach space

,
3. of Apr 2014:
free discussion

,
6. of Mar 2014:
free discussion