Hacker News Reader

Comment by excalibur | Hacker News Reader

> We’ve now established that if we choose some constant C, then defining division such that x/0 = C does not lead to any inconsistencies.

No, you haven't. You've merely failed to locate any. You've said "I'm not going to prove that this works. I'm going to assume that it does and act as if it did, and place the burden on you to prove otherwise."

View on HN

Absolutely correct. That said, proof assistants are being used. Here's a quote from TFA:

> Lawrence Paulson, professor of computational logic and inventor of Isabelle: > > [...] This identity holds in quite a few different proof assistants now.

Wrong. Division is not part of the field axioms, it is a defined function, and changing its definition has absolutely no bearing on the consistency of your equational theory.

> No, you haven't. You've merely failed to locate any. You've said "I'm not going to prove that this works. I'm going to assume that it does and act as if it did, and place the burden on you to prove otherwise."

Excellent point. It's not even known if we can get any inconsistencies without making this definition; and it's known that, if it's true that we can't get any inconsistencies without it, then we can't prove that it's true. Building on such possibly shaky foundations can't make them stronger.

(That's not mathematical maundering, by the way; it is a correct if informal statement of part of the incompleteness theorems. I appreciated excalibur (https://news.ycombinator.com/item?id=17736486 )'s point, and wanted to underline the significant, and mathematically precise, difference between "one apparent inconsistency is not present" and "there is no inconsistency.")

It's painful how dumb this blog post is. It's clear that the multiplication is no longer associative with this definition.

Reply on news.ycombinator.com