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.
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.
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.
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.
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.
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.
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.
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.
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)
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.
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.
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).
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.
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).
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.
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.
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.