Interpreting a proof of $2^mathbb{N}$ being uncountable

Question

Suppose I have the following proof:
open import Agda.Builtin.Equality
open import Data.Nat.Base

data ⊥ : Set where

data ? : Set where
  I : ?
  O : ?

inv : ? → ?
inv I = O
inv O = I

invNeq : ∀ d → d ≡ inv d → ⊥
invNeq I ()
invNeq O ()

data Idx : Set where
  at : ℕ → Idx

ℝ : Set
ℝ = Idx → ?

_≈_ : {a b : Set} → (f₁ f₂ : a → b) → Set
_≈_ f₁ f₂ = ∀ x → f₁ x ≡ f₂ x

diagEx : (f : ℕ → ℝ) → ℝ
diagEx f (at n) = inv (f n (at n))

doesn'tBelong : (f : ℕ → ℝ) → (n : ℕ) → (f n ≈ diagEx f) → ⊥
doesn'tBelong f n funEq = invNeq (f n (at n)) (funEq (at n))

We encode real numbers as functions from natural numbers to binary digits, then (in diagEx), given some mapping f from natural numbers to reals (or, rather, some subset of those), we build a function that doesn't belong to said mapping, and then prove (in doesn'tBelong) that, for any mapping f, there exists a function (built by diagEx f) that isn't equal to any real number enumerated by the f. This, of course, includes f's claiming to be surjective, so that's largely the diagonal argument for proving uncountability of reals. Yay!
Or at least that's the intent of the proof. But what have we really proven? Could it be that we've only proven that there doesn't exist a terminating numbering of reals? Or a computable one?
My concern is that we're working in some language, and said language only allows terminating functions (modulo some irrelevant details, but even with them it's about computable functions). On the other hand, we don't rely on the computational behaviour of f at all, so, in theory, this f could be postulated (or, stretching it a little, it could even go ahead and consult some external oracle about each next digit without making the system inconsistent, I guess).
So what's the power of this proof? What's the right tool to reason about this kind of questions? It feels related to model theory, but I have very passing familiarity with that subject.

Dan Doel · Accepted Answer

There is no assumption in your proof that the functions involved are computable, so it would be quite stingy to interpret the proof that way merely because Agda allows you to compute with its terms.
Rather, yes how it should be interpreted depends on the model, and constructive (in the sense of just removing axioms) proofs like the one you've given enable an even wider range of models. So it applies to classical functions, because we can (I believe) interpret all the operations you used as operations on classical functions. It's just that when those operations are used to combine classical functions, they don't produce computable functions, even though the operations are in a sense computable.
When you do interpret the proof in a computable setting, what you get is actually a stronger result. The classical reading is, "the reals (or, Cantor space really for your example) are uncountable." The computable reading is, "the computable reals are computably uncountable." The latter means that we can actually compute a real that is left out of any alleged computable enumeration.
A good write up of this is here, although it applies equally well to types that aren't inductive, even though the title doesn't emphasize it. The first part of the author's thesis also gives a pretty good description of modest sets, which are a way of thinking about the 'computable operations on non-computable data' angle.
So, don't make the mistake of thinking that Agda and the like are only for reasoning about their own terms. It's an easy mistake to make coming from a computer programming background, but I think it's a mistake even there.
The reason why is your oracle example. One could imagine a model where there is an extra $?^ℕ$ sequence added as a sort of brute fact (also all sequences computable from it, of course). When you ask about its bits, the computer accesses some sort of physical sensor and determines the answer based on that (and memoizes it). This bit sequence is not 'computable' in the sense of being described by some term, but as long as you haven't added axioms that depend on bit sequences being describable by terms, your proofs should hold for it. So this sort of 'open world' assumption seems to match aspects of actual computers.

Andrej Bauer · Answer

Agda has an interpretation in classical set theory, as well as in realizability models.
Any proof carried out in Agda is valid in any of these models. It can therefore be interpreted in classical set theory to give a proof of uncountability of $2^mathbb{N}$, but it can also be interpreted in the effective topos to give a proof of computable uncountability of computable total maps.
Just because a theory does not allow you to exhibit a non-computable map, that does not imply that it can only speak about computable maps. To give an analogy: the definition of a group only mentions the unit element specifically, but this does not mean that every group is trivial.
P.S. Please do not call $2^mathbb{N}$ "reals" because this is not the case anywhere, except in set theory (and even there I would argue this is an abuse of terminology).

Interpreting a proof of $2^mathbb{N}$ being uncountable

2 Answers

Add your own answers!

Ask a Question