#import "@preview/touying:0.6.1": *
#import themes.dewdrop: *
#show link: underline
#show math.equation: box // prevent line breaks in the middle of equations

#show: dewdrop-theme.with(
  aspect-ratio: "16-9",
  navigation: none,
  config-info(
    title: [The countable reals],
    author: [Exposition by Jean Abou Samra \ (Eötvös Loránd University, Budapest) \ of work by Andrej Bauer and James E. Hanson: \ _The countable reals_, #link("https://arxiv.org/abs/2404.01256")[arXiv:2404.01256]
    ],
    date: [November 10th 2025],
  ),
)


#title-slide()


== Introduction

Cantor proved that $ℝ$ is uncountable in two ways.

First proof: Take $u : ℕ → ℝ$. Construct nested intervals

$ [x_0, y_0] ⊇ [x_1, y_1] ⊇ [x_2, y_2] ⊇ ⋯ $

such that $[x_n, y_n]$ avoids $u_n$. Then $u$ misses any point in the intersection, so is not surjective.

== Introduction

Construction: cut $[x_n, y_n]$ in three equal parts $[x_n, a_n], [a_n, b_n], [b_n, y_n]$ and set

$ [x_(n+1), y_(n+1)] = cases([x_n, a_n] "if" u_n > a_n, [b_n, y_n] "if" u_n < b_n) $

#pause

Constructively, we can obtain “if $a_n < b_n$ then $u_n > a_n$ or $u_n < b_n$”, but “$u_n > a_n$ or $u_n ≤ a_n$” is the analytic limited principle of omniscience, a constructive taboo.

#pause

Alternatively, use dependent choice: If for all $s$ there exists $s'$ such that $R(s, s')$ then there is a sequence $(s_n)$ such that $R(s_n, s_(n+1))$.

#pause

Or, by making all choices in advance, just countable choice: If for all $n ∈ ℕ$ there exists $s$ such that $R(n, s)$ then there exists $f$ such that $R(n, f(n))$.

== Introduction

Second proof: Take $u : ℕ → 2^ℕ$. The sequence $n ↦ "flip"(u_(n)(n))$ is not in the image of $u$.

Constructively valid, but proves that $2^ℕ$ is uncountable, a different theorem!

Building the decimal expansion of a real requires the analytic limited principle of omniscience “$x ≥ y$ or $x < y$” again.

== Which flavor of constructive mathematics?

Technically: the internal language of an “elementary 1-topos with natural numbers object”. Traditionally higher-order logic, but can model extensional type theory as well.

#pause

Practically speaking:

- Constructive
- Impredicative: type $Ω$ of truth values, powerset of $A$ is $Ω^A$
- Quotients and propositional truncation
- Equality reflection, function extensionality, propositional extensionality, unique choice

#pause

Terminological points:

- Existence means mere existence ($∃$ not $Σ$).
- A set $X$ is *inhabited* when there exists an element in it ($‖X‖ ≡ ∃ x : X, ⊤$).
- A truth value $p ∈ Ω$ is *decidable* when $p ∨ ¬p$ (→ decidable subset, decidable equality), and *classical* when $¬¬p ⇒ p$.

== Countability in constructive mathematics

$X$ is *countable* when there is a surjection $ℕ → X+1$.

If a countable set surjects into $X$ then $X$ is countable.

A countable union $⋃_(i ∈ I) A_i$ can be rewritten as $⋃_(n ∈ ℕ) B_i$.

#pause

$X$ is *subcountable* when there is an injection $X → ℕ$.

A countable set may contain an uncountable subset! Countability and subcountability are unrelated constructively.

#pause

Bauer previously exhibited a model where $ℝ$ and even $2^ℕ$ are subcountable.

== The real numbers in constructive mathematics

The construction of the field $ℚ$ is unproblematic. It is countable and has decidable equality and ordering.

Three constructions of $ℝ$ from $ℚ$:

- Cauchy reals: using Cauchy sequences to “add missing limits” in $ℚ$. Sub-variants: quotient in one go, or add sequences and quotient them at the same time, quotient-inductive-inductively.

- Dedekind reals: next slide.

- MacNeille reals: a different order completion construction. Always uncountable, but “$x < 1$ or $x > 0$” not provable.

#pause

Even classically, it is interesting to consider all three because they generalize in different ways: Cauchy reals → $p$-adic numbers, Dedekind reals → surreal numbers, MacNeille reals → Dedekind-MacNeille completion of a poset.

== The Dedekind reals

Intuition: Represent $r ∈ ℝ$ by $L := {x ∈ ℚ | x < r}$ and $U := {x ∈ ℚ | x > r}$.

A *Dedekind cut* is a pair $(L, U)$ such that:

- $L$ is inhabited, i.e., $‖L‖$
- $L$ is downwards-closed, i.e., for all $y ∈ ℚ$, if there exists $x ∈ L$ such that $y < x$, then $y ∈ L$
- $L$ is open, which in view of downwards-closedness is equivalent to the converse: if $y ∈ L$ then there exists $x ∈ L$ such that $y < x$
- Symmetrically, $U$ is inhabited and $y ∈ U ⇔ (∃ x ∈ U, x < y)$
- $L$ is below $U$: if $x ∈ L$ and $y ∈ U$ then $x < y$
- $L$ and $U$ are located: if $x < y$ then $x ∈ L$ or $y ∈ U$

== Realizability

The counter-model is a variant of realizability models.

Curry-Howard: A proof is a program… #pause in an expressive typed programming language with propositions-as-types

#meanwhile Realizability: A proof is a program… #pause in a model of computation that may be completely untyped

#pause

A “Curry-Howard model” is just a syntactic model/term model.

A realizability model is more complicated: sets with computational representations, maps which have a computational counterpart

Realizability was invented by Kleene in 1945, \~25 years earlier than Curry-Howard. Variants: Dialectica (Gödel), linear realizability, classical realizability, …

#pause

Realizability can work with a very general class of models of computation: models of a variant of the SKI combinator calculus where application is a partial operation.

== Partial combinatory algebras

Let $A$ be a set with a partial operation $A × A ⇢ A$. An expression is, inductively, a variable, a constant or the application of an expression to an expression.

$A$ is a partial combinatory algebra when for all expression $e$ in variables $x_0, …, x_n$, there exists $a ∈ A$ such that for all $a_0, …, a_n ∈ A$:

1. $a a_0 … a_(n-1) a_n ≃ e[a_0\/x_0, …, a_n\/x_n]$ where $≃$ means one is defined iff the other is, and then they have the same value
2. $a a_0 … a_(n-1)$ is defined

#pause

Reason for (2): $p ∧ q ⇒ r$ implies $p ⇒ q ⇒ r$ intuitionistically, so we need currification that gives a defined function if we apply it with fewer arguments.

#pause

For SKI fans, this is equivalent to having $k, s ∈ A$ such that $k a b = a$, $s a b c = a c (b c)$ and $s a b$ defined.

== Examples of partial combinatory algebras

Fundamental example: “Kleene's first algebra” $𝒦_1$ is $ℕ$ — Gödel codes of Turing machines — with application by execution of Turing machines

More pcas:

- Untyped λ-terms
- Better: every model of the untyped λ-calculus
- Infinite-time Turing machines, used to make $ℝ$ and $2^ℕ$ subcountable
- Turing machines with a fixed oracle

== The maze of higher-order computability

Giving a computational interpretation to higher-order logic involves some choices.

What is a computable function $ℕ → ℕ$? Answered by the pca, e.g., Church-Turing model.

What is a computable function $2^ℕ → ℕ$? Several ideas:

#pause

- A Turing machine which receives a program and is guaranteed to terminate provided that the program defines a total function $f : ℕ → 2$
- Same, but the output must only depend on $f$, not on the program (→ function extensionality)

#pause

- A Turing machine with an oracle
- A Turing machine with an oracle, but only required to terminate provided the oracle is computable (not equivalent!!)

#pause

What is a computable function $(2^ℕ → ℕ) → ℕ$?

== Assemblies

The primary object in realizability is an assembly: A set $X$ together with a realizability relation $⊩$ between the pca $A$ and $X$, where $a ⊩ x$ is read “$a$ realizes $x$”, such that every $x$ is realized by some $a$.

Basic assembly: $ℕ$ where $⌈n⌉$ realizes $n$.

== Assemblies

In the category of assemblies over $A$, the exponential $X^Y$ is made of functions $Y → X$ which are realized, where $a$ realizes $f$ when for every $x$ and for every $b$ realizing $x$, the application $a b$ is defined and realizes $f(x)$.

#pause

Example:

- $ℕ → ℕ$ is the assembly of computable functions; each $f$ is realized by the Gödel codes of Turing machines computing $f$.
- Elements of $2^ℕ → ℕ$ take computable bit sequences to natural numbers; each $f$ is realized by $a$ when $a$ takes every program computing a bit sequence $u$ to $f(u)$ (no termination guarantee if input does not compute a bit sequence)

#pause

The category of assemblies is quite well-behaved: it has finite limits, finite colimits and exponentials, and it is regular.

But it is not a topos because we lack a notion of truth values.

== Realizability toposes

The realizability topos over a pca $A$ is obtained by a more sophisticated construction with setoid-like objects.

Intuition: The object of truth values $Ω$ is $𝒫(A)$, and to realize equality of truth values $p, q ⊆ A$, we must provide a realizer that converts an element of $p$ to an element of $q$ and vice-versa.

#pause

The effective topos is the realizability topos over $𝒦_1$.

- Internal Church Thesis: every function $ℕ → ℕ$ is computable
- Failure of excluded middle
- Failure of analytic limited principle of omniscience
- All real functions are continuous
- Any non-computably-enumerable subset of $ℕ$ is subcountable but uncountable
- An immune set is neither finite nor infinite (injection from $ℕ$)
- But countable choice!

== Parameterized realizability toposes

If we “adjoin an oracle” to be able to compute a new sequence, diagonalization kicks in and gives us a real not in the sequence.

Idea: introduce parameters into the pca.

Application: oracle Turing machines but parameterized by the oracle.

A function $X → Y$ between assemblies is realized by those $a ∈ A$ such that for all $x$, for all $b$ realizing $x$, and for _all_ parameter $p$, the application $a ⋅_p b$ is defined and realizes $f(x)$.

== The Miller sequence construction

Notion of oracle representing a real when it encodes a sequence of rationals rapidly converging to the real (rapidly = specified modulus of convergence). Oracle representing a sequence of reals.

Miller sequence: A sequence $μ : ℕ → [0, 1]$ such that if $x$ is a real and $n$ is a program representing $x$ when given _any_ oracle representing $μ$, then actually $x$ appears in $μ$.

Construction uses Kakutani's fixed point theorem, a generalization of Brouwer's fixed point theorem. Very classical: in the effective topos, there exists a map from the unit square to itself that moves every point by a positive distance.

In the parameterized realizability topos where oracles are those which represent a given Miller sequence, the reals are countable!