5 ms·

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

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

cryptonector 8y ago
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.
JadeNB 8y ago
> 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.
- JadeNB 8y ago
  (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 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.")
nonintuitive 8y ago
It's painful how dumb this blog post is. It's clear that the multiplication is no longer associative with this definition.
Kutta 8y ago
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.

cryptonector 8y ago

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.

JadeNB 8y ago

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

JadeNB 8y ago
(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 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.")

nonintuitive 8y ago

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

Kutta 8y ago

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.