Oberseminar Logik - WS 2022/23

Organizers

• Prof. Dr. Philipp Hieronymi
• Dr. Christian d'Elbée

Time and location

Unless stated otherwise: Mondays 17.00-18.00 in room N0.007, Endenicher Allee 60 and on Zoom.

The participants of the seminar are welcome for coffee and tea in room 4.005 (office Hieronymi) at 16.30 before the talks.

Subscribe to the mailing lists for the Oberseminar and other logic activities in Bonn: https://listen.uni-bonn.de/wws/subscribe/logic.

Talks

• October 10th: No seminar
  
• October 17th: Christian d'Elbée (Bonn) - The generic theory of fields expanded by a multiplicative endomorphism
  
  I will present the theory ACFH which axiomatises existentially closed fields expanded by a multiplicative homomorphism, which is a function satisfying f(xy)=f(x)f(y). This theory is NSOP_1 and not simple, and I will explain how to get to those conclusions. I will mention results about higher amalgamation and imaginaries.
  
• October 24th: No seminar
  
  
• October 31th: Eion Blanchard (Illinois) - Decidability bounds for Presburger arithmetic extended by sine
  
  Abstract. We consider Presburger arithmetic (PA) extended by the sine function, call this extension sine-Presburger arithmetic (sin-PA), and systematically study decision problems for sets of sentences in sin-PA. In particular, we detail a decision algorithm for existential sin-PA sentences under assumption of Schanuel's conjecture for the complex numbers. This procedure reduces decisions to the theory of the ordered additive group of real numbers extended by sine, whose decidability under Schanuel's conjecture follows from work of Macintyre and Wilkie. On the other hand, we also prove four alternating quantifier blocks suffice for undecidability of sin-PA sentences. This work is joint with Philipp Hieronymi.
  
• Wednesday November 2nd 15:15-17:15, Lipschitz-Raum: Johan Commelin (Freiburg) - Introductory lecture on Lean and demonstrations
  
  This is part of the Pluecker lectures 2022. It will consists of this introductory lecture, an intense practical tutorial session on the Lean theorem prover and two lectures by Kevin Buzzard in the following week.
  
• Monday November 7th, Plücker Lecture 17:00-18:00, Lipschitz-Raum: Kevin Buzzard (Imperial College London) - The future of mathematics?
  
  Abstract. The computer has undoubtedly changed mathematics. Its ability to do calculations at superhuman speeds means that we can numerically solve differential equations, run simulations, and test certain conjectures by trying them on many examples. But we are now entering an age where the computer will not just help us to compute, but help us to reason?. Machine learning techniques have led humans to new theorems in knot theory, group theory and the theory of PDEs. Interactive theorem provers are now capable of understanding modern mathematics. Putting these techniques together, machines can now solve some Mathematical Olympiad level problems completely autonomously, and the systems will only get more powerful over time. How good will they get? Absolutely nobody knows. However I do believe that it is important that mathematicians begin to learn more about this area, and this is why I chose the subject to be the topic of my Plücker lectures.
  
  In my first lecture I will give an overview of the new ways that computers are being used by mathematicians. A mathematical background will be assumed, but no understanding of machine learning or theorem provers is necessary. In my second lecture I will explain how a mathematician can teach research level mathematics (sphere eversion, condensed mathematics and so on) to an interactive theorem prover, based on my experiences using the Lean theorem prover.
  
• Tuesday November 8th, Plücker Lecture 17:00-18:00, Lipschitz-Raum: Kevin Buzzard (Imperial College London) - Theorem provers and modern research
  
  Abstract. See above.
  
• November 14th: No seminar
  
  
• November 21th: Rosario Mennuni (Pisa) - Automorphisms of ordered abelian groups and dependent positive theories
  
  This talk is concerned with the interaction between two themes: generic structures with an automorphism and NIP (or dependent) theories. NIP theories are a generalisation of stable theories which include ordered structures such as ordered abelian groups, or the real exponential field. They played a central role in the model theory of the last couple of decades, notably in the solution of Pillay's o-minimal conjectures and in the model theory of valued fields. As for the first theme, recall the following construction. Start with a theory T, add to the language a symbol for an automorphism, resulting in a theory T', and look at the class K of existentially closed models of T'. Sometimes, the class K is elementary. This is for instance true when T is the theory of algebraically closed fields; in this case, elementarity of K allowed to apply neostability-theoretic techniques to its theory, known as ACFA, resulting in important applications to difference algebra. Suppose we perform the above construction by taking as T the theory of ordered abelian groups, or more generally by starting with a NIP unstable T. By a result of Kikyo and Shelah, the class K is not elementary. In order to study such classes, and for example ask whether they are NIP, one needs to generalise neostability properties outside of the context of classical first-order theories. This is indeed possible by working in the framework of positive logic. I will report on recent work of myself and Jan Dobrowolski on the development of NIP in positive logic, and on the study of existentially closed ordered abelian groups with an automorphism.
  
• November 28th: No seminar
  
  
• December 5th: Adrian De Lon (Bonn) - Ingredients for natural formalization
  
  The Naproche work group here in Bonn designs and implements the natural proof assistant Naproche, an interactive computer program that can understand and verify (controlled) natural language mathematics, using automated first-order theorem provers to fill in proof gaps. In this talk I will first present a brief overview of the architecture and individual components of Naproche, and then report on my current work in improving upon the existing design and implementation of Naproche. We will also look at example formalizations in Naproche.
  
• December 12th: Adrien Deloro (Sorbonne Université) - Quasi-Frobenius pairs in model theory
  
  The talk is in model-theoretic algebra, more specifically at the intersection of group theory and model theory. The latter is `soft', as it uses only dimension functions and no stability theory. A pair of groups (C < G) is called quasi-Frobenius if (1) C has trivial intersections with its distinct G-conjugates and (2) C has finite index in its normaliser in G. This generalises the classical notion of a Frobenius pair, in order to also capture natural configurations from geometric algebra, such as the geometry of PGL(2,C) or SO(3,R). The talk studies these pairs in the context of finite-dimensional theories, which generalise both finite Morley rank and o-minimal worlds. I shall survey recent work by a number of people.
  
• December 19th: No seminar
  
  
• January 9th: No seminar
  
  
• January 19th, Bethe Colloquium, 16.15, Lecture Hall I, Physics Institute (Nussallee 12) Thomas Grimm (Utrecht University) - The Tameness of Quantum Physics
  
  Abstract. While physicists have learned to accept the many wild phenomena of quantum theories, one might hope that at least the mathematical structure of these theories is more tame and inherently geometric in nature. The aim of this colloquium is to introduce a general tameness principle, using o-minimal structures originating in mathematical logic, and argue that it is common to many well-defined quantum theories. We will discuss quantum field theories and the tameness of perturbative scattering amplitudes. At the non-perturbative level, tameness depends on the high-energy definition of the physical theory and might be seen as a condition that arises from consistency with quantum gravity. In fact, all well-understood effective theories derived from string theory are tame. This fact was key in the mathematical proof of an almost 20-year-old finiteness conjecture for string theory vacua.
  
• Saturday January 28th Lipschitz-Raum: GeSAMT (Gemeinsames Seminar Algebra und Modelltheorie)
  
  11:00 - 11:45 Coffee
  11:45 - 12:45 Daniel Hoffmann (Münster/Warsaw/Dresden): A bit of model theory of finite group actions
  Abstract: The content of the talk is based on a joint paper with Piot Kowalski, "PAC structures as invariants of finite group actions" - a preprint is available on the personal websites of the authors. Apparently, the notion of a PAC structure is closely related to group actions by automorphisms on structures. For example, in the case of ACFA, the subfield of invariants is a pseudofinite field and encodes some properties of the whole difference field. As we study group actions of finite groups, this relation between the whole structure equipped with a group action and its substructure of invariants should be more evident. We work with structures equipped with a group action of a finite group, which are substructures of some saturated stable overstructure. Our first main result says when a structure with a group action is existentially closed - and this is encoded by the properties of the substructure of invariants. The second result gives a condition for the existence of a model companion of discussed substructures with finite group action. Then we list examples of model companions obtained by applying our general technique.
  
  13:00 - 14:45 Lunch
  14:45 - 15:45 Alessandro Codenott (Münster) : Some examples of tame dynamical systems answering questions of Glasner and Megrelishvili
  Abstract: Glasner and Megrelishvili have recently introduced two measures of complexity for tame dynamical systems. The first is a division of those systems into three classes: tame, tame_1 and tame_2, while the second is a countable ordinal called the beta-rank of the system. They asked whether there is an action on a dendrite that fails to be tame_1 and whether, for every countable ordinal alpha, there is a tame dynamical system of beta-rank alpha. They also asked whether there exists a tame rigid system which is not HNS and whether there exists a minimal tame rigid system which is not equicontinuous. We give a positive answer to those four questions by constructing various examples of tame systems.
  
  15:45 - 16:00 Cofee
  16:00 - 17:00 Francesco Gallinaro (Freiburg) : Quasiminimality of Complex Powers
  Abstract: A conjecture due to Zilber predicts that the complex exponential field is quasiminimal: that is, that all subsets of the complex numbers that are definable in the language of rings expanded by a symbol for the complex exponential function are countable or cocountable. Zilber showed that this conjecture would follow from Schanuel's Conjecture and an existential closedness-type property asserting that certain systems of exponential-polynomial equations can be solved in the complex numbers; later on, Bays and Kirby were able to remove the dependence on Schanuel's Conjecture, shifting all the focus to the existence of solutions. In this talk, I will discuss recent work about the quasiminimality of a reduct of the complex exponential field, that is, the complex numbers expanded by multivalued power functions. This is joint work with Jonathan Kirby.