Gödel's Incompleteness Theorem in Bash
lacker.io
lacker.io
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"
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.
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.)
You can understand the halting problem without math. You can explain it logically. But the halting problem has nothing to do with Turing. As I stated, the halting problem was invented/discovered by someone else years after Turing's death. We don't need Turing or the Turing machine to understand undecidability since Alonzo Church already proved undecidability before Turing.
> but there's no reason that encoding has to be number-theoretic
Sure. Turing encoded to the standard description ( letters ) and to description numbers. But number theory is necessary if you want to follow Turing's approach since you need to show for starters that turing machines and computable numbers are enumerable.
Really? I did not include a reference link here but I grabbed the dates from Wikipedia, which states:
Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist.
https://en.wikipedia.org/wiki/Halting_problem
Obviously Wikipedia is not the end-all be-all of mathematical sources, but I'd be curious to see a source that contradicts it here.
https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
I'll let you guess what Entscheidungsproblem means.
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.
>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.
I think the difficulty of understanding Gödel's proof has changed with the rise of computers. For him the difficult part of the proof was showing that you can represent text as numbers and manipulate it using arithmetic operations. These days we all do that for our day jobs. So you can skip over the part that Gödel thought was difficult in one line, and focus your attention on the clever use of self-reference.
Also these days we would probably use a binary encoding instead of Gödel's encoding via prime factorisation, so even if you did want to explain the details of the encoding the amount of number theory would be reduced.
When you write programs, you don't prove them correct, and you go down to assembly instructions, which is essentially what Gödel did.
Yes - this is a great way of putting it.
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?
You might be able to derive philosophical or empirical meaning from an interpretation of some non-precise statement, but you shouldn't hope that such an interpretation is a valid mathematical theorem.
I think when you say "pure", you actually mean "formal" or "symbolic" or "mathematical". Many believe that there is much more to logic than a mere formalism – although that itself is a major point of contention in the philosophy of logic.
> You might be able to derive philosophical or empirical meaning from an interpretation of some non-precise statement, but you shouldn't hope that such an interpretation is a valid mathematical theorem.
Berry's paradox may not be a mathematical paradox – but that doesn't show it is not a paradox. And, even if it is not a mathematical paradox, it nonetheless made a valuable contribution to mathematics, by inspiring the construction of formal analogues, some of which turned out not to be paradoxical (but nonetheless interesting). However, I don't think it necessarily follows, that just because those formal analogues turned out not to be actual paradoxes, that its natural language version cannot be a real paradox. And, some argue there are formal analogues which are genuine paradoxes – see for example https://ojs.victoria.ac.nz/ajl/article/download/4972/4634/73...
Isn't this getting a bit circular, as it seems to be using the presumed existence of a formal analogue to justify the informal Berry's paradox? If it has a paradoxical formal analogue, then it does not stand as an example of a useful yet unavoidably informal paradox.
Also, given that there seem to be more than one plausible formal analogue, not all of which are paradoxes, does the dispute not just re-form around which is the real formal analogue? That's what seems to be happening in the exchange of papers from which your example was taken.
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.
Well, it was a profound discovery about the limits of consistent formal systems, and of course it is interesting in that light. But, viewing that as profoundly interesting does not require one to adopt your apparent position that only the formalisable is "real".
> If you have a contradiction, you cannot believe anything that the theory proves.
Only with classical logic. With paraconsistent logic, you can believe things proven from inconsistent axioms. Classical logic includes the principle of explosion (ex contradictione quodlibet, from a contradiction anything follows); so inconsistent theories immediately collapse into trivial ones, and trivial theories are of course utterly useless. But since paraconsistent logic rejects the principle of explosion, inconsistent theories do not collapse into triviality, and thus may be useful in spite of their inconsistency.
One argument for this: material implication is a poor model of how implication works in natural language, as the well-known paradoxes of material implication show. With modal logic, we can introduce strict implication, which performs better, but still falls short as an accurate model of natural language implication, as shown by the paradoxes of strict implication. Relevant logics (aka relevance logics) avoid the paradoxes of strict implication as well. But relevant logics are also paraconsistent.
Using an appropriate paraconsistent logic, Berry's paradox can be turned into a formal paradox, and such a formal paradox can be viewed as a straight-forward formalisation of the informal Berry's paradox.
Attempts to formalise Berry's paradox using classical logic fail to produce a paradox, because classical logic lacks sufficient self-referential power – classical logic cannot cope with inconsistency, so classical formal systems must have their powers of self-reference neutered – compared to natural language – to prevent self-referential paradoxes – and those restrictions also prevent a formal Berry's paradox from existing. Paraconsistent logic is far better at handling inconsistency, so it does not have to restrict self-reference, and becomes much closer to natural language in power – and Berry's paradox becomes a formal paradox as well as an informal one.
So, given the above – in what sense is Berry's paradox not "real"?
"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".
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.
In the broader formulation behave_differently.sh tells that its argument program terminates and produces finite input, which is a halting problem.
class RusselSet(set):
def __contains__(self, other):
return other not in other
paradox = RusselSet()
paradox in paradox # ?https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...
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).
They seem distinct.
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.
It says there are something non-mechanical about intelligence.
Apparently people think it is just a paradox or some other boring idea.
See "Emperor's New Mind" from Roger Penrose.
I don't think Gödel drew that conclusion; that's Roger Penrose's reasoning. He uses Gödel's Theorem as an example of correct reasoning that can't be algorithmic (i.e. Gödel's mind cannot be replaced by an algorithm). It's not a proof, and it's controversial. I find it convincing; but then I'm biased - I'm predisposed to the view that the mind is not algorithmic.
But I find it very disheartening when such an interesting find is presented as simply "a paradox" akin to the phrase "this is a lie". That would be the most uninteresting thing ever.
Many articles on the internet thus describe Gödel's theorem, and also that famous book from Douglas Hofstadter.
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.
Hofstaedter discusses this at length in his book Gödel, Escher, Bach if you are interested in this topic.
head -c 1024 /dev/urandom
sleep 1
date
Imagine my_program.sh says: echo "2022-02-26 10:30:00" and you run your version of behave_differently.sh at 10:29:59 on the 26/2. Then the output is the same.
I think that's the problem here.
No, the heat death might be _more likely_ to happen first, but it's not guaranteed.
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.
[1]: https://tigyog.app/lessons/fr9uub3hqgab/r/the-halting-proble...
./loop_iff_halts_on_self.sh loop_iff_halts_on_self.sh
do?
It's important to know what isn't possible, to not throw infinite resources at the problem.
echo foo
exec “$@“
[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.
Then I think the above behave_differently would actually behave the same
echo foo
exec $0Which 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-...