Workshop on inductive definitions

Invitation pdf

Workshop on inductive definitions

An inductively defined domain is a domain whose elements may be thought of as having been generated in a stepwise fashion. Standard examples are the natural numbers, the words over some alphabet, and the constructive ordinals. Over an inductively defined domain, functions may be defined by induction on the structure of the elements. Both forms of inductive definition are central to mathematics. In constructive mathematics, in particular, they are usually treated as primitive forms of definition. In this workshop, both conceptual and technical aspects of inductive definitions will be discussed. 

Programme

Thursday 2 May

-------

10.00 Introduction by Ansten Klev (Prague)

11.00 Peter Dybjer (Gothenburg) – Inductive definitions, predicativity and the Mahlo Universe

14.00 Laura Crosilla (Florence) – Predicativity as invariance

15.30 Mark van Atten (Paris) – Intuitionistic inductive definitions

Friday 3 May

------

9.30 Thierry Coquand (Gothenburg) – Inductive definitions and constructive mathematics

11.00 Øystein Linnebo (Oslo) – Inductive definitions and Weyl's notion of extensional determinateness

14.00 Ulrik Buchholtz (Nottingham) – TBA

15.30 Wilfried Sieg (Pittsburgh) – Methodological frames: Mathematical structuralism and proof theory

The workshop will be broadcast via Zoom. Write Tato e-mailová adresa je chráněna před spamboty. Pro její zobrazení musíte mít povolen Javascript. for the link.
The talks by Van Atten and Sieg will be exclusively via Zoom. 

Generously funded by a Lumina quaeruntur grant (LQ300092101) from the Czech Academy of Sciences.