[FOM] undefined expressions
Paul Blain Levy
P.B.Levy at cs.bham.ac.uk
Tue Jun 5 19:13:07 EDT 2018
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
More information about the FOM
mailing list