In traditional HN style, I will now thumb my nose at Vertasium's excellent video due to him skipping over how godel came up with the proof.
He built up the whole damn video for that one moment, when he says "And godel went through all this trouble to come up with this card..." and flips over the card. But how godel did it is at least as cool as the proof itself.
I'm mostly being tongue in cheek with the Veritasium nose-thumbing. But if you saw it and want to understand it more deeply (and in my opinion more satisfyingly), I recommend "What Godel Discovered": https://news.ycombinator.com/item?id=25115746
It explains Godel's proof using Clojure. Quite accurately, too.
The thread is also hilarious. Shoutout to the MIT professor who took offense at someone linking to his wikipedia page: "Wikipedia is contentious and often potentially libelous." ... and then you check his wikipedia page, and it's a super positive article about all of his discoveries and life's work.
> Shoutout to the MIT professor who took offense at someone linking to his wikipedia page […] and it's a super positive article about all of his discoveries and life's work.
Carl Hewitt is no doubt a famed and accomplished professor, but why does nobody point out that he is claiming that Gödel’s proof is incorrect[0]?
I already heard of his conviction that “The Church/Turing Thesis is that a nondeterministic Turing Machine can perform any computation. […] [T]he Thesis is false because there are digital computations that cannot be performed by a nondeterministic Turing machine.”[1].
(Which, to be fair, is a strongly related argument to the one that Gödel was wrong.)
I don’t personally know whether he is right, and his digression about millions of people risking death as a result does not inspire confidence, but in my understanding, neither statement is widely accepted.
I don't want to be a professional Hewitt debunker, but his stance has been ripped to shreds; at this point, he is wrong about Direct Logic refuting Gödel and Turing, and his ActorScript can't be implemented on real machines.
I don't know anything about Hewitt or his stance, but I don't feel like this adds a whole lot to the conversation. I mean I can tell that you're sure that he's wrong, but why should the strength of your belief convince me?
It would be helpful if you added some links or some explanation, or just anything beyond what you've written there.
It’s similar to claiming someone made a perpetuum mobile — extraordinary claims going against basically every mathematician/computer scientist since Gödel require extraordinary evidence.
And the result is quasi always that the one claiming, looked over some small but crucial detail.
Isn’t the order of a proposition included in its Gödel number?
Each proposition is assigned to an increasing prime power, and the increasing list of primes has total order, such that swapping propositions yields a distinct Gödel number.
I think what ProfHewitt means here (based on other writing I've found, as he is frustratingly low on details in these conversations) is "order" in the sense of "first order logic", "second order logic"; not in the sense of "first proposition, second proposition" etc.
His claim is that the proposition "This proposition is not provable", formalized as "P equivalent to P is not provable" is not well formed in a typed logic, as "P"'s type is first-order, while "P is not provable"'s type is second-order. Therefore, his claim is that the proposition is simply not well-typed and therefore not interesting. Godel's proofs were discussing an untyped logic, but according to Hewitt that is not an accurate representation of mathematics.
I don't think anyone in the space agrees with him, though, as far as I could tell from some cursory reading.
Could you provide two statements with equal Gödel numbers and the same characters in different orders, and a detail of how you compute the Gödel numbers?
If two statements have the same characters in the same order, how are they not the same statement? And why would that make Gödel’s statement invalid in Principia Mathematica?
I know of several computer verified proofs of the incompleteness theorem. See entry 6 of https://www.cs.ru.nl/~freek/100/ for a small catalogue.
How does this relate to your objection? Are there bugs in the verifiers? Or did people verify the wrong theorem statement?
So you say that the computer verified proofs of the incompleteness theorem of verifying the wrong theorem? Because there can't be bugs in a computer verified proof.
(Of course there can theoretically be bugs in a computer verified proof. If there are bugs in the verifier. But if 4 independent proof assistants verify a proof of a theorem, this is extremely unlikely.)
Suppose that Turing is wrong. Then Turing gave an algorithm which should defeat Rice's Theorem. Therefore, I may simply ask, to Hewitt: Could you please write up a short program in a popular Turing-complete programming language which proves or disproves Goldbach's Conjecture? It should be trivial!
Of course, on actual computers, Turing's result applies, Rice's Theorem manifests, and such a program will likely run indefinitely, until we get bored and give up.
The point that Hewitt has made in another thread is typical misdirection. See, it doesn't matter which order of logic we're talking about; in general, we have results for higher order logic, all the way up to Lawvere's fixed-point theorem for any Cartesian closed category. To fight this, Hewitt has to disclaim the entirety of 20th-century mathematics. (At least he's internally consistent -- he does deny modern maths!)
Sad fact is that, ever since 1976 (http://www.laputan.org/pub/papers/aim-353.pdf) folks have recognized that Hewitt's claims about the foundations of computation are not just wrong, but flamebait. But he never had the humility to learn from his mistakes.
Loosely, because ActorScript requires some sort of genuine non-determinism where an actor explores multiple states simultaneously, we need some sort of magic non-deterministic computer. A quantum computer isn't enough; simulating an ActorScript program is NP-complete.
Maybe there can be physical machines which run ActorScript, but I would expect them to come with new laws of physics, and also I think that there are probably more comfortable programming languages. We already have https://en.wikipedia.org/wiki/Constraint_Handling_Rules for example.
Because it is? It isn't quite "ridiculous", as it is somewhat more amusing than that. It certainly isn't "funny", FWIW, as I have absolutely no positive connotations with it... "hilarious" feels like the correct term.
He built up the whole damn video for that one moment, when he says "And godel went through all this trouble to come up with this card..." and flips over the card. But how godel did it is at least as cool as the proof itself.
I'm mostly being tongue in cheek with the Veritasium nose-thumbing. But if you saw it and want to understand it more deeply (and in my opinion more satisfyingly), I recommend "What Godel Discovered": https://news.ycombinator.com/item?id=25115746
It explains Godel's proof using Clojure. Quite accurately, too.
The thread is also hilarious. Shoutout to the MIT professor who took offense at someone linking to his wikipedia page: "Wikipedia is contentious and often potentially libelous." ... and then you check his wikipedia page, and it's a super positive article about all of his discoveries and life's work.