[FOM] undefined expressions

[Paul Blain Levy]

> Message: 2
> Date: Sat, 2 Jun 2018 20:56:11 -0400
> From: Norman Megill <nm at alum.mit.edu>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: [FOM] Harrison Advocates ZFC (Metamath)
> Message-ID: <bdaf9175-6934-939c-eace-c9dfa67b1a6c at alum.mit.edu>
> Content-Type: text/plain; charset=utf-8; format=flowed
>
> Since Metamath has been mentioned, I'll make some remarks on it that may 
> be of interest.
> In set.mm, 1/0 is "undefined" because the domain of the 2nd argument of 
> the division operation excludes 0.  Technically, 1/0 evaluates to the 
> empty set (that's what we chose for out-of-domain behavior of functions 
> in general - why we chose that is another discussion)
I'm interested in why you chose it.  For intuitionistic ZF, I would
think that it's the only option.

Paul
> , but there is 
> nothing we can do with it in the context of complex numbers, whose 
> members are the urelement-like objects I described.  We cannot prove 
> that 1/0 is or is not a complex number, so it is effectively undefined.
>