Earlier quoted context omitted.
You don't need to implement a diagonalisation in order to prove results about it - this is true for computers as much as it is true for humans. There are formalisations of Godel's theorems in Lean, for instance. Similarly for arguments involving excluded middle and other non-constructive axioms. I hear your point that humans reason with heuristics that are "outside" of the underlying formal system, but I don't know o…
what is the basic intuition of how godel's theorem are proven in Lean? I understand OP's point of diagonalization proof being impossible to prove on a computer. (Did I get this right?)
In mathematics we often use language to talk about a hypothetical function without actually implementing it in any specific programming language. Formal proofs do exactly the same thing in their own formal language.
Although in the case of Cantor's diagonal argument, I don't know in what sense any function involved in that proof would even fail to be implementable in a specific programming language,. Let's say I encode each real number x such that 0
from typing import Callable
# PosInt, Zero and One aren't built-in Python types but just assume they are
Number = Callable[[PosInt], Zero | One]
Sequence = Callable[[PosInt], Number]
def diagonalize(sequence: Sequence) -> Number:
def diagonal(n: PosInt) -> Zero | One:
if sequence(n)(n) == 0:
return 1
else:
return 0
return diagonal
This is just a simple logical argument---it wouldn't be too hard to write it down explicitly as a natural deduction tree where each step is explicitly inferred from previous one using rules like modus ponens, but I'm not going to bother doing that here.