Teaching

Content

The lecture began with the basics of logic and set theory, in particular relations: functions, equivalence relations and orders, together with quotient structures and hence well-definedness. It continued with abstract groups, rings and fields, and only then turned to vector spaces, going up to and including the spectral theorem for self-adjoint matrices. I took time to motivate each new concept and to discuss how its definition can be understood; the definition of a vector space alone filled a whole lecture.

The notes go a little further than the lecture: they also contain the spectral theorem for normal operators, historical remarks and an appendix.

Format

Every week there was an exercise sheet, worked on at home in groups of one to three students, and an exercise class with further exercises solved together. The exercise class and the correction of the sheets were taken care of by colleagues.

The Two Versions of the Notes

In the colour version every block sits in a coloured box, so that one sees at a glance where a block ends, which helps when looking something up:

• guiding examples (Leitbeispiele): orange
• examples: yellow
• definitions: green
• remarks: red
• theorems, propositions, lemmas and the like: blue
• proofs: purple

The black-and-white version leaves out the boxes, for printing, for e-ink displays, or simply for less visual noise. Without the boxes the layout changes, so page numbers differ between the two versions; when referring to a page, please mention which version you use.

Licence

The notes are licensed under CC BY-NC-SA 4.0: you may use, share and adapt them for non-commercial purposes, as long as you credit me, indicate what you changed, and publish adaptations under the same licence. They were written with the help of AI. The semester is over, but I am happy to correct and update the notes; please write to me if you find a mistake.

Content

The lecture began with the definition of a topological space by open sets and compared it with the equivalent descriptions by closed sets, by the Kuratowski closure axioms and by Hausdorff’s neighbourhood axioms. It then treated convergence, continuity and sequential continuity, bases, subbases and neighbourhood bases, and the construction of new topologies as initial and final topologies, in particular product, trace and quotient topologies.

The second part was about separation and countability axioms: Hausdorff, regular and normal spaces, Urysohn’s lemma, and first and second countability.

The third part was about compactness: compactness in general and in first-countable spaces, the Cantor intersection theorem, the Alexandroff compactification, filters and ultrafilters, Tychonoff’s theorem, the Stone–Čech compactification, and nets and subnets. Excursions showed compactness at work outside topology, for instance the compactness theorem of propositional logic, and the fact that the Riemann integral, as a map on the integrable functions from [0,1] to [0,1] with the topology of pointwise convergence, is sequentially continuous but not continuous. An appendix of the notes collects the facts about metric spaces that the lecture uses.

Format

Before a proof was presented, students were invited to propose their own ideas, and we discussed intuitive arguments that fail and why they fail. Some sessions were given over entirely to discussion exercises. Four problem sheets of varying difficulty were set as homework.

Day 1: Lambda Calculus and Simple Types

• Untyped lambda calculus: terms, substitution, alpha equivalence, beta and eta reduction, normal forms and the Church–Rosser theorem; Church encodings of the Booleans and the natural numbers; fixed-point combinators, recursion and undecidability.
• Simply typed lambda calculus: contexts and typing rules, typing derivations and untypable terms; uniqueness of types, subject reduction, progress, strong normalization and the decidability of definitional equality.

Day 2: More Type Formers

• Type formers: formation, introduction, elimination and computation rules, and Gentzen’s harmony between them.
• Product, unit, sum and empty types.
• Meta-theory: confluence, subject reduction, strong normalization and canonicity of the extended calculus, and from these its consistency.

Day 3: Intuitionistic Logic and Curry–Howard

• Intuitionistic logic: the Brouwer–Heyting–Kolmogorov interpretation, the law of excluded middle and natural deduction.
• Curry–Howard correspondence: propositions are types, proofs are programs, and proof normalization is evaluation.
• Consequences: consistency of intuitionistic propositional logic, the disjunction property and the unprovability of the excluded middle.

Day 4: System F, Dependent Types and Lean

• System F: the type former ∀, polymorphism, second-order propositional logic through Curry–Howard, and impredicativity.
• Dependent types: Π-types and Σ-types, the conversion rule and universes; Curry–Howard for dependent type theory and the lambda cube.
• First inductive types: the Booleans and the natural numbers.
• How Lean differs from the ideal picture: strong normalization fails, definitional equality is undecidable, and consistency is shown by models.

Day 5: Inductive Types

• General inductive types and how they give products, sums, the Booleans, the natural numbers and more.
• The equality type, and with it a proof of the Peano axioms for the natural numbers.
• The general recursor and the strict positivity condition.

Topics

• Syntax and semantics of predicate logic
• The axioms of Zermelo–Fraenkel set theory (two talks), including which of them follow from the others; my addendum shows why the axiom of replacement does not
• Ordinal numbers
• Construction of the natural numbers, the Peano axioms, transfinite induction and ordinal arithmetic
• Cardinal numbers and their arithmetic
• Construction of the real numbers by Dedekind cuts
• The axiom of choice (two talks): equivalent forms, applications, independence from ZF and Vitali’s theorem
• The axiom of regularity: the cumulative hierarchy and von Neumann rank

Literature

• T. Jech, Set Theory, Springer, 3rd edition, 2000.
• O. Deiser, Einführung in die Mengenlehre, Springer, 2004 (a PDF is available on the author’s homepage).
• T. Tantau, Einführung in die Logik, lecture notes, University of Lübeck, winter term 2017/18.

• Analysis 1 (lecture by T. Jäger), winter term 2023/24: homework tutorial and exercise class
• Fractal Geometry (lecture by T. Jäger), summer term 2023: exercise class
• Topology (lecture by T. Jäger), winter term 2022/23: exercise class
• Mathematics pre-course for new students, October 2020
• Exam preparation weekends of the student representatives, early 2019 and early 2020
• Measure Theory (lecture by M. Neumann), winter term 2019/20: exercise class
• Linear Algebra 1 (lecture by B. Külshammer), winter term 2018/19: exercise class