Talks and abstracts

  1. Albert Atserias:

    • Proof Complexity and Its Relations to SAT-Solving

      Propositional proof complexity is the study of algorithms that recognize the set of tautologies in propositional logic. Initially conceived as an approach to address the “P versus NP” problem in computational complexity, the field has gradually expanded its focus to include new objectives. Among these is the goal of providing a theoretical foundation for comparing the effectiveness of heuristics for algorithms that exhaustively explore the solution spaces of combinatorial problems. Dually, and complementarily, the methods of proof complexity can also be used to assess how to certify that a given exploration path of such an algorithm ultimately leads to a dead end. A notable challenge faced by this methodology lies in the fact that, despite the theoretically proved modelling power of propositional logic, as established by the theory of NP-completeness, propositional logic is not always the best specification language for all application domains. Addressing this challenge involves studying the expressive power of various languages and their associated proof systems through the lens of computational complexity.

      The first part of this talk will be a survey of how the emergence of these new objectives for propositional proof complexity came to be, and what the theory’s methods offer in pursuing them. The second part will review the current state of the art on the computational complexity of automating the proof search problem for various proof systems for propositional logic and other languages. While it is now known and well understood that fully automating propositional Resolution as a proof system for propositional logic is NP-hard, it remains an open question whether it is possible to distinguish satisfiable formulas from unsatisfiable ones with short Resolution proofs of unsatisfiability in polynomial time. As of the time of writing, there is no consensus among experts on whether this problem should be considered computationally intractable.

  2. Ingo Blechschmidt:

    • The curious world of infinite time Turing machines (Slides 1)

      There are more real numbers than natural numbers. Or are there? Meet the bizarre topos of infinite time Turing machines, where two plus two is still four and still infinitely many prime numbers exist, but where the axiom of choice fails, not every mathematical assertion is true or false—and where there is an injection from $\mathbb{R}$ to $\mathbb{N}$.

    • Computing an integer using the modal toposophic multiverse (Slides 2)

      Combinatorics and commutative algebra abound with situations where we prove quite concrete results by quite abstract transfinite methods, such as minimal bad sequences or maximal ideals. Amazingly, such infinitary arguments can often be understood as blueprints for quite explicit computations—as called for by Hilbert’s programme. In this talk, we will travel the modal toposophic multiverse to facilitate this kind of mining abstract proofs for refined quantitative results. We will use a celebrated theorem from order theory about sequences $\mathbb{N}\rightarrow\mathbb{N}$ that everybody can relate with as a running example.

  3. Adrien Deloro:

    • Dimensions in model theory and model-theoretic algebra (Slides 1, Slides 2)

      The first talk is a survey aimed at a general audience. One needs to know what first-order logic is, and the notion of a model; no further knowledge of model theory is required. I shall explain how two quite different branches of model theory naturally merge into the same topic: theories with a dimension function.

      The second talk will focus on model-theoretic algebra, viz. the study of algebraic structures under model-theoretic constraints. One should certainly know what a field or a group is, but I shall keep things unspecialised. I shall review what is known or not under some dimensionality assumptions, with special focus on o-minimal and finite Morley rank contexts.

      The talks connect, of course, but may be attended independently.

  4. Laura Fontanella:

    • Programming the foundations: a journey through set theory and realizability

      In the 19th century, mathematicians began to explore fundamental questions about the foundations of mathematics. This inquiry led to the development of formal logic, marked by a particular focus on axiomatic systems, from which set theory emerged as a solid foundation for all mathematics. Around the same time, the concept of computability was investigated in connection with the idea that mathematical proofs should be “computable.” This line of inquiry gave rise to Kleene’s realizability.

      In this talk, we will examine how these two research traditions are now converging in the field of classical realizability for set theory. We will explore the construction of models of ZF using lambda-terms and use this technique to investigate the computational content of set theory. We will present the current state of the art alongside several open problems in this area. In particular, we will show that while it is possible to realize even large cardinal axioms, the computational content of the Axiom of Choice remains elusive.

  5. Jonathan Kirby:

    • Some Model Theory of Exponential Fields

      I will survey some of the work done towards understanding the model theory of exponential fields, particularly around Zilber’s approach to the complex exponential field, and the progress towards his conjecture that it is quasiminimal and does not interpret the real field.

  6. Chris Lambie-Hanson:

    • Set theory and derived functors

      These talks will be broadly concerned with the study of questions of compactness, i.e., questions regarding the extent to which the global properties of a structure are determined by its local properties. Such questions are central to the fields of both homological algebra, where failures of local to global phenomena are explicitly measured via derived functors, and set theory, where sophisticated methods have been developed to either construct incompact objects or prove that, at least consistently, they do not exist. These talks will survey some applications of ideas and techniques from set theory to questions about derived functors coming from homological algebra. In the first lecture, we will survey some now-classical results, including Shelah’s work on the Whitehead problem and results of Goblot and Mitchell on derived limits. In the second lecture, we will discuss recent progress on applications of set theory to the study of higher derived limits. No prior knowledge of homological algebra will be necessary; we will focus on the combinatorial ideas underlying the applications.

IMJ-PRG Université Paris Cité Sorbonne Université CNRS