4 ms·

You've gotten a lot of thoughtful answers here already. Here's mine. I'll come at it from a constructivist perspective. There is a way to completely define a

by cvoss 3y ago

You've gotten a lot of thoughtful answers here already. Here's mine. I'll come at it from a constructivist perspective. There is a way to completely define a countable list. I do not say that you can completely write the list out in finite time. But you can specify it fully. Write a function f : Nat -> X, where X is the type of the things in the list, such that f is total, i.e., provably halts on every input. Your favorite typed lambda calculus or other theorem proving language will give you this property basically for free. The entire list is encoded as f. It doesn't matter that you can only extract elements one at a time by processing this function. They're all there, well-defined. Now, we use this technique twice in Cantor's argument. First, we suppose the existence of f : Nat -> Real with the property that f covers all the reals. What we mean by that is you cannot define a real, x, such that f i != x for all i. (But we will do so.) Second, each real number is itself encoded as a countable list of digits. So, Real := Nat -> Digit. In some sense, every real number is itself "a process" of digit generation, but you don't need to carry it out. Simply holding the function will suffice. Now, it's kind of tricky to compare reals to see which are equal and unequal, but ignoring the 0.99999... = 1 issue, which can be resolved, a proof that x != y involves identifying just one place i : Nat where the digits disagree: x i != y i. Here we go: define x as x i := (f i i) + 1 mod 10. We claim x witnesses that f doesn't cover the reals. We agreed this means we must show x != f i for all i. We agreed that means finding j such that x j != f i j. The proof we seek: Let j := i. We're just pushing functions around in a suitably typed language. Everything halts, nothing is running forever, no infinite storage space is required to hold the supposed list of reals nor the digits of each real. You can whip this up pretty fast in Lean or Coq etc.

btilly 3y ago
Ironically, Cantor's argument falls apart in constructivism.
- 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.

by cvoss 3y ago

btilly 3y ago

Ironically, Cantor's argument falls apart in constructivism.

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.