3 ms·

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 to

by 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.
  - Tainnor 3y ago
    > You've clearly decided that I don't know what I'm talking about. Yes, by now I'm pretty certain of this.
    - btilly 3y ago
      And I am likewise convinced that you are missing basic connections between computing, Gödel, the halting problem and so on. Last try. Suppose that X is an axiom system that models computation. Since Turing machines can be described in arithmetic, and arithmetic in computation, that's actually equivalent to being able to model arithmetic. But we'll stick with computation. I'll use Python syntax for computation. Both because it is readable, and because it has https://docs.python.org/3/tutorial/classes.html#generators https://docs.python.org/3/tutorial/classes.html#generators, closures, and eval. Which are really convenient for what I'm going to do. Let's look at code that generates a functions that take natural numbers and return Booleans. Some are simple. def is_even (n): return n % 2 == 0 Obviously this always returns a Boolean. Some are more complex. 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)) We don't know that collatz_is_even always returns. It returns a Boolean if it does. But if the Collatz conjecture is false, then some inputs will never return and this isn't a Boolean sequence. Now the following function can obviously be written, but will be somewhat complicated: def proofs (X): # Does a breadth-first search through proofs in first order logic # from axiom system X. Will yield proofs in order. ... Here is another function that can clearly be written, and is also somewhat complicated. 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. .... Based on these we can write the following. 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 And now let's diagonalize to produce a new sequence. 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) OK. If proofs and found_boolean_seq are both correctly written, we can prove from how Python works that every proof from X will show up in proofs(X). And every piece of code that X can prove defines a Boolean sequence will show up in boolean_seqs(X). Now a question. Can the diagonalized sequence show up in boolean_seqs(X)? If X is inconsistent, then it certainly does. X proves anything. Including that that code always returns a Boolean. Next question. If the diagonalized sequence shows up in the n'th position, what will happen if we call seq(n) on it? The answer is that the copy we call will find its own code in the sequence and will eval it. It will then call seq(n) on that copy, which will repeat. By induction we can prove that it will create an unlimited number of copies of itself, which takes forever, so it never returns. But note, If it is on the list, that's because axiom system X proved that it WOULD return. So if it is on the list, then axiom system X is inconsistent. A version of Gödel's theorem follows. If the axiom system X is consistent, then the diagonalized sequence is not on the list. This means that X cannot prove whether or not the diagonalized sequence always returns. Which in turn means that X is incomplete. The fact that I keep pointing out is that cannot prove whether or not the diagonalized sequence always returns. If the axiom system X is consistent, then you need a strictly stronger axiom system than X to prove that the diagonalized function always returns a Boolean. It has to be stronger exactly because proving things about the diagonalized function means that you're proving things about the axiom system X. And that is true of diagonalized computation in general. Diagonalizing creates a layer of self-reference. Which means that you can't always prove things about the diagonalized function, even though you can prove the same thing about each function in the sequence.

by btilly 3y ago

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.
- Tainnor 3y ago
  > You've clearly decided that I don't know what I'm talking about. Yes, by now I'm pretty certain of this.
  - btilly 3y ago
    And I am likewise convinced that you are missing basic connections between computing, Gödel, the halting problem and so on. Last try. Suppose that X is an axiom system that models computation. Since Turing machines can be described in arithmetic, and arithmetic in computation, that's actually equivalent to being able to model arithmetic. But we'll stick with computation. I'll use Python syntax for computation. Both because it is readable, and because it has https://docs.python.org/3/tutorial/classes.html#generators https://docs.python.org/3/tutorial/classes.html#generators, closures, and eval. Which are really convenient for what I'm going to do. Let's look at code that generates a functions that take natural numbers and return Booleans. Some are simple. def is_even (n): return n % 2 == 0 Obviously this always returns a Boolean. Some are more complex. 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)) We don't know that collatz_is_even always returns. It returns a Boolean if it does. But if the Collatz conjecture is false, then some inputs will never return and this isn't a Boolean sequence. Now the following function can obviously be written, but will be somewhat complicated: def proofs (X): # Does a breadth-first search through proofs in first order logic # from axiom system X. Will yield proofs in order. ... Here is another function that can clearly be written, and is also somewhat complicated. 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. .... Based on these we can write the following. 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 And now let's diagonalize to produce a new sequence. 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) OK. If proofs and found_boolean_seq are both correctly written, we can prove from how Python works that every proof from X will show up in proofs(X). And every piece of code that X can prove defines a Boolean sequence will show up in boolean_seqs(X). Now a question. Can the diagonalized sequence show up in boolean_seqs(X)? If X is inconsistent, then it certainly does. X proves anything. Including that that code always returns a Boolean. Next question. If the diagonalized sequence shows up in the n'th position, what will happen if we call seq(n) on it? The answer is that the copy we call will find its own code in the sequence and will eval it. It will then call seq(n) on that copy, which will repeat. By induction we can prove that it will create an unlimited number of copies of itself, which takes forever, so it never returns. But note, If it is on the list, that's because axiom system X proved that it WOULD return. So if it is on the list, then axiom system X is inconsistent. A version of Gödel's theorem follows. If the axiom system X is consistent, then the diagonalized sequence is not on the list. This means that X cannot prove whether or not the diagonalized sequence always returns. Which in turn means that X is incomplete. The fact that I keep pointing out is that cannot prove whether or not the diagonalized sequence always returns. If the axiom system X is consistent, then you need a strictly stronger axiom system than X to prove that the diagonalized function always returns a Boolean. It has to be stronger exactly because proving things about the diagonalized function means that you're proving things about the axiom system X. And that is true of diagonalized computation in general. Diagonalizing creates a layer of self-reference. Which means that you can't always prove things about the diagonalized function, even though you can prove the same thing about each function in the sequence.