When the principle of omniscience just holds.
Abstract: Without assuming excluded middle, in constructive mathematics one may prove that plenty of infinite sets X satisfy the principle of omniscience, which gives a logical counter-part of the topological notion of compactness, generalizing constructive notions of finiteness. The principle says that it is decidable whether any given 2-valued function on X has a zero or not. We examine this in the context of Martin-Löf type theory, touching some concepts of Univalent Foundations (UF). In particular, we discuss the role of two different notions of constructive existence present in UF. We provide new methods of constructing omniscient sets, involving the injectivity of the universe of types and a certain "micro Tychonoff Theorem" that asserts the closure of omniscient types under products indexed by a subsingleton. The omniscient types we obtain turn out to be ordinals with the property that every non-empty decidable subset has a least element. They are countable in a weak sense.
Descriptive Set Theory of Topological Equivalence Relations
Abstract: Borel reducibility equips the set of all equivalence relations (ER) on Borel subsets of Polish spaces with a partial order structure. Since many mathematical object classes (countable models, separable Banach spaces, C*-algebras and Polish spaces themselves) can be coded as Borel subsets of Polish spaces, this theory provides tools for the analysis of the complexity of classification problems. In this talk I will present some recent results on topological ERs: A knot is an embedding of a circle into R^3 and two knots are equivalent if there is a homeomorphism of R^3 taking one to the other. This ER is induced by a Polish group action, but is not classifiable by countable structures. The homeomorphism relation on subsets of R^3 which are the union of an open set and a point is strictly above the universal ER induced by a Polish group action (UERPG). This is in a sense best possible, because the homeomorphism on locally compact spaces has exactly the same complexity as UERPG. A major part of the latter result is due to Sabok, Zielinski, Kechris and Solecki. I conclude with a list of open questions in this area.
"Type theory as a language for homotopy theory": what does it mean, really?
Abstract: Around ten years ago, the discovery of rich connections between type theory and homotopy-theoretic settings (by Hoffmann-Streicher, Voevodsky, Awodey-Warren, and others) sparked off the programme of work known as homotopy type theory or univalent foundations . Since then, slogans like "type theory is the logic of homotopy theory" and "homotopy type theory is the internal language of infinity-toposes" have been widely bandied around; but their precise status has not always been clear. I will survey the different things these could or should mean — some heuristic, some precise; some conjectural, some now established. This will include (among other things) recent work of Kapulkin, Shulman, Cisinski, and myself.
Independence, the Continuum Hypothesis, and the nature of infinity
Abstract: The modern mathematical story of infinity began in the period 1879-84 with a series of papers by Cantor that defined the fundamental framework of the subject. Within 40 years the key ZFC axioms for Set Theory were in place and the stage was set for the detailed development of transfinite mathematics, or so it seemed. However, in a completely unexpected development, Cohen showed in 1963 that even the most basic problem of Set Theory, that of Cantor's Continuum Hypothesis, was not solvable on the basis of the ZFC axioms. The 50 years since Cohen's work has seen a vast development of Cohen's method and the realization that the occurrence of unsolvable problems is ubiquitous in Set Theory. This arguably challenges the very conception of Cantor on which Set Theory is based. Thus a fundamental dilemma has emerged. On the one hand, the discovery, also over the last 50 years, of a rich hierarchy of axioms of infinity seems to argue that Cantor's conception is fundamentally sound. But on the other hand, the developments of Cohen's method over this same period seem to strongly suggest there can be no preferred extension of the ZFC axioms to a system of axioms that can escape the ramifications of Cohen's method. But this dilemma was itself based on a misconception and recent discoveries suggest there is a resolution.
February 18, 2016, Erik Palmgren. Email: palmgren [at] math (dot) su {dot} se