module Padova2025.Explorations.Uncountability.Impossible where
Seemingly impossible programs and proofs
open import Padova2025.ProgrammingBasics.Booleans open import Padova2025.ProvingBasics.Connectives.Disjunction open import Padova2025.ProvingBasics.Connectives.Existential open import Padova2025.ProvingBasics.Negation open import Padova2025.ProvingBasics.Equality.Base open import Padova2025.ProvingBasics.Equality.General import Padova2025.ProvingBasics.Equality.Booleans as B
A root of a decidable predicate P : X → Bool is
a value x : X such that P x ≡ false (as with
roots of ℕ-valued functions). Let us call a type
X searchable iff every decidable predicate
P : X → Bool has a root or alternatively is constantly
true.
Searchable : Set → Set Searchable X = (P : X → Bool) → (∃[ x ] P x ≡ false) ⊎ ((x : X) → P x ≡ true)
In classical mathematics, every type is trivially searchable. But as
long as we do not postulate classical mathematics, this searchability
condition expresses in Agda a much stronger claim—namely that, given a
predicate P, we can decide by means of an
algorithm which alternative holds.
Equivalent (for inhabited types) is the following property related to the drinker paradox.
HasDrinkers : Set → Set HasDrinkers X = (P : X → Bool) → ∃[ a ] (P a ≡ true → ((x : X) → P x ≡ true))
false≢true : false ≢ true false≢true ()
HasDrinkers⇒Searchable : {X : Set} → HasDrinkers X → Searchable X
HasDrinkers⇒Searchable = {!!}
Searchable⇒HasDrinkers : {X : Set} → X → Searchable X → HasDrinkers X
Searchable⇒HasDrinkers = {!!}
Exercise: The Booleans are searchable
Finite types such as Bool are searchable: To decide
whether a predicate has a root, we can inspect every element of the type
in turn.
Bool-searchable : Searchable Bool
Bool-searchable P with P false in eq | P true in eq'
... | false | y = {!!}
... | true | false = {!!}
... | true | true = {!!}
There is also a slick proof involving the ideas of the cryptic
is-tautology₁' function from the module on equality
results on Booleans.
Bool-hasDrinkers : HasDrinkers Bool
Bool-hasDrinkers P = P false , {!!}
Infinite yet searchable types?
open import Padova2025.ProgrammingBasics.Lists open import Padova2025.ProgrammingBasics.Naturals.Base open import Padova2025.ProgrammingBasics.Operators open import Padova2025.ProvingBasics.Termination.Gas open import Padova2025.Explorations.Uncountability.Applications
Amazingly, beyond the finite types, there do exist infinite types which are searchable.
In any flavor of constructive mathematics where function extensionality is available, such as Cubical Agda, the “one-point compactification of the natural numbers”, roughly speaking
ℕwith an added point∞, is searchable.In some flavors, even the Cantor space is searchable—its uncountability notwithstanding.
This shocking fact has been thoroughly explored by Martín Escardó. To jump into this fascinating area, have a look at this classic post on Andrej Bauer’s blog, this Agda code or these slides.
A miniature toy version (blithely employing a recursion which will be but cannot be shown to be terminating) is available in the following module.
open import Padova2025.Explorations.Uncountability.Impossible.Toy
This module exports a function
root : (Cantor → Bool) → Maybe List which should either
return just xs with xs the first five terms of
a root of the input predicate (more terms could also be generated as
needed), or nothing in case no root exists. When applied to
predicates defined in the empty context, not using any assumptions or
postulates, the root function always works correctly,
though this meta-assertion is not provable in Agda.
More precisely, the recursion employed be the root
function terminates in case the input function is uniformly continuous.
It is a meta-theorem about certain flavors of Martin-Löf type theory
that every term of type Cantor → Bool in the empty context
is indeed uniformly continuous, and one can entertain the idea that this
result also holds for Agda (which however strictly speaking is
ill-specified). See this note
by Thierry Coquand and Guilhem Jaber for details and the PhD
thesis of Martin Baillon for many new results and pointers to the
literature.
Try it yourself: Fill in the hole as you wish; press
C-c C-v; enter root example; observe the
results. For instance, if examples xs is defined as
not (xs zero) || xs one || not (xs two), then
root example will reduce to
just (true ∷ false ∷ true ∷ false ∷ false ∷ []).
example : Cantor → Bool
example xs = {!!}