I really don't understand what Carl Hewitt is saying with his recent takedowns of Gödel and I'm not sure if that's on me or... https://cacm.acm.org/blogs/blog-cacm/233650-computer-science-relies-on-the-opposite-of-godels-results/fulltext
@cwebber It doesn't make sense to me, either.
Hewitt's article is beyond my mathematical and philosophical education, but I didn't get "takedown of Gödel" so much as "Gödel does not matter for practical computational math". (Altho he might have intended a takedown...)
I suspect that Gödel does matter for computation on the edges, e.g. isn't the https://en.wikipedia.org/wiki/Halting_problem related?
But the halting problem doesn't matter for practical results.
Do you think I missed anything important?
Typically in courses on computational complexity, Gödel's incompleteness is presented as 'practical' only in the sense of assuring humans won't be put out of a job by computers brute forcing math proofs. Which matters greatly to me personally, but has little influence on actually computing anything. (Although, it's not so artificially constructed as it seems; we deal with Gödel numbers daily, as the binary representation of any program is one.)
I'm going to have to take a deep breath before examining this one because he doesn't seem to give the reader time to come up for air between shifts of reference frame. My intuition is that a critical distinction has been overlooked or misconflated, but I expect it would be about two hours of decyphering to confirm or deny that even with all necessary background knowledge. [bookmarks]
@abs @cwebber Yeah Hewitt is just a crank. Apparently did some interesting AI research back in the day but I don't think he's taken seriously anymore.
1. Hewitt has advanced a proposed , formal "foundation for mathematics" that he calls Direct Logic. Direct Logic is powerful enough to theorize natural numbers, real numbers, sets, lambda calculus, and Actors (and more).
2. The bit about Goedel is two-fold:
(A) In Direct Logic, there is a trivial, formal proof that the theory is consistent. The proof is "unconvincing" -- perhaps the theory also contains a proof that theory is inconsistent. But the proof is there, in the theory. According to Goedel as popular understood, since DL can formally prove itself consistent, it must be inconsistent -- but, not so. ...
@Thomas_Lord @abs @cwebber Can you point me to a reference which actually defines Direct Logic? And anyway, I doubt that the definition of "consistency" inside DL actually corresponds to what I would call consistency. This is in contrast to PA where the internal definition of PA via Godel-numbering is clearly what I think of as consistency.
(B) Goedel's "proof" that DL must be inconsistent because it can prove its own consistency assumes that a DL sentence can be constructed by computing a particular fixed point. The typing rules of DL do not allow this.
So, Hewitt's contention is that Goedel's proof is basically confused, and relies on ambiguous metaphysical fantasms.
If I recall correctly, DL is more or less entirely given between the appendix and body of that paper.
(So, I disagree with your earlier statement to the contrary.)
"Mathematics" (which is more than the core DL - it is DL plus some additional axioms) *formally* proves its own consistency by contradiction. End note 8: "Which is not the same as proving the much stronger proposition that no contradiction can be derived from the exact axioms and inference rules of Direct Logic"
You and Hewitt think of "consistency" pretty much the same way, I think.
Hewitt's point is *not* "I have proved standard set theory - or something just as good - lacks contradictions". He doesn't believe that he has done that.
His point is "I have a foundation of Mathetmatics that contains a formal self-proof of consistency and in which Goedel's "proof" is inexpressible because it violates the type rules for constructing sentences.
I've read that the modern full form of Goedel would say something like "consistency, completeness, or enumerable axioms: pick any two".
"Mathematics" in DL happens to have uncountable axioms and it formally (even if unconvincingly) proves its own consistency -- i.e. Goedel's trick doesn't apply.
Turing's does. "Mathematics in DL" definitely has *undecidable* propositions.
@axiom @abs @cwebber
If you posed that as a question to Hewitt the right way, he'd probably agree with you. In part he's making a critique over the standard choices of foundation, saying that all the useful stuff in "standard mathematics" can be defined on this alternative foundation that excludes all of those classical paradoxes -- but that instead expresses the same essence in terms of innumerability of axioms and undecidable propositions.
@Thomas_Lord @abs @cwebber Eh, he spends like half of the paper ranting about how no one recognizes his genius, so I don't really feel like asking him anything. I don't agree that the useful parts of standard mathematics *can* be put on such a foundation. I think he's done something very trivial and thinks it's clever.
> "he spends like half of the paper ranting about how no one recognizes his genius,"
The purpose of that particular paper is to situate DL in its historic specificity. E.g. Russell thought he could avoid paradoxes by ranking sets. Goedel proved a limit of Russell's theory or anything like it. Wittgenstein argued (weakly) that Goedel was confusing himself with a syntactic illusion. Hewitt shows Wittgenstein correct by construction.
N.P. I'll just conclude that: I would agree insofar as a more pedagogical presentation of the system would be nice to have. I also agree that its in some sense "trivial" but I think choice of formal foundations makes a big practical difference, both for ease and clarity of thought and for automation. And appendices 4,5, and 6 etc lay out the system pretty well, but not in a way that makes a good linear presentation of it.
@Thomas_Lord @abs @cwebber choice of foundations certainly makes a difference. I consider it absurd to found mathematics on a system which can't be explained clearly. I tried to look at those appendices in a last-ditch effort to salvage some meaning out of the paper, but was stymied by the fact that there's literally an endnote every couple symbols. Anyway I see that you are all over the internet defending Hewitt's work so I don't see much point in trying to convince you.