Abstract
Based on jww Sam Sanders
Inspired by results due to Martín Escardó we can see that a set X ⊆ 𝟚^ℕ admits a quantifier ∃x ∈ X(P(x)), computable in some f ∈ ℕ^ℕ and working for all predicates P, if and only if X is closed and countable. These quantifiers can be seen as functionals of type 3 computable in some f. For classical applications of quantifiers in real analysis we must go beyond this, make use of quantifiers normally represented by the functionals ∃²(∃n⁰) or ∃³(∃f¹), where the first is too weak for most purposes in ordinary mathematical analysis while the latter is far too strong.
In the NorSan project we consider partial quantifiers, subfunctionals of ∃³, and consider for how complex predicates P we need an oracle answering questions of the sort ∃f(P(f)). This is in analogy with how comprehension axioms are used in Reverse Mathematics.
In this talk we will survey some of the old results, and then discuss some recent observations relating the classes Fσ, Gδ and Fσ ∩ Gδ of subsets of reals. For the first two classes, we will need the axiom of choice to select a Borel code for each element of the class while for the third one we can select one computably in a very modest partial functional of type 3.
There will be some focus on motivation and on the foundational impact.
Talk Details
Speaker: Dag Normann (University of Oslo, Norway)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Thursday 18 December 2025
Time: 14:50 (remote)
Key Topics
- Higher-order functionals
- Quantifiers in analysis
- Reverse mathematics
- Borel hierarchy
- F-sigma and G-delta sets
- Comprehension axioms
- Type theory
- Computability theory
Collaborators
- Sam Sanders (NorSan project)