Logic seminar: Nicolai Kraus
| Dates: | 14 May 2025 |
|---|
| Times: | 15:00 - 16:00 |
|---|
| What is it: | Seminar |
|---|
| Organiser: | Department of Mathematics |
|---|
| Who is it for: | University staff, External researchers, Adults, Alumni, Current University students |
|---|
|
Title: Constructive Ordinal Arithmetic
Abstract:
Cantor's ordinal numbers can be described as an extension of the natural numbers: 0, 1, 2, ..., omega, omega+1, and so on. Although much larger than the natural numbers, they retain the property that any decreasing sequence is finite. This makes them a tool for showing that functions are well-defined, processes terminate, and for justifying transfinite induction as well as general well-founded inductive proofs.
In a constructive setting, ordinals can sometimes be surprisingly tricky. I will give an overview of constructive ordinal arithmetic and discuss what we can or cannot do [1]. If time permits, I will specifically speak about ordinal exponentiation [2], a topic that is simultaneously confusing and insightful due to observations such as 2^omega = omega.
Much of this work has been carried out in (homotopy) type theory and mechanised in the type theory-based proof assistant Agda. Nevertheless, the ideas work just as well in a generic constructive set theory, and no knowledge of type theory is required to follow the talk.
1 as developed by Escardo and others
2 joint work with de Jong, Nordvall Forsberg, and Xu
Travel and Contact Information
Find event
Frank Adams 1
Alan Turing Building
Manchester
