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 axi

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.