Oberseminar mathematische Logik

Organizers

• Prof. Dr. Peter Koepke
• Dr. Philipp Lücke

Time and location

Tuesdays 10-12 in room N0.003, or by appointment (see below), Endenicher Allee 60.

The participants of the seminar are welcome for coffee and tea in the Hausdorffraum at 10.00 before the talks.

Talks

• 12 October (10.30 -12.00, SR N0.007): Makarius Wenzel (Augsburg) Isabelle as IDE for Formal Mathematical Documents
  
  Conventionally, Isabelle is understood as a platform for interactive theorem proving. The standard Isabelle/HOL library provides theories and tools for specifications and proofs in simply-typed set-theory. Isabelle/HOL applications are collected in the online journal "Archive of Formal Proofs" (AFP), where articles consist of formal document source that is checked by Isabelle and printed via PDF-LaTeX.
  
  Thus we may further understand Isabelle as Integrated Development Environment (IDE) for documents with arbitrary formal content, combined with informal text. Isabelle allows to define new sub-languages in user-space, with semantic editor support included by default: the standard logical language is an example for that.
  
  Here we shall particularly explore support for Formal Mathematical Documents. Mixed languages and tools are implemented in Isabelle/ML, Isabelle/Scala or as external programs; the integration with Isabelle provides some formality to existing backends like BibTeX. There is also a perspective towards document rendering in HTML/CSS, with instantaneous preview inside the IDE.
  
• 16 October: Philipp Lücke (Bonn) Tree forcings at higher cardinals
  
  Classical work of Sacks shows that there exists a ω-tree forcing that is ^ωω-bounding, i.e. there is a non-atomic partial order P consisting of subtrees of ^<ω2 of height ω ordered by inclusion with the property that, given a condition T in P and a node t in T, the subtree of T consisting of all nodes comparable with t is again a condition in P and every function from ω to ω in a P-generic extension is bounded by a function in the ground model. Kanamori showed that a partial orders with analogous properties exists for inaccessible cardinals. In this talk, I want to present some consequences of the existence of a ^κκ-bounding κ-tree forcing for an uncountable regular cardinal κ. These results will show that the Bounded Proper Forcing Axiom implies the non-existence of such partial orders for ω₁.
  
• 23 October: Peter Holy (Bonn) Small models and large cardinals
  
  Most strong notions of large cardinals, starting from measurability upwards, are characterized through the existence of certain class sized elementary embeddings having the large cardinal in question as their critical point. Weaker large cardinals, for example weakly compact or Ramsey cardinals, can often be characterized in terms of elementary embeddings between models the size of the large cardinal. Classical results from Kunen, Kleinberg and others show that several smaller large cardinals can also be characterized through the existence of certain filters over countable models of set theory. We will show that these results, perhaps unsurprisingly, also have embedding analogues, however using embeddings with target models that are not necessarily well-founded, and we also consider extensions of these results to domain models that are not necessarily countable, but only smaller than the large cardinal that is to be characterized. We thus characterize regular cardinals, inaccessible cardinals and completely ineffable cardinals. This is based on joint work with Niels Ranosch and Philipp Schlicht.
  
• 30 October (10.00-11.30): Aleksandra Kwiatkowska (Münster) Infinite permutation groups
  
  We discuss several results on infinite permutation groups, that is, closed subgroups of the symmetric group on a countable set, or equivalently, automorphism groups of countable structures. We will focus on ample genericity, where a topological group G has ample generics if for every n, the diagonal conjugacy action of G on Gⁿ has a comeager orbit, on similarity classes, and on topological generators of permutation groups. For example, we show that for a permutation group G, under mild assumptions, for every n and an n-tuple f in G, the countable group generated by f is discrete, or precompact, or the conjugacy class of f is meager. Finally, we will focus on automorphism groups of structures equipped with a definable linear order, such as the ordered random graph, the ordered rational Urysohn metric space, the ordered random poset, the ordered random boron tree, and many other extremely amenable permutation groups. In particular, we give new examples of such groups which have a comeager conjugacy class. This is joint work with Maciej Malicki.
  
• 06 November: Robert Passmann (Amsterdam) The de Jongh Property for a Subtheory of CZF
  
  After recalling intuitionistic logic, Kripke semantic, and (Heyting) algebra-valued models for set theory, we will introduce the notions of loyalty and faithfulness: An algebra-valued model is called loyal if its propositional logic is the propositional logic of its underlying algebra; it is called faithful if all elements of the underlying algebra are truth values of sentences in the language of set theory in the model. We will then analyse the loyalty and faithfulness of a particular construction of Kripke models of set theory due to Iemhoff, and, by using classical models of ZFC set theory and the forcing technique, prove the de Jongh property for the constructive set theory CZF^* satisfied by Iemhoff’s models, i.e., for any propositional formula φ(p₀,...,p_n-1) with propositional letters p₀,...,p_n-1, it holds that intuitionistic logic IPC proves φ(p₀,...,p_n-1) if and only if CZF^* proves φ(ψ₀,...,ψ_n-1) for all set theoretical sentences ψ₀,...,ψ_n-1. More precisely, we show that CZF^* has the de Jongh property with respect to every logic that can be characterised by a class of Kripke frames.
  
• 20 November: André Nies (Auckland) Topological isomorphism for classes of closed subgroups of the group of permutations of ℕ
  
  The closed subgroups of the group of permutations of ℕ coincide with the automorphism groups of structures with domain ℕ. We consider natural Borel classes of such groups, such as being profinite (each orbit is finite), or being oligomorphic (for each k there are only finitely many k-orbits). We work towards classifying the complexity of their isomorphism relation in the sense of Borel reducibility.
  
  For each class, work with A. Kechris and K. Tent (J. Symb. Logic, in press) shows that the topological isomorphism relation is Borel below the isomorphism relation among countable graphs. For the class of profinite groups, we show that this bound is sharp. On the other hand, for oligomorphic groups, work with Schlicht and Tent from this year shows that the isomorphism relation is below a Borel equivalence relation with only countable classes, and hence much lower than graph isomorphism. A lower bound, other than the identity relation on the set of reals, remains unknown.
  
• 04 December: Sandra Müller (Wien) Structural properties of the Stable Core
  
  The Stable Core 𝕊, introduced by Sy Friedman in 2012, is a proper class model of the form (L[S],S) for a simply definable predicate 𝕊. He showed that V is generic over the Stable Core (for 𝕊-definable dense classes) and that the Stable Core can be properly contained in HOD. These remarkable results motivate the study of the Stable Core itself. In the light of other canonical inner models the questions whether the Stable Core satisfies GCH or whether large cardinals is V imply their existence in the Stable Core naturally arise.
  
  In a joint work with Sy Friedman and Victoria Gitman we give some answers to these questions and show that GCH can fail at all regular cardinals in the Stable Core. Moreover, we show that measurable cardinals in general need not be downward absolute to the Stable Core, but in the special case where V = L[μ] is the canonical inner model for one measurable cardinal, the Stable Core is in fact equal to L[μ].
  
• 15 January: Gunter Fuchs (New York) Beschränkte Forcing-Axiome und die Erhaltung von breiten Aronszajn-Bäumen
  
  Ich werde über Verbindungen zwischen zwei Eigenschaften einer Klasse Γ von Forcings sprechen. Einerseits geht es um das bekannte (ω₁,κ)-beschränkte Forcing-Axiom für diese Klasse, das von Goldstern und Shelah für proper forcing eingeführt wurde. Die andere Eigenschaft ist der Erhalt von Aronszajn-Bäumen der Höhe ω₁ und Breite κ. Ich werde zeigen, dass unter der Voraussetzung, dass κ=κ^ω ist und Forcings in Γ keine neuen abzählbaren Teilmengen von κ hinzufügen, diese beiden Eigenschaften äquivalent sind. Die Klasse der Forcings, die Jensens Eigenschaft der subcompleteness erfüllen, ist eine kanonische Klasse, die keine reellen Zahlen hinzufügt, und ein Korollar des obigen Resultats ist, dass das (ω₁,2^ω)-beschränkte Forcing-Axiom für subcomplete Forcings äquivalent ist zum Erhalt von Aronszajn-Bäumen von Höhe ω₁ und Breite 2^ω. Dies verallgemeinert ein gemeinsames Resultat mit Kaethe Minden. Ich werde dann einige weitere Resultate und offene Fragen zum Erhalt von Aronszajn-Bäumen der Höhe ω₁ und anderen Breiten diskutieren.
  
• 19 March (10.30 -12.00, SR 1.007): Sean Cox (Richmond) Martin's Maximum and the Diagonal Reflection Principle
  
  Several years ago I introduced the Diagonal Reflection Principle (DRP), a maximal form of simultaneous stationary reflection. Roughly, DRP asserts that for all regular θ > ω₁, there are stationarily many sets W of size ω₁ such that every stationary element of W reflects to W (i.e. if S ⊂ [θ]^ω is stationary and S ∈ W, then S ∩ [W ∩ θ]^ω is stationary). In that paper I showed that that MM^+ω₁ -- even just the '+ω₁' version of the forcing axiom for σ-closed forcings -- implies DRP. In this talk I will prove that MM, even its technical strengthening MM^+ω, does NOT imply DRP, contrary to my initial expectations. This is joint work with Hiroshi Sakai.