Infinite sets that satisfy the principle of omniscience in constructive type theory

Martín Escardó

School of Computer Science
University of Birmingham

Friday, 26 May 2017, 16:00 (note the unusual weekday and time!)
Cybernetica Bldg (Akadeemia tee 21B), room CYB-101

Slides from the talk [pdf]

Abstract: We exhibit infinite types X that have a procedure (Π(p:X →2).(Π(x:X).p(x)=0)+(Σ(x:X).p(x)=1)). Among them, several are ordinals (sets X equipped with transitive, well-founded, extensional relations) and the above procedure finds minimal witnesses when they exist. That is, this class of ordinals satisfies that every detachable, non-empty subset has a minimal element. As an example, we exhibit such a searchable ordinal dominating ε0, although it is possible to get much higher searchable ordinals indeed, which we sketch. This requires either assuming that p is extensional wrt to a setoid structure on X, or else having function extensionality, as in univalent type theories such as cubicaltt. An unplanned connection with the delay monad arises in this investigation.

Tarmo Uustalu
Last update 26 May 2017