Oberseminar Logik/Oberseminar Formal Mathematics and Computer-Assisted Proving - WiSe 2023/24

Organizers

• Prof. Dr. Philipp Hieronymi
• Prof. Dr. Floris van Doorn

Time and location

Unless stated otherwise: Mondays 17.00-18.00 in SemR N0.003, Endenicher Allee 60.

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 23rd: Pantelis Eleftheriou (Leeds), Unbounded versions of Zarankiewicz's problem
  
  Abstract: Zarankiewicz's problem for hypergraphs asks for upper bounds on the number of edges of a hypergraph that has no complete sub-hypergraphs of a given size. Let M be an o-minimal structure. Basit-Chernikov-Starchenko-Tao-Tran (2021) proved that the following are equivalent:
  
  (1) "linear Zarankiewicz's bounds" exist for hypergraphs whose edge relation is induced by a fixed relation definable in M
  (2) M does not define an infinite field.
  
  We prove that the following are equivalent:
  
  (1') linear Zarankiewicz bounds exist for sufficiently "distant" hypergraphs whose edge relation is induced by a fixed relation definable in M
  (2') M does not define a full field (that is, one whose domain is the whole universe of M).
  
  We will also report on current work on Zarankiewicz's problem in Presburger Arithmetic. This is joint work (in progress) with Aris Papadopoulos.
• Tuesday October 24rd 10.15am N0.008 Neubau: Clara List (Hamburg), On the model account of forcing
  
  Abstract: Forcing is a fundamental technique in set theory that was introduced in 1963 by Paul Cohen and was first used to prove the independence of the Continuum Hypothesis. It is a method for constructing new models of set theory by extending an already known model, the ground model, in a carefully chosen way as to allow for a considerable amount of control over the structure and truths of the extension model. The technique has revolutionized the field of set theory, leading to far-reaching applications and an abundance of new models of ZFC. This relation between a ground model and its forcing extensions has led to the notion of the set-theoretic multiverse, a rich hierarchy of set-theoretic universes. Its structure has been studied by means of a forcing interpretation of the modalities □ and ♢. For a model M of set theory we interpret M |= □φ as “in every forcing extension φ holds” and M |= ♢φ as “in some forcing extension φ holds”.
  
  In this talk I will outline to what extend we know the modal validities of forcing. This question was first investigated in a paper by Hamkins and Löwe (2007), in which a full description of the ZFC-provable propositional modal principles was given. I will also report on an ongoing joint project with Hamkins and Löwe to generalise this result to predicate modal principles.
• October 30th 4.30pm: Sven Manthe (Bonn), A decidability result on a restricted monadic theory of order
  
  Abstract: The monadic second-order theory of order of the naturals (S1S) is decidable (it essentially describes ω-automata). However, by a result of Shelah and Gurevich, for the reals the theory is undecidable. In this series of talks we will discuss decidability if quantification is restricted to Borel sets (or alternatively, under the axiom of determinacy). The first talk is concerned with basic results on monadic theories, giving some context to the result, and basic tools of descriptive set theory needed for the proof.
• November 6th: Philip Dittmann (Dresden), Model theory of finitely ramified henselian valued fields
  
  Abstract: Henselian valued fields are a class of structures whose model theory has been much investigated. After an introduction to this area, I will present recent joint work with Anscombe and Jahnke in the finitely ramified setting. No prior knowledge of valued fields will be assumed.
• November 7th 10.15am-11am N0.008 Neubau: Sven Manthe (Bonn), A decidability result on a restricted monadic theory of order (Part II)
• November 13th: Nima Rasekh (MPIM Bonn), Formalizing (Double) Categories
  
  Abstract: In recent years formalization of mathematics has experienced a meteoric growth with applications ranging from computing stable homotopy groups of spheres to condensed mathematics. In this talk we will focus on the formalization of categorical concepts and in particular surprising mathematical challenges that one encounters in the univalent setting. If time permits I will also discuss ongoing joint work with Benedikt Ahrens, Paige North and Niels van der Weide aimed at generalizing this formalization to double categories. No significant knowledge of type theory, formalization or proof assistants will be assumed for this talk and mathematicians of all stripes are welcome to attend!
• November 14th 10.15am-11.45am N0.008 Neubau: Sven Manthe (Bonn), A decidability result on a restricted monadic theory of order (Part III)
• November 20th: Leon Chini (Bonn), Model companions of o-minimal theories with a rational vector space homomorphism
  
  Abstract: Let T be a first-order theory, which defines a non-trivial Q-vector space in every model, and T_theta := T \cup {"theta is a homomorphism of said vector space"}. We also consider certain extensions T^C_theta of T_theta, which enforce that the kernels of some endomorphisms of the form f[theta] = \sum_{i=0}^d (f_i) theta^i satisfy certain equations. I will state a sufficient condition under which a model companion for each T^C_theta exists, and roughly outline the steps for a proof. By previous work of Block Gorman, said condition holds in certain o-minimal Theories, which include Th(R, 0, +, <) with the additive group as a vector space and RCF with the multiplicative group on the positive elements as a vector space. If time permits, I will present some results obtained for the respective model companions in these cases.
• November 21th 10.15am-11.45am N0.008 Neubau: Sven Manthe (Bonn), A decidability result on a restricted monadic theory of order (Part IV)
• November 27th: No seminar
• November 28th 10.15am-11.45am N0.008 Neubau: Sven Manthe (Bonn), A decidability result on a restricted monadic theory of order (Part V)
• December 4th: No seminar
• December 5th 10.15am-11.45am N0.008 Neubau: Sven Manthe (Bonn), A decidability result on a restricted monadic theory of order (Part VI)
• December 11th: Gabriel Dill (Bonn), Distinguished categories and the Zilber-Pink conjecture
  
  Abstract: The Zilber-Pink conjecture is a very general statement that implies many well-known results in diophantine geometry, e.g., Manin-Mumford, Mordell-Lang, and André-Oort. I will report on recent joint work with Fabrizio Barroero in which we proved that the Zilber-Pink conjecture for a complex abelian variety A can be deduced from the same statement for its trace, i.e., the largest abelian subvariety of A that can be defined over the algebraic numbers. This gives some unconditional results, e.g., the conjecture for curves in complex abelian varieties (over the algebraic numbers this is due to Habegger and Pila) and the conjecture for arbitrary subvarieties of powers of elliptic curves that have transcendental j-invariant. While working on this project, we realized that many definitions, statements, and proofs were formal in nature and we came up with a categorical setting that contains most known examples and in which (weakly) special subvarieties can be defined and a Zilber-Pink statement can be formulated. We obtained some conditional as well as some unconditional results.
• December 18th: No seminar
• January 8th: No seminar
• January 15th: No seminar
• January 22th: Peter Koepke (Bonn), A Natural Language Formalization of Perfectoid Rings in the Proof Assistant Naproche
  
  Abstract: The formalization of P. Scholze's perfectoid spaces in the Lean proof assistant by K. Buzzard, J. Commelin, and P. Massot has been a milestone in bringing formal mathematics closer towards leading research-level mathematics. Whereas the Lean text is not "readable" in the ordinary sense, the Naproche natural language proof checker aims for proof-checked mathematical formalizations that read like standard mathematical texts. We present a Naproche formalization of perfectoid rings which are main components of perfectoid spaces. The Naproche formalization is a LaTeX file perfectoid_rings.ftl.tex which can be read as a pdf printout, or it can be loaded and edited in the well-known Isabelle prover platform where it will be proof-checked automatically by the inbuilt Naproche component.
• January 29th: Leonardo Cano (Universidad Nacional de Colombia), About the pullback of families of first order structures and natural semantics
  
  Abstract: The talk is about results obtained in collaboration with Pedro Zambrano. We remark that the pullback of structures is well defined but that forcing is incompatible with it. We study other semantics naturally defined for families of structures (over fiber bundles) with respect to its compatibility with pullback and finally we associate to a Ehresmann connection (which of course involves differential geometry) a semantics which is compatible with the pullback. For this semantics the observer plays a defining role and this semantics distinguishes two extensions of the true: the horizontal, that we think of as the spatial-temporal extension; and the vertical, which we think of as associated with the accuracy of our tools of measurement.