3 ms·

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. Incid

by 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.
    - btilly 3y ago
      I have no argument with Coq. I do argue that your chosen definition entirely misses the point of what I was saying. Specifically this definition. Definition Real := nat -> Digit My definition of a Real is NOT a function from a nat to a Digit. It is a program that is SUPPOSED TO return a Digit when it gets a nat. Where "supposed to" means that there is a proof in the axiom system saying that it will. This does not mean it actually will return a digit. Our axiom system might be broken. But we can claim to have a proof from our axiom system that it will. Given an enumeration of such programs, a program representing your diagonalized function can be created. Your proof demonstrates that IF it always returns a Digit, THEN it will produce output that is different from anything on the list. But does it always return a Digit? Just as before, maybe, maybe not. The new program waits on another program, and the other program might not return a Digit. Before we could claim to have a proof in the axiom system that our program would return a digit. We now have less than that. What we now have is a proof that there is a proof in the axiom system that it will return a Digit. A proof of a proof is not actually a proof from the axiom system. What we have does represent a proof in (axiom system + consistency of axiom system) that it will return a Digit. But this is a strictly weaker claim than we had before. And it is weaker by the fact that we now need a new axiom. Namely the axiom of the consistency of our previous axiom system. And consistency is necessary because we have to deal with the reference to the axiom system introduced through diagonalization. If you still doubt, please don't bother arguing with me. Go ask your neighborhood mathematical logician. Then argue with them. You've clearly decided that I don't know what I'm talking about. But you haven't decided that of them, so they still have a chance.
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?"

by btilly 3y ago

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.
  - btilly 3y ago
    I have no argument with Coq. I do argue that your chosen definition entirely misses the point of what I was saying. Specifically this definition. Definition Real := nat -> Digit My definition of a Real is NOT a function from a nat to a Digit. It is a program that is SUPPOSED TO return a Digit when it gets a nat. Where "supposed to" means that there is a proof in the axiom system saying that it will. This does not mean it actually will return a digit. Our axiom system might be broken. But we can claim to have a proof from our axiom system that it will. Given an enumeration of such programs, a program representing your diagonalized function can be created. Your proof demonstrates that IF it always returns a Digit, THEN it will produce output that is different from anything on the list. But does it always return a Digit? Just as before, maybe, maybe not. The new program waits on another program, and the other program might not return a Digit. Before we could claim to have a proof in the axiom system that our program would return a digit. We now have less than that. What we now have is a proof that there is a proof in the axiom system that it will return a Digit. A proof of a proof is not actually a proof from the axiom system. What we have does represent a proof in (axiom system + consistency of axiom system) that it will return a Digit. But this is a strictly weaker claim than we had before. And it is weaker by the fact that we now need a new axiom. Namely the axiom of the consistency of our previous axiom system. And consistency is necessary because we have to deal with the reference to the axiom system introduced through diagonalization. If you still doubt, please don't bother arguing with me. Go ask your neighborhood mathematical logician. Then argue with them. You've clearly decided that I don't know what I'm talking about. But you haven't decided that of them, so they still have a chance.

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?"