4 ms·

Ironically, Cantor's argument falls apart in constructivism.

by btilly 3y ago

Tainnor 3y ago
Cantor's argument shows that there exists no surjective map from the natural numbers to the reals and that proof is valid constructively. So the proof still works, it just has a different interpretation.
- btilly 3y ago
  My point is that it DOES have a different interpretation. In particular, we don't interpret it as saying that there are somehow fundamentally more reals. Incidentally the "exists no surjective map" interpretation may or may not be correct, depending on the exact choice of definitions. Here is how it can be false. Suppose that we define a function f in some programming language to be a real if it can be proven from a specific set of axioms that f(n) is always a rational, and that |f(n) + f(m)| is always less than or equal to 1/n + 1/m. Let's call those axioms, ASSUME. It is now straightforward to write a program that maps the natural numbers onto the reals. Just do a breadth-first search for all proofs from ASSUME that some function f represents a real. Given n, we return the program that is the subject of the n'th such proof. It is also straightforward to do Cantor's diagonalization argument. But proving that the resulting function produces an output for every n requires proving that ASSUME is consistent. Which, as Gödel pointed out, hopefully doesn't follow from ASSUME. And therefore the construction does not result in a real by the chosen definition. (When we start thinking carefully about reasoning, we find that there is an important difference between "X proves" and "X proves that X proves".)
  - Tainnor 3y ago
    The diagonalisation argument shows that if f is a total function i: N -> j: N -> [0..9] (which calculates the j-th digit of the i-th real number), then g j = (f j j + 1) % 10 is a total function N -> [0..9] and has the property that for all i there exists a j, such that f i j /= g j. To me, that's an entirely constructive proof that there is no (computable) surjective map from the integers to the (computable) reals, but if you disagree, then I guess that's just a debate about definitions. I have no idea what Gödel has to do with any of this or why you think we would have to prove some axioms consistent. We don't have to prove our axioms consistent to do mathematics, thankfully, because that would be impossible.
    - btilly 3y ago
      The problem is that you are cavalierly throwing around terms like "f is a total function" instead of the more careful, "this set of axioms proves that f is a total function". Diagonalization adds a level of self-reference which may require that you use stronger axioms to prove that if is a total function. That is not due to a question of definitions or constructivism. This is a point of mathematical logic that most pay little attention to. Namely proving that you prove something is not the same as proving it. And the difference between those two is the question of whether you are consistent. Suppose that I have a list of axioms, which I'm calling ASSUME. If you want, pick ZFC as the axioms, doesn't matter. Suppose that I have a program P that takes any positive integer as input and produces an output in finite time. So I get a list P(1), P(2), P(3) and so on. You can model this mathematically in various ways. Gregory Chaitin's version of LISP is particularly nice for this. But any Turing-complete programming language will work. Suppose that by the construction of my program, each P(i) comes with a proof from ASSUME showing that it will take an positive integer as input, and produce a rational number as output. For any given i, we can find that associated proof. Then using ASSUME we can verify that proof and prove that P(i)(1), P(i)(2), P(i)(3), ... is a sequence of rational numbers. The surprise from mathematical logic is that ASSUME generally does NOT prove that the following is a sequence of rational numbers: P(1)(1), P(2)(2), P(3)(3), ... The reason is that we have shown: > ASSUME proves that for each i, there is a proof from ASSUME that P(i)(i) is well-defined. To prove that P(i)(i) is well-defined, we need to inspect the i'th proof. But proving it for every i requires something strong, like that ASSUME is consistent. And therefore proving that the function f produced by diagonalization is total generally requires a stronger set of axioms than the ones needed to prove things about each item on the list.
      - Tainnor 3y ago
        > 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.
  - cvoss 3y ago
    > define a function f in some programming language to be a real if it can be proven from a specific set of axioms that... Fine, but these programs only comprise constructive reals. Similarly, with my choice of Real := Nat -> Digit, there are only countably many functions you could actually (create a process to) write down which inhabit that type, but that doesn't make the type countable. There are at most countably many programs one can access in any type. This follows from what programs are: finite (though arbitrarily long) strings over a finite alphabet. That doesn't refute other interesting properties about the "sizes" of these things, as given by the existence or non-existence of certain maps into and out of other types.
    - btilly 3y ago
      And the age-old debate. The classical mathematician says, "...but those are only the constructive reals. What about the rest?" The constructivist says, "What rest? The ones that don't exist?"

Ironically, Cantor's argument falls apart in constructivism.

by btilly 3y ago

Ironically, Cantor's argument falls apart in constructivism.

Cantor's argument shows that there exists no surjective map from the natural numbers to the reals and that proof is valid constructively. So the proof still works, it just has a different interpretation.

btilly 3y ago
My point is that it DOES have a different interpretation. In particular, we don't interpret it as saying that there are somehow fundamentally more reals. Incidentally the "exists no surjective map" interpretation may or may not be correct, depending on the exact choice of definitions. Here is how it can be false. Suppose that we define a function f in some programming language to be a real if it can be proven from a specific set of axioms that f(n) is always a rational, and that |f(n) + f(m)| is always less than or equal to 1/n + 1/m. Let's call those axioms, ASSUME. It is now straightforward to write a program that maps the natural numbers onto the reals. Just do a breadth-first search for all proofs from ASSUME that some function f represents a real. Given n, we return the program that is the subject of the n'th such proof. It is also straightforward to do Cantor's diagonalization argument. But proving that the resulting function produces an output for every n requires proving that ASSUME is consistent. Which, as Gödel pointed out, hopefully doesn't follow from ASSUME. And therefore the construction does not result in a real by the chosen definition. (When we start thinking carefully about reasoning, we find that there is an important difference between "X proves" and "X proves that X proves".)
- Tainnor 3y ago
  The diagonalisation argument shows that if f is a total function i: N -> j: N -> [0..9] (which calculates the j-th digit of the i-th real number), then g j = (f j j + 1) % 10 is a total function N -> [0..9] and has the property that for all i there exists a j, such that f i j /= g j. To me, that's an entirely constructive proof that there is no (computable) surjective map from the integers to the (computable) reals, but if you disagree, then I guess that's just a debate about definitions. I have no idea what Gödel has to do with any of this or why you think we would have to prove some axioms consistent. We don't have to prove our axioms consistent to do mathematics, thankfully, because that would be impossible.
  - btilly 3y ago
    The problem is that you are cavalierly throwing around terms like "f is a total function" instead of the more careful, "this set of axioms proves that f is a total function". Diagonalization adds a level of self-reference which may require that you use stronger axioms to prove that if is a total function. That is not due to a question of definitions or constructivism. This is a point of mathematical logic that most pay little attention to. Namely proving that you prove something is not the same as proving it. And the difference between those two is the question of whether you are consistent. Suppose that I have a list of axioms, which I'm calling ASSUME. If you want, pick ZFC as the axioms, doesn't matter. Suppose that I have a program P that takes any positive integer as input and produces an output in finite time. So I get a list P(1), P(2), P(3) and so on. You can model this mathematically in various ways. Gregory Chaitin's version of LISP is particularly nice for this. But any Turing-complete programming language will work. Suppose that by the construction of my program, each P(i) comes with a proof from ASSUME showing that it will take an positive integer as input, and produce a rational number as output. For any given i, we can find that associated proof. Then using ASSUME we can verify that proof and prove that P(i)(1), P(i)(2), P(i)(3), ... is a sequence of rational numbers. The surprise from mathematical logic is that ASSUME generally does NOT prove that the following is a sequence of rational numbers: P(1)(1), P(2)(2), P(3)(3), ... The reason is that we have shown: > ASSUME proves that for each i, there is a proof from ASSUME that P(i)(i) is well-defined. To prove that P(i)(i) is well-defined, we need to inspect the i'th proof. But proving it for every i requires something strong, like that ASSUME is consistent. And therefore proving that the function f produced by diagonalization is total generally requires a stronger set of axioms than the ones needed to prove things about each item on the list.
    - Tainnor 3y ago
      > 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.
- cvoss 3y ago
  > define a function f in some programming language to be a real if it can be proven from a specific set of axioms that... Fine, but these programs only comprise constructive reals. Similarly, with my choice of Real := Nat -> Digit, there are only countably many functions you could actually (create a process to) write down which inhabit that type, but that doesn't make the type countable. There are at most countably many programs one can access in any type. This follows from what programs are: finite (though arbitrarily long) strings over a finite alphabet. That doesn't refute other interesting properties about the "sizes" of these things, as given by the existence or non-existence of certain maps into and out of other types.
  - btilly 3y ago
    And the age-old debate. The classical mathematician says, "...but those are only the constructive reals. What about the rest?" The constructivist says, "What rest? The ones that don't exist?"