[FOM] 618: Adventures in Formalization 4

[Mario Carneiro]

To add another bullet for my own system of choice:

* In Metamath, built on ZFC, the division function has domain (C x C\{0}),
so 1/0 is outside the domain, yielding the empty set (if you wanted to
evaluate it anyway) by the definition of function value out of domain.

Mario

On Thu, Sep 17, 2015 at 4:20 PM, Dominic Mulligan <
dominic.p.mulligan at googlemail.com> wrote:

> After discussing with Freek Wiedijk offline and performing some digging of
> my own, I feel the post I made earlier, quoted below, needs some
> refinement, and Harvey has a point when it comes to how division is handled
> in some proof assistants. Namely:
>
>   * Agda handles division how I claimed, by giving the division function a
> dependent type and requiring a proof that the denominator is non-zero. Note
> the proof argument is implicit, meaning Agda will try to infer the
> denominator is non-zero itself, only requiring an explicit proof if that
> fails.
>   * Coq has multiple axiomatisations and constructions of the reals, both
> classical and constructive. The standard library implementation defines 1/0
> to be an unknown but defined number. The CCorn library implements the
> constructive reals and requires an explicit non-zero proof provided by the
> user when calling the division function.
>   * Mizar and HOL Light define 1/0 = 0 explicitly.
>
> So, it seems like there's multiple different approaches in use, and
> whether 1/0=0 or not depends on the particular proof assistant, and even on
> the particular library in use. Hope this clears things up.
>
> Dominic
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150918/ae575787/attachment-0001.html>