Hacker News Reader

> Diagonalization adds a level of self-reference which may require that you use stronger axioms to prove that if is a total function.

Sorry, but this is nonsense.

Here's a proof of my argument in Coq (without any extra axioms) which is based on constructive logic (and yes, I'm ignoring the fact that some sequences of digits are the same real number and everything before the decimal point etc. pp. for simplicity's sake):

  Require Import Coq.Init.Nat.

  Inductive Digit :=
    | Zero | One | Two | Three | Four | Five | Six | Seven | Eight | Nine.

  Definition succ (d : Digit) : Digit := match d with
    | Zero => One | One => Two | Two => Three | Three => Four | Four => Five | Five => Six
    | Six => Seven | Seven => Eight | Eight => Nine | Nine => Zero
    end.

  Theorem d_succd : forall (d : Digit), d <> succ d.
  Proof.
  intros d.
  destruct d; discriminate.
  Qed.

  Theorem feq_each : forall {A} {B} (f g : A -> B), f = g -> forall (x : A), f x = g x.
  Proof.
  intros A B f g hyp x. rewrite hyp. reflexivity. Qed.

  Definition Real := nat -> Digit.

  Definition Seq (A : Type) := nat -> A.

  Definition not_includes {A} (s : Seq A) (e : A) := forall (i : nat), s i <> e.

  Theorem diag : forall (l : Seq Real), exists (g : Real), not_includes l g.
  Proof.
  intros l.
  remember (fun x => succ (l x x)) as g.
  exists g.
  intros i.
  intros contra.
  specialize ((feq_each (l i) g) contra).
  intros contra'.
  specialize (contra' i).
  rewrite Heqg in contra'.
  revert contra'.
  apply d_succd.
  Qed.

If you're going to argue with Coq, then whatever, but this is as constructivist as it gets.

Edited to add that a proof of essentially the same theorem can be found in Bishop's "Foundation of Constructive Analysis" (in my edition, page 25), with explicit reference to Cantor.

View on HN

def is_even (n): return n % 2 == 0 def collatz (n): i = 0 while n != 1: i += 1 if n % 2 == 0: n = n // 2 else: n = 3 * n + 1 return i def collatz_is_even (n): return is_even(collatz(n))

def found_boolean_seq (code): # If proof proves that <code> returns a function seq which always # returns a Boolean when passed a natural number, will return code # as a string. # # Otherwise it returns None. ....

def boolean_seqs (X): # A list that will include every function that X proves defines a # boolean sequence. All functions that X can prove this about will # be somewhere in the sequence. # # This returns them as closures. # for proof in proofs(X): code = found_boolean_seq(proof) if code is None: yield lambda n: False else yield eval(code, {}) def boolean_seq (X, n): # Returns the n'th boolean sequence from boolean_seqs. # # This returns it as a closure. i = 0 for f in boolean_seqs(X): i += 1 if i == n: return f

def diagonalize (X): # Returns a sequence that disagrees with every other one on our list. def inner (n): return not boolean_seq(X, n)(n) return inner # Do some work to set up the axiom system X ... # And return the diagonalized sequence. diagonalize(X)