8 ms·

Gödel's Incompleteness Theorem in Bash

189 points by lacker 5y ago

amluto 5y ago
But this is bash, which runs on Unixy systems, which have exec. behave_differently is trivial: echo foo exec “$@“ This little hack will carry over to some, but possibly not all [0], models of computation. Fixing this would involve cleaning up some definitions in the proof. [0] Specifically, it does carry over to any model of a program that outputs a stream of symbols one at a time. A single-tape Turing machine that computes a function doesn’t work like that.
- assbuttbuttass 5y ago
  What if the program you're running outputs "foo" in an infinite loop? Then I think the above behave_differently would actually behave the same
- KerrickStaley 5y ago
  That does not work. Your example does not change the behavior of the following program: echo foo exec $0
  - dskloet 5y ago
    Your program is very close to the above commenter's program. You could have picked the identical program which is exactly what the proof does.
adamnemecek 5y ago
Godels incompleteness theorems get much more attention than the completeness theorems which are much more interesting. https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...
- slaymaker1907 5y ago
  Unfortunately while valid logical formulas have finite deductions, proving that a formula is not valid (or equivalently that some formula is satisfiable) is Turing complete and thus impossible. So the set of valid first order formulae is recursively enumerable. However, if you limit your scope to finite sets bounded by some size, the problem is merely NP-complete. Given a program, you can construct a formula which is satisfiable iff the program halts (with said formula being polynomial in size with respect to the size of the program).
smitty1e 5y ago
"Any problem in computer science can be solved with another level of indirection."--David Wheeler[0] Which is arguably a re-packaging of Gödel's point: absent a management layer to keep some state concerning the computation, one is in trouble. https://blog.devgenius.io/software-engineering-great-quotes-3af63cea6782 https://blog.devgenius.io/software-engineering-great-quotes-...
automatoney 5y ago
I really like this explanation! It's definitely helpful to see this sort of abstract math idea brought down to super concrete terms. Although I did have a bit of confusion around the "./behave_differently.sh ./my_program.sh ./my_input.txt" part - I expected another layer of concreteness so I was looking for actual outputs (which I realize isn't the point - my_program.sh is supposed to be anything/everything). Other than that though this is a great piece! Short, decently written, and with a good focus but a lot of hints at further things to explore. I guess I'm also not sure about the conclusion - feels a bit like the author's pet issue on how we should teach things, and I feel like that sort of discussion is separate from the article's main focus. I'm more a fan of "here's A different pov on this topic" than "here's THE pov we should teach for this topic"
charcircuit 5y ago
I can implement a basic behave_differently.sh head -c 1024 /dev/urandom paradox.sh paradox.sh will be different than paradox.sh paradox.sh
- geysersam 5y ago
  Not always. ;) Specifically, if my_program.sh outputs some 1024 lines then it is still nonzero probability that your behave_differently.sh does not in fact behave differently.
  - charcircuit 5y ago
    No, there's a 0% chance my implementation outputs 1 as that is only 1 byte long. If you outputted 1023 0s and then a 1 there would be a 2^-1024 chance. That probability is too small to practically happen. The heat death of the universe will happen first.
    - geysersam 5y ago
      You're right that my example was flawed. I've updated it. There is however still nonzero probability that ./behave_differently.sh some_peogram.sh behaves the same as ./some_program.sh
    - shrx 5y ago
      > The heat death of the universe will happen first. No, the heat death might be _more likely_ to happen first, but it's not guaranteed.
  - tromp 5y ago
    One could try to guarantee unique outputs with sleep 1 date but the intended requirement of behave_differently is that it produces different output when run on a computer in exactly the same state. Or equivalently, that the program doesn't depend on the computer state, which is true in the more formal setting of universal Turing machines that start from a fixed state.
eximius 5y ago
Does this actually mirror the incompleteness theorem logic or does it just create an infinite recursive loop? They seem distinct.
- QuercusMax 5y ago
  It's showing that the halting problem is unsolvable, using an infinite recursive loop as an example. The halting problem is related to the incompleteness theorem.
  - BizarroLand 5y ago
    I wonder if it could be solvable by an algorithm that was capable of operating at a higher level. Mayhaps the issue is approaching the problem at the same dimensional level that the problem originated from. After all, humans can come at the problem from a higher cognitive level and, given enough time, resolve that an infinite loop is taking place, so the problem is not fundamentally unsolvable. Einstein said, "No Problem Can Be Solved From The Same Level Of Consciousness That Created It", so it is feasible to assume that, say, a quantum computer running every possible iteration of an algorithm could easily identify which iterations of the algorithm's parameters would induce infinite loops by simple attrition.
    - blackbrokkoli 5y ago
      Yes, definitely. But then the next task is just to solve the incompleteness problem on the level of the higher algorithm, because there must always be incompleteness. Hofstaedter discusses this at length in his book Gödel, Escher, Bach if you are interested in this topic.
- CaptainNegative 5y ago
  It's more or less the same argument. They key additional ingredient in Godel's proof (besides some slight technicality on soundness vs. omega-consistency) is the encoding of an arithmetic interpreter inside of arithmetic itself. That a bash script can run and capture the output of another bash script is pretty obvious, but the first order logic analogue is not nearly as neat and easy. The argument given here is a modern translation of Turing's work in his original paper introducing Turing Machines and the Halting problem, in which he devotes an entire section to the connection between his proof and that of Godel.
Annatar 5y ago
Which practical uses could this have in production?
- maweki 5y ago
  You can explain to your boss that them wanting to check for undecidable properties is impossible. It's important to know what isn't possible, to not throw infinite resources at the problem.
  - bqmjjx0kac 5y ago
    Sometimes probabilistic answers are okay, though.
    - dllthomas 5y ago
      But usually a good idea to understand that that's what you're aiming at producing.
- feintruled 5y ago
  Only preventative measures! One would know enough, for example, not to try to construct a static analysis tool to helpfully tell the user if their code will inadvertently loop infinitely. Imagine running the tool on itself.
- GTP 5y ago
  Maybe a company could decide that developing a tool that, given two programs as imput, tells if those two programs are equivalent would be a great tool to help teams migrate their code to a different programming language (or equivalently migrate to a new version of the same language, like it happened from Python 2.x to Python 3.x). But you can reduce this problem to the halting problem and show that this is not possible. More generally, the halting problem is a great tool to prove that other more practical things are unfortunately impossible to achieve, at least in the general case. But as another commenter pointed out, given a specific problem you could come up with heuristics that work most of the times (but sometimes would not be able to give a conclusive answer)
woolion 5y ago
>His proof is fairly difficult to understand - it involves prime numbers, factorization, all this number theory. Actually, the textbook proof itself is not very different from the presentation in this article, so not hard at all. The difficult part is in formalizing that you can write "a program that proves a program halts". To do so you have to encode it into the language of mathematics, and that is the painful part. To be clear: you have the paradox of the set that contains all sets that don't contain themselves. In naïve set theory, it is trivial to write down formally. However the Berry paradox is not a real paradox because there is no way to encode "The smallest positive integer not definable in under sixty letters". So the whole point of going through the encoding is to show that yes, we can encode what a provable statement, and thus the first 'paradox' is actually a crucial flaw in the mathematical theory, whereas the second is a flaw/paradox in human language, but does not mean anything. The computer world is not as strict, it's more squishy (human?) than mathematics.
- skissane 5y ago
  > However the Berry paradox is not a real paradox because there is no way to encode "The smallest positive integer not definable in under sixty letters". Why is a “way to encode” necessary for a paradox to be “real”? > So the whole point of going through the encoding is to show that yes, we can encode what a provable statement, and thus the first 'paradox' is actually a crucial flaw in the mathematical theory, whereas the second is a flaw/paradox in human language, but does not mean anything. How can you say something “does not mean anything” simply because it cannot be formalised? Since when is formalisability a prerequisite for meaningfulness?
  - woolion 5y ago
    >How can you say something “does not mean anything” simply because it cannot be formalised? Since when is formalisability a prerequisite for meaningfulness? I'm wondering then, what you think is the interest of this theorem? The goal of Gödel was to create a metamathematics. You need to know what is a paradox of the theory or a paradox or not to know if it is correct. If you have a contradiction, you cannot believe anything that the theory proves. So the whole thing is ultimately about separating mathematical paradox from "other types" of paradoxes.
void_one 5y ago
There is a fallacy in constructing "paradox.sh" problem. "behave_differently.sh" requires an argument, a program to be run and produce some output. If "behave_differently.sh" is run without any argument, then there is no specified correct behavior. Thus, "paradox.sh" also requires "$1" to be non-empty, otherwise it's result is undefined. When invoking "./paradox.sh ./paradox.sh", the inner "paradox.sh" will be launched without any arguments, running "behave_differently.sh" also without arguments. There is no logical impossibility, just constructed way to trigger unspecified behavior in "behave_differently.sh".
- OscarCunningham 5y ago
  The second paradox.sh in './paradox.sh ./paradox.sh' isn't run at all. It's soucre gets read in as input to behave_differently.sh.
  - void_one 5y ago
    yes, and then behave_differently.sh runs it to capture and modify its output, but without any arguments
    - OscarCunningham 5y ago
      Note that behave_differently.sh takes two inputs, both a program and the input for that program. Also note that paradox.sh gives both these inputs by using $1 twice. And behave_differently.sh is supposed to be an arbitrary program. It can run the input program but it doesn't have to, it can analyse it in any way it wishes.
      - void_one 5y ago
        It is a good point that behave_differently.sh does not necessary run its argument program, but can analyze it in another way. (The context of Bash scripts suggests execution but that is a misleading hint.) In the broader formulation behave_differently.sh tells that its argument program terminates and produces finite input, which is a halting problem.
born-jre 5y ago
i found this explanation to be easier to grasp `truth alone does not exist or is not valuable without the steps to deduction to that truth (contrary to what mathematician traditionally believed`.
jamesfisher 5y ago
I recently wrote this [1] explanation of the halting problem. I should follow up with this approach to proving the incompleteness theorem! [1]: https://tigyog.app/lessons/fr9uub3hqgab/r/the-halting-problem https://tigyog.app/lessons/fr9uub3hqgab/r/the-halting-proble...
uslic001 5y ago
I was just re-reading this book last night. https://www.amazon.com/G%C3%B6del-Escher-Bach-Eternal-Golden/dp/0465026567/ref=sr_1_1?crid=1X18YL1CX1JSD&keywords=godel+escher+bach&qid=1645802899&s=books&sprefix=godel%2Cstripbooks%2C71&sr=1-1 https://www.amazon.com/G%C3%B6del-Escher-Bach-Eternal-Golden...
- lacker 5y ago
  That book is where I first learned about Gödel's incompleteness theorem. Definitely a good book! I spent a while when I first read it trying to understand Gödel numbering, all the stuff where you multiply prime numbers together, 11 stands for (, that sort of thing. It wasn't until far later that I realized all of that was just a mathematician in the 1930's trying to explain how a string of characters could be encoded as a binary number, something that modern computer programmers more or less take for granted.
qiskit 5y ago
> When Turing proved the halting problem was undecidable - that there is no program that can decide whether another program will ever finish Turing didn't prove the halting problem was undecidable. The halting problem was defined after Turing's death by Martin Davis. It's a common misunderstanding people have. Turing's definition of Turing Machines classified machines that halted as circular/unsatisfactory. Turing wanted his machine to run forever ( circle-free/satisfactory ). > Personally, I think we should set aside Gödel’s original number-theory-based proof as an artifact of history, the way we no longer use Isaac Newton’s original notation for calculus. We also don't teach Turing's version either. No computer science class teaches real Turing. It's been reformulated to a point Turing would barely recognize it. Also, you can't understand the halting problem or Turing without "number-theory-based proof" as "number based proof" and godel numbering is at the heart of turing machines ( look up what descriptive numbers ) are. > We should accept that the concepts of mathematical proof and computer algorithms are intertwined at their heart Computer algorithms are mathematical algorithms. Mathematicians have been using computers/algorithms to derive theorems from axioms since at least the 1950s. You are saying we should accept what everyone already accepts and have accepted for decades.
- JadeNB 5y ago
  > We also don't teach Turing's version either. No computer science class teaches real Turing. It's been reformulated to a point Turing would barely recognize it. I think that this is true of most long-lived subjects taught in a modern science course. Imagine Euclid's puzzlement at all the things that are now called Euclidean! > Also, you can't understand the halting problem or Turing without "number-theory-based proof" as "number based proof" and godel numbering is at the heart of turing machines ( look up what descriptive numbers ) are. Since you say most of what one learns in a CS course isn't directly about Turing's original work, I don't want to speak to that, but I think that it is possible to understand the halting problem, and even its undecidability, without number theory. It arguably isn't possible to understand the halting problem without some notion of encoding (of the data that constitute a Turing machine in a form that can itself be processed by a Turing machine), but there's no reason that encoding has to be number-theoretic. (I speak here as a number theorist—it's a neat application, just much more important for incompleteness than for halting.)
gregfjohnson 5y ago
Here is a hypothetical bash script that neatly characterizes the the impossibility of solving the halting problem: "loop_iff_halts_on_self.sh". What does ./loop_iff_halts_on_self.sh loop_iff_halts_on_self.sh do?
bedman12345 5y ago
This is a mischaracterisation of gödels incompleteness theorem. The set of axioms the theorem is about isn't even mentioned in the article. This is very important. If you pick the empty set as your axioms, most statements will be independent of them. The important insight is different. One can simulate a computer in the peano axioms. If you could prove or disprove (starting from a computable set of axioms) every statement about simulated computers you could also solve the halting problem. Kleenes (the kleene star guy) proof goes that way.

189 points by lacker 5y ago

But this is bash, which runs on Unixy systems, which have exec. behave_differently is trivial: echo foo exec “$@“ This little hack will carry over to some, but possibly not all [0], models of computation. Fixing this would involve cleaning up some definitions in the proof. [0] Specifically, it does carry over to any model of a program that outputs a stream of symbols one at a time. A single-tape Turing machine that computes a function doesn’t work like that.

assbuttbuttass 5y ago
What if the program you're running outputs "foo" in an infinite loop? Then I think the above behave_differently would actually behave the same
KerrickStaley 5y ago
That does not work. Your example does not change the behavior of the following program: echo foo exec $0
- dskloet 5y ago
  Your program is very close to the above commenter's program. You could have picked the identical program which is exactly what the proof does.

adamnemecek 5y ago

Godels incompleteness theorems get much more attention than the completeness theorems which are much more interesting. https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...

slaymaker1907 5y ago
Unfortunately while valid logical formulas have finite deductions, proving that a formula is not valid (or equivalently that some formula is satisfiable) is Turing complete and thus impossible. So the set of valid first order formulae is recursively enumerable. However, if you limit your scope to finite sets bounded by some size, the problem is merely NP-complete. Given a program, you can construct a formula which is satisfiable iff the program halts (with said formula being polynomial in size with respect to the size of the program).

smitty1e 5y ago

"Any problem in computer science can be solved with another level of indirection."--David Wheeler[0] Which is arguably a re-packaging of Gödel's point: absent a management layer to keep some state concerning the computation, one is in trouble. https://blog.devgenius.io/software-engineering-great-quotes-3af63cea6782 https://blog.devgenius.io/software-engineering-great-quotes-...

automatoney 5y ago

I really like this explanation! It's definitely helpful to see this sort of abstract math idea brought down to super concrete terms. Although I did have a bit of confusion around the "./behave_differently.sh ./my_program.sh ./my_input.txt" part - I expected another layer of concreteness so I was looking for actual outputs (which I realize isn't the point - my_program.sh is supposed to be anything/everything). Other than that though this is a great piece! Short, decently written, and with a good focus but a lot of hints at further things to explore. I guess I'm also not sure about the conclusion - feels a bit like the author's pet issue on how we should teach things, and I feel like that sort of discussion is separate from the article's main focus. I'm more a fan of "here's A different pov on this topic" than "here's THE pov we should teach for this topic"

charcircuit 5y ago

I can implement a basic behave_differently.sh head -c 1024 /dev/urandom paradox.sh paradox.sh will be different than paradox.sh paradox.sh

geysersam 5y ago
Not always. ;) Specifically, if my_program.sh outputs some 1024 lines then it is still nonzero probability that your behave_differently.sh does not in fact behave differently.
- charcircuit 5y ago
  No, there's a 0% chance my implementation outputs 1 as that is only 1 byte long. If you outputted 1023 0s and then a 1 there would be a 2^-1024 chance. That probability is too small to practically happen. The heat death of the universe will happen first.
  - geysersam 5y ago
    You're right that my example was flawed. I've updated it. There is however still nonzero probability that ./behave_differently.sh some_peogram.sh behaves the same as ./some_program.sh
  - shrx 5y ago
    > The heat death of the universe will happen first. No, the heat death might be _more likely_ to happen first, but it's not guaranteed.
- tromp 5y ago
  One could try to guarantee unique outputs with sleep 1 date but the intended requirement of behave_differently is that it produces different output when run on a computer in exactly the same state. Or equivalently, that the program doesn't depend on the computer state, which is true in the more formal setting of universal Turing machines that start from a fixed state.

eximius 5y ago

Does this actually mirror the incompleteness theorem logic or does it just create an infinite recursive loop? They seem distinct.

QuercusMax 5y ago
It's showing that the halting problem is unsolvable, using an infinite recursive loop as an example. The halting problem is related to the incompleteness theorem.
- BizarroLand 5y ago
  I wonder if it could be solvable by an algorithm that was capable of operating at a higher level. Mayhaps the issue is approaching the problem at the same dimensional level that the problem originated from. After all, humans can come at the problem from a higher cognitive level and, given enough time, resolve that an infinite loop is taking place, so the problem is not fundamentally unsolvable. Einstein said, "No Problem Can Be Solved From The Same Level Of Consciousness That Created It", so it is feasible to assume that, say, a quantum computer running every possible iteration of an algorithm could easily identify which iterations of the algorithm's parameters would induce infinite loops by simple attrition.
  - blackbrokkoli 5y ago
    Yes, definitely. But then the next task is just to solve the incompleteness problem on the level of the higher algorithm, because there must always be incompleteness. Hofstaedter discusses this at length in his book Gödel, Escher, Bach if you are interested in this topic.
CaptainNegative 5y ago
It's more or less the same argument. They key additional ingredient in Godel's proof (besides some slight technicality on soundness vs. omega-consistency) is the encoding of an arithmetic interpreter inside of arithmetic itself. That a bash script can run and capture the output of another bash script is pretty obvious, but the first order logic analogue is not nearly as neat and easy. The argument given here is a modern translation of Turing's work in his original paper introducing Turing Machines and the Halting problem, in which he devotes an entire section to the connection between his proof and that of Godel.

Annatar 5y ago

Which practical uses could this have in production?

maweki 5y ago
You can explain to your boss that them wanting to check for undecidable properties is impossible. It's important to know what isn't possible, to not throw infinite resources at the problem.
- bqmjjx0kac 5y ago
  Sometimes probabilistic answers are okay, though.
  - dllthomas 5y ago
    But usually a good idea to understand that that's what you're aiming at producing.
feintruled 5y ago
Only preventative measures! One would know enough, for example, not to try to construct a static analysis tool to helpfully tell the user if their code will inadvertently loop infinitely. Imagine running the tool on itself.
GTP 5y ago
Maybe a company could decide that developing a tool that, given two programs as imput, tells if those two programs are equivalent would be a great tool to help teams migrate their code to a different programming language (or equivalently migrate to a new version of the same language, like it happened from Python 2.x to Python 3.x). But you can reduce this problem to the halting problem and show that this is not possible. More generally, the halting problem is a great tool to prove that other more practical things are unfortunately impossible to achieve, at least in the general case. But as another commenter pointed out, given a specific problem you could come up with heuristics that work most of the times (but sometimes would not be able to give a conclusive answer)

woolion 5y ago

>His proof is fairly difficult to understand - it involves prime numbers, factorization, all this number theory. Actually, the textbook proof itself is not very different from the presentation in this article, so not hard at all. The difficult part is in formalizing that you can write "a program that proves a program halts". To do so you have to encode it into the language of mathematics, and that is the painful part. To be clear: you have the paradox of the set that contains all sets that don't contain themselves. In naïve set theory, it is trivial to write down formally. However the Berry paradox is not a real paradox because there is no way to encode "The smallest positive integer not definable in under sixty letters". So the whole point of going through the encoding is to show that yes, we can encode what a provable statement, and thus the first 'paradox' is actually a crucial flaw in the mathematical theory, whereas the second is a flaw/paradox in human language, but does not mean anything. The computer world is not as strict, it's more squishy (human?) than mathematics.

skissane 5y ago
> However the Berry paradox is not a real paradox because there is no way to encode "The smallest positive integer not definable in under sixty letters". Why is a “way to encode” necessary for a paradox to be “real”? > So the whole point of going through the encoding is to show that yes, we can encode what a provable statement, and thus the first 'paradox' is actually a crucial flaw in the mathematical theory, whereas the second is a flaw/paradox in human language, but does not mean anything. How can you say something “does not mean anything” simply because it cannot be formalised? Since when is formalisability a prerequisite for meaningfulness?
- woolion 5y ago
  >How can you say something “does not mean anything” simply because it cannot be formalised? Since when is formalisability a prerequisite for meaningfulness? I'm wondering then, what you think is the interest of this theorem? The goal of Gödel was to create a metamathematics. You need to know what is a paradox of the theory or a paradox or not to know if it is correct. If you have a contradiction, you cannot believe anything that the theory proves. So the whole thing is ultimately about separating mathematical paradox from "other types" of paradoxes.

void_one 5y ago

There is a fallacy in constructing "paradox.sh" problem. "behave_differently.sh" requires an argument, a program to be run and produce some output. If "behave_differently.sh" is run without any argument, then there is no specified correct behavior. Thus, "paradox.sh" also requires "$1" to be non-empty, otherwise it's result is undefined. When invoking "./paradox.sh ./paradox.sh", the inner "paradox.sh" will be launched without any arguments, running "behave_differently.sh" also without arguments. There is no logical impossibility, just constructed way to trigger unspecified behavior in "behave_differently.sh".

OscarCunningham 5y ago
The second paradox.sh in './paradox.sh ./paradox.sh' isn't run at all. It's soucre gets read in as input to behave_differently.sh.
- void_one 5y ago
  yes, and then behave_differently.sh runs it to capture and modify its output, but without any arguments
  - OscarCunningham 5y ago
    Note that behave_differently.sh takes two inputs, both a program and the input for that program. Also note that paradox.sh gives both these inputs by using $1 twice. And behave_differently.sh is supposed to be an arbitrary program. It can run the input program but it doesn't have to, it can analyse it in any way it wishes.
    - void_one 5y ago
      It is a good point that behave_differently.sh does not necessary run its argument program, but can analyze it in another way. (The context of Bash scripts suggests execution but that is a misleading hint.) In the broader formulation behave_differently.sh tells that its argument program terminates and produces finite input, which is a halting problem.

born-jre 5y ago

i found this explanation to be easier to grasp `truth alone does not exist or is not valuable without the steps to deduction to that truth (contrary to what mathematician traditionally believed`.

jamesfisher 5y ago

I recently wrote this [1] explanation of the halting problem. I should follow up with this approach to proving the incompleteness theorem! [1]: https://tigyog.app/lessons/fr9uub3hqgab/r/the-halting-problem https://tigyog.app/lessons/fr9uub3hqgab/r/the-halting-proble...

uslic001 5y ago

I was just re-reading this book last night. https://www.amazon.com/G%C3%B6del-Escher-Bach-Eternal-Golden/dp/0465026567/ref=sr_1_1?crid=1X18YL1CX1JSD&keywords=godel+escher+bach&qid=1645802899&s=books&sprefix=godel%2Cstripbooks%2C71&sr=1-1 https://www.amazon.com/G%C3%B6del-Escher-Bach-Eternal-Golden...

lacker 5y ago
That book is where I first learned about Gödel's incompleteness theorem. Definitely a good book! I spent a while when I first read it trying to understand Gödel numbering, all the stuff where you multiply prime numbers together, 11 stands for (, that sort of thing. It wasn't until far later that I realized all of that was just a mathematician in the 1930's trying to explain how a string of characters could be encoded as a binary number, something that modern computer programmers more or less take for granted.

qiskit 5y ago

> When Turing proved the halting problem was undecidable - that there is no program that can decide whether another program will ever finish Turing didn't prove the halting problem was undecidable. The halting problem was defined after Turing's death by Martin Davis. It's a common misunderstanding people have. Turing's definition of Turing Machines classified machines that halted as circular/unsatisfactory. Turing wanted his machine to run forever ( circle-free/satisfactory ). > Personally, I think we should set aside Gödel’s original number-theory-based proof as an artifact of history, the way we no longer use Isaac Newton’s original notation for calculus. We also don't teach Turing's version either. No computer science class teaches real Turing. It's been reformulated to a point Turing would barely recognize it. Also, you can't understand the halting problem or Turing without "number-theory-based proof" as "number based proof" and godel numbering is at the heart of turing machines ( look up what descriptive numbers ) are. > We should accept that the concepts of mathematical proof and computer algorithms are intertwined at their heart Computer algorithms are mathematical algorithms. Mathematicians have been using computers/algorithms to derive theorems from axioms since at least the 1950s. You are saying we should accept what everyone already accepts and have accepted for decades.

JadeNB 5y ago
> We also don't teach Turing's version either. No computer science class teaches real Turing. It's been reformulated to a point Turing would barely recognize it. I think that this is true of most long-lived subjects taught in a modern science course. Imagine Euclid's puzzlement at all the things that are now called Euclidean! > Also, you can't understand the halting problem or Turing without "number-theory-based proof" as "number based proof" and godel numbering is at the heart of turing machines ( look up what descriptive numbers ) are. Since you say most of what one learns in a CS course isn't directly about Turing's original work, I don't want to speak to that, but I think that it is possible to understand the halting problem, and even its undecidability, without number theory. It arguably isn't possible to understand the halting problem without some notion of encoding (of the data that constitute a Turing machine in a form that can itself be processed by a Turing machine), but there's no reason that encoding has to be number-theoretic. (I speak here as a number theorist—it's a neat application, just much more important for incompleteness than for halting.)

gregfjohnson 5y ago

Here is a hypothetical bash script that neatly characterizes the the impossibility of solving the halting problem: "loop_iff_halts_on_self.sh". What does ./loop_iff_halts_on_self.sh loop_iff_halts_on_self.sh do?

bedman12345 5y ago

This is a mischaracterisation of gödels incompleteness theorem. The set of axioms the theorem is about isn't even mentioned in the article. This is very important. If you pick the empty set as your axioms, most statements will be independent of them. The important insight is different. One can simulate a computer in the peano axioms. If you could prove or disprove (starting from a computable set of axioms) every statement about simulated computers you could also solve the halting problem. Kleenes (the kleene star guy) proof goes that way.