Division by zero in type theory: a FAQ

Re:Division by zero in type theory: a FAQ by empath75 on Monday July 06, 2020 @11:40PM (#23755485)

> But you allow seemingly nonsense theorems when you forget to condition (x>0).

Such as what? I’ve only spent a few hours with lean, but I’m fairly sure that any attempt to prove something silly would fail because it would catch the weird behavior of 0.

For example. If you tried to use a/a = 1 as the article mentions, you’d be unable to prove it without adding the condition that a != 0, and you’d be unable to use it further on without that condition in place.

[ Parent | on HN ]

Re:Division by zero in type theory: a FAQ by leanuser57 on Tuesday July 07, 2020 @12:29AM (#23755702)

Here is a "nonsense" theorem that is provable in Lean:

“There exists a real number r such that 1/r = 0.”

If you try to translate this theorem into maths, you will run into trouble at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.

[ Parent | on HN ]

Re:Division by zero in type theory: a FAQ by empath75 on Tuesday July 07, 2020 @12:44AM (#23755757)

That’s a perfectly sensible function, it’s just not ordinary division on the reals where x = 0, and you can’t use it that way.

[ Parent | on HN ]