[FOM] undefined expressions

[Paul Blain Levy]

On 05/06/18 13:05, Norman Megill wrote:
> On 6/4/18 1:17 PM, Paul Blain Levy wrote:
>
>>> 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.
>
> Why?  (That might be important to know for the intuitionistic iset.mm,
> where contributor Jim Kingdon is just starting to add IZF set theory.)
For intuitionistic ZF, in defining f(c), we cannot assume that c either
is or is not in the domain of f, as we can in the classical setting.

The only option I can think of is to define f(c) to be the union set of
{d | (c,d) in f }.  It follows that, if c is in the domain of f, then
f(c) is the unique f-image of c, and if c is not in the image of f, then
f(c) is the empty set.

Paul