Follow

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

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.)

@cwebber

@bhaugen My argument is about the relevance of the halting problem to practical computer science: It is undecidable in general, but it is always decidable for a given computer program, because the computer with its program is a finite automaton (and so it either halts or loops, visiting the same state infinitely many times).

Thanks for asking, I haven't thought about this question in "ages". I suppose my arguments may be a little dusty 🙂

@cwebber

Thanks for asking, I haven't thought about this question in "ages". I suppose my arguments may be a little dusty 🙂

@cwebber

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]

@cwebber Got me lost from the first sentences. I've always thought Gödel said that a consistent theory is not complete, and I can't see how computer science is, especially given the various undecidability results, giving rise to the whole infinite arithmetical hierarchy.

Speaking of lambda calculus: equality of two lambda terms is undecidable: https://en.m.wikipedia.org/wiki/Lambda_calculus#Undecidability_of_equivalence

But I'm afraid I don't even get the message of the article.

Speaking of lambda calculus: equality of two lambda terms is undecidable: https://en.m.wikipedia.org/wiki/Lambda_calculus#Undecidability_of_equivalence

But I'm afraid I don't even get the message of the article.

@cwebber wat

> [...] it is of no practical importance that theorems are not computationally enumerable because they are uncountable.

There are uncountable many theorems now? What does that mean even. What a weird article

> [...] it is of no practical importance that theorems are not computationally enumerable because they are uncountable.

There are uncountable many theorems now? What does that mean even. What a weird article

@epicmorphism @cwebber I think he's referring to the concept of enumerability from computability theory, that is the existence of a computational surjection from the natural numbers into the theorems (which are only the probable formulas).

@epicmorphism @cwebber In his "direct logic" there are uncountably many theorems (at least he claims that to be the case). You generally have to be a bit careful when reading this because he is moving between first order logic and his logic very seamlessly.

I have only looked over the abstract of his paper but the things he says about inconsistency and contradictions at least make it seem like his logic is fairly non-standard in how it behaves.

I have only looked over the abstract of his paper but the things he says about inconsistency and contradictions at least make it seem like his logic is fairly non-standard in how it behaves.

@epicmorphism @cwebber One way I can think of is having theorems that can't be written down in syntax (just as there "are" real numbers you can't describe).

There certainly is a burden of justification attached to that.

There certainly is a burden of justification attached to that.

@epicmorphism @cwebber My intuition for getting this would be making theorems a type that does not have a way of pattern matching on it and then adding an assumption of a suitable injection. Of course you still wouldn't be able to give a undescribable theorem, but this would be a way of going about it.

I don't think there is any benefit to doing this, though.

I don't think there is any benefit to doing this, though.

@cwebber At the very least everything he says seems to be resting on the second citation which is a paper he authored on his own. I don't have the time to read such a big paper but if you really want to get to the bottom of it, you'd probably have to do that. Though I feel there is a high chance this might be broken somewhere (or he is using the terminology in a misleading way).

also: https://www.theguardian.com/technology/2007/dec/09/wikipedia.internet

@abs @axiom @cwebber Looking at the thread above, I think the information I could usefully add here is....

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. ...

(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.

@Thomas_Lord @abs @cwebber I called him a crank based on his paper, not his blog post

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.

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.

> "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.

Blake C. Stacey@bstacey@icosahedron.website@cwebber It doesn't make sense to me, either.