## Oberseminar mathematische Logik

### Organizers

- Prof. Dr. Peter Koepke
- Dr. Peter Holy
- Dr. Philipp Lücke

### Time and location

Monday 16.30-18.00 in room 0.007, Endenicher Allee 60.

The participants of the seminar are welcome for coffee and tea in the Plückerraum 1.012 at 16.00 before the talks.

### Talks

**09.11.2015**Peter Holy (University of Bonn) -- Forcing lightface definable wellorders without the GCH

(joint work with David Aspero and Philipp Lücke)**16.11.2015**Ana Njegomir (University of Bonn) -- Thin-very tall compact scattered spaces

In this talk we will introduce the notion of thin-tall compact spaces and introduce a forcing which preserves all cardinals and forces the existence of such a space. We follow the unpublished paper by M.A. Mota and W. Weis.**23.11.2015**Aleksandra Kwiatkowska (University of Bonn) -- Homeomorphism groups of spaces with many symmetries and their universal minimal flows

I will talk about compact and connected metric spaces, which are universal and ultrahomogeneous and about their homeomorphism groups. Then I will focus on the homeomorphism group of the Lelek fan and compute its universal minimal flow. This is joint work with Dana Bartosova.**30.11.2015**Sheila Miller (City University of New York) -- The quandary of quandles: a Borel complete knot invariant

The isomorphism type of the knot quandle introduced by Joyce is a complete invariant of tame knots. Whether two quandles are isomorphic is in practice difficult to determine; we show that this question is provably hard: isomorphism of quandles is Borel complete. The class of tame knots, however, is trivial from the perspective of Borel equivalence, suggesting that a less complex complete invariant of tame knots likely exists.**Friday 04.12.2015, 10:00 - 11:30, room 2.008**Markus Makarius Wenzel -- Intelligible semi-automatic reasoning in December 2015.

Isabelle was introduced in 1989 (by L. Paulson) as a generic logical framework for higher-order natural deduction. Intelligible semi-automated reasoning (Isar) was introduced in 1999 (by M. Wenzel) as a structured proof language for human-readable formal proof documents. Today, in December 2015, we see large applications of Isabelle/Isar in the Isabelle/HOL object-logic, e.g. in the Archive of Formal Proofs (http://afp.sf.net) with more than 240 entries.

After so many years, development of Isar is still not finished. Recent refinements of old concepts and additions of new concepts include: structured rule statements (Eigen-contexts), multi-branch elimination (case-splitting), structured backwards refinement. The new Eisbach language (by D. Matichuk et al) allows to define complex proof methods in their usual syntax, instead of traditional Isabelle/ML. Sledgehammer (by J. Blanchette et al) allows to generate semi-intelligible Isar proofs from machine-generated proofs (via external ATPs and SMTs).

The ultimate aim of Isabelle/Isar is to turn the results of formal proof production into mathematical documents with nice type-setting. Document source was mainly written in LaTeX in the past, but is now moving towards Markdown, with specific GUI support in the Prover IDE (Isabelle/jEdit).**Friday 04.12.2015, 16:30 - 18:00, room 0.007**Ralf Schindler (University of Münster) -- PFA^-

We isolate a new forcing axiom, PFA^-, which is strictly between BPFA and PFA. PFA^- is equiconsistent with a remarkable cardinal, it implies the failure of \square_{\omega_1}, but it is compatible with \square_\kappa for all \kappa\geq\omega_2.**07.12.2015**Regula Krapf (University of Bonn) -- Characterizations of Pretameness

The notion of pretameness was introduced in order to characterize the preservation of the axioms of ZF^- under class forcing. We will give some new characterizations of pretameness in terms of several properties which always hold in the context of set forcing but may fail in class forcing, such as the preservation of Separation, the forcing theorem and the existence of nice names. This is joint work with Peter Holy and Philipp Schlicht.**11.01.2016**Wolfgang Wohofsky (University of Hamburg) -- No large sets which can be translated away from every Marczewski null set

We will show the following (ZFC) theorem which is recently finished work joint with Joerg Brendle: There is no set of size continuum which is "s_0-shiftable", i.e., which can be translated away from every set in the Marczewski ideal s_0 (where a set of reals is in s_0 if for every perfect set there is a perfect subset disjoint from it). For regular continuum, the proof is easier, and we will go through it in detail. If there is time left, we will also discuss the singular case. The theorem is very much in contrast to the respective situation when s_0 is replaced by the meager ideal: there are models (e.g., all models that satisfy CH) with large meager-shiftable (i.e., strong measure zero) sets.**Friday 15.01.2016, 16:30 - 18:00, room 0.007**Chris Le Sueur (University of Münster) -- Determinacy a bit beyond co-analytic and class Prikry forcing with M-ultrafilters

It is a well known result that 0-sharp is equivalent to co-analytic determinacy, and a less well-known result that 0-dagger is equivalent to (omega^2+1)-Pi^1_1 determinacy, a level of the difference hierarchy on the co-analytic sets. I will show some results just below the latter level using weaker hypotheses. The methods are remarkable for using a combination of results provable in systems much weaker than ZFC and tools from inner model theory and forcing, ultimately requiring large cardinal strength. The forcing is particularly interesting because of this: in the weak setting it is a class forcing, and proving the forcing theorem is a challenge requiring an unusual solution.**18.01.2016**Philipp Lücke (University of Bonn) -- Ascending paths and forcings that specialize higher Aronszajn trees

One of the most basic questions asked about set-theoretical trees is the question whether they contain a cofinal branch. Special trees are important examples of trees without cofinal branches, because the non-existence of cofinal branches through such trees is absolute in a strong sense. In this talk, I want to consider properties of trees that cause them to be non-special in an absolute way.**25.01.2016**David Schrittesser (University of Copenhagen) -- Maximal discrete sets with large continuum

In recent joint work with Asger Törnquist, we showed how to construct definable maximal discrete sets in forcing extensions of L, in particular in the Sacks and Miller extension. In particular, the existence of such sets is consistent with V ≠ L. In this talk I shall show the stronger result that the existence of definable discrete sets is consistent with large continuum. In the process, I show an interesting generalization of Galvin's theorem. In particular, this applies to the example of maximal orthogonal families of measures (mofs). One might hope for a simpler way of constructing a mof in a model with large continuum: to find an indestructible such family in L. While such an approach is possible e.g. for maximal cofinitary groups, this is impossible for mofs.**01.02.2016, 10:30 - 12:00, room N0.003**Benno van den Berg (University of Amsterdam) -- Constructive set theory - an overview

I will give an overview of the area of constructive set theory, with special emphasis on Harvey Friedman's IZF (for intuitionistic Zermelo-Fraenkel set theory) and Peter Aczel's CZF (for constructive Zermelo-Fraenkel set theory).**Friday 05.02.2016, 16:30 - 18:00, room 1.007**Maciej Malicki (Warsaw School of Economics) -- Polish groups and the notion of ample generics

I would like to discuss some of my recent results on Polish groups in the context of the notion of ample generics. Recall that a Polish group G has ample generics if all its diagonal conjugation actions have a comeager orbit. This property has very interesting and strong consequences such as the automatic continuity property (i.e. every homomorphism from G into a separable group is continuous), the small index property (i.e. every subgroup H < G with [G: H] < c is open), and uncountable cofinality for non-open subgroups (i.e. there are no countably infinite exhaustive chains of non-open subgroups in G.) First of all, I will discuss the existence of ample generics in the context of isometry groups of Polish ultrametric spaces. Then I will say a little about proving the main consequences of the existence of ample generics, when ample generics themselves are not present (i.e. for the isometry group of the Urysohn space or the unitary group). Finally, I will give examples of Polish groups with ample generics that fail to be non-archimedean.