## Oberseminar mathematische Logik

### Organizers

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

### Time and location

Tuesdays 10-12 in room 1.007, 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

- 20 April, 10:15-12:00, SR N0.008: Steffen Frerix and Peter Koepke (Bonn) Text-Orientated Formal Mathematics

The System for Automated Deduction (SAD) by Andrei Paskevich accepts and proof-checks input texts written in nearly natural mathematical language, without explicit system commands or prover commands. Making practical improvements of the checking algorithm and extending the input language we have been able to efficiently process considerably longer and interlinked texts which are immediately readable by mathematicians. This suggests an approach to formal mathematics through texts in (a controlled) natural language which makes use of natural language features like soft typing by noun phrases to guide text processing and proof checking. In our talk we shall present various aspects of the enhanced SAD system and present working example texts.

- 08 May: Ana Njegomir (Bonn) Characterizing large cardinals through Neeman's pure side condition forcing

Using Neeman's pure side condition forcing, we characterize certain large cardinal properties through the validity of combinatorial principles in its generic extensions. In other words, an uncountable regular cardinal possesses some given large cardinal property if and only if a certain combinatorial principle holds for this cardinal in the corresponding generic extension. In order to do this we use the concept of internal large cardinals. In this way, we characterize various types of large cardinals, such as inaccessible, Mahlo, Pi^m_n-indescribable for all 0<m,n<omega, subtle, ineffable, lambda-ineffable for certain lambda and supercompact cardinals. In this talk, I will present our characterization of Mahlo cardinals. This is joint work with Peter Holy and Philipp Lücke.

- 29 May: Marlene Koelbing (Wien) Generalized Laver Forcing

Do forcings which add a κ-dominating real (i.e., an element of the generalized Baire space κ^{κ}that is eventually above all ground model elements) also add a κ-Cohen real? I show that this is indeed the case for a large class of forcing notions, among them all Laver type forcings on κ^{<κ}. This is very different from the classical setting where it is easy to add dominating reals without adding Cohen reals, e.g., by ordinary Laver forcing. This is joint work with Yurii Khomskii, Giorgio Laguzzi and Wolfgang Wohofsky.

- 13 June, 10:15-12:00, SR N0.008: Andrei Paskevich (Paris) FORmal THEory Language, its syntax and semantics

The modern proof assistants are systems with elaborate logical foundations, input languages, and proof development tools. This creates a considerable barrier for newcomers, even for those experienced in formal mathematics. In this talk, we present an atypical tool whose primary objective was to lower this barrier: by using the elements of natural language in its input, by adopting traditional "declarative" style of proof, and by hiding the specifics of the back-end verifier.

We describe a formal language called ForTheL that imitates the natural language and style of "human" mathematical texts. This language is used as the input language of SAD, a proof assistant intended for automated proof verification. We show that ForTheL allows for terse and comprehensible formalizations and describe its syntax and semantics with respect to verification.

- 19 June: TBA

- 26 June: Stefan Hoffelner (Münster) The Π
^{1}_{3}-uniformization property

The question of whether definable subsets of the plane have a definable choice function is an old, well-studied one, which has led to a very rich theory connecting descriptive set theory with large cardinals and determinacy of infinite games.

We will show that there is a universe in which the Π^{1}_{3}-uniformization property holds, i.e. every Π^{1}_{3}-definable subset of the plane has a Π^{1}_{3}-definable choice function. The proof will use a forcing construction with the constructible universe L as a ground model and will preserve CH. The developed ideas can be applied to higher projective levels and yield the currently best known upper bounds in terms of large cardinal strength. Also there is a natural extension of the argument to the generalized Baire space. This is joint work with S.D. Friedman

- 03 July: TBA

- 10 July: TBA

- 17 July: Boriša Kuzeljević TBA