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... cacm.acm.org/blogs/blog-cacm/2

@cwebber

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 en.wikipedia.org/wiki/Halting_ related?

But the halting problem doesn't matter for practical results.

Do you think I missed anything important?

@bhaugen
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 @cwebber That's how I would read the message as well, but then a simpler argument should be possible, in my opinion, since practical computer science is essentially about (very) big finite automata.

@scolobb

What would the simpler argument sorta look like, and do you mean argument for or against Gödel or Hewitt, or something else? (Vague handwaving version, don't go to a lot of work...)

@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

@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.
@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
@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.
@abs @cwebber I know but how can you have uncountable many theorems if you have a countable language to begin with?
@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.
@abs @cwebber what is a theorem that you can’t write down? Also, nice new avatar
@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.
@abs @cwebber but that’s not what the word theorem means in logic. Anyway it seems like as usual Goedels theorems attract a lot of crackpottery
@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).

@abs @cwebber I read the paper, it's complete nonsense. At no point does it even come close to coherently specifying a theory. I think the blog post is also BS.

@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.
also: theguardian.com/technology/200

@abs @axiom @cwebber

I'm a little bit familiar with Hewitt's work on this. I don't think he's a crank. The CACM blog post that Cristopher linked to does not try to advance a complete argument. It informally describes some of Hewitt's work.

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

@abs @axiom @cwebber Direct Logic is not a first order logic. It is a typed logic that deals with sentences and theories directly. Types are strictly ranked -- new types are constructed only from earlier types.

@abs @axiom @cwebber

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.

@abs @axiom @cwebber

(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

@axiom @abs @cwebber

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

hal.archives-ouvertes.fr/hal-0

@Thomas_Lord @abs @cwebber I assume you mean appendix 4? It's entirely unclear. Nor do I see how he defines consistency.

@axiom @abs @cwebber

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

@axiom @abs @cwebber

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.

@axiom @abs @cwebber

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.

@Thomas_Lord @abs @cwebber I disagree with the notion that a "system" with undecidable axioms is even a system. Here's a simple version of such a "system": take every true sentence of PA to be an axiom. It's absurd to claim this is a formalization of mathematics.

@Thomas_Lord @abs @cwebber Disagree. One big issue I see is that he uses the turnstile itself inside the definition of the proof system. In other words he's confusing the theory with the metatheory. With this going on it's easy to "prove" consistency

@axiom @abs @cwebber

> "he's confusing the theory with the metatheory"

It's not confusion, it's the point. Core DL is a general purpose *reflexive* theory-of-theories. It needs no meta-theory. It is self-theorizing. (e.g., see paragraph 4 in the abstract.)

@Thomas_Lord @abs @cwebber Anyone who has studied logic for 10 minutes can tell you that that's nonsense and has nothing to do with what mathematicians do or with what they mean by "theory" or "consistency".

@Thomas_Lord @abs @cwebber well, it's not entirely "nonsense" but it certainly isn't a foundation of mathematics.

@Thomas_Lord @abs @cwebber (separately I think his paper is also nonsense because it's totally unclear and unreadable)

@Thomas_Lord @abs @cwebber I'm well versed in logic and type theory. I can recognize bullshit and distinguish it from "above my level". Please don't insult me like that.

@axiom @abs @cwebber

> "I'm well versed in logic and type theory"

No insult was intended. Hewitt is writing for an audience with primary interest in the history of mathematical thought.

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

@axiom @abs @cwebber

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

@Thomas_Lord @abs @cwebber I disagree with this characterization of the situation but I don't have infinite patience to argue about it on the internet. I remain completely unconvinced.

@axiom @abs @cwebber

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.

@axiom @abs @cwebber

Hardly "all over the Internet."

Given what you've been saying about the level of effort you've put into his text, though: please consider that your calling him a "crank" might be a bit unjustified. That's all.

@Thomas_Lord @abs @cwebber Maybe "senile" then, unfortunately. I think I've put in enough effort to tell that this work is nowhere near research-quality for mathematics.

Show more
Sign in to participate in the conversation
Octodon

Octodon is a nice general purpose instance. more