[FOM] undefined expressions

[Norman Megill]

On 6/4/18 1:17 PM, Paul Blain Levy wrote:
>> Date: Sat, 2 Jun 2018 20:56:11 -0400
>> From: Norman Megill <nm at alum.mit.edu>
>>

>> 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.

I chose it mainly because it matches the out-of-domain behavior of the 
definitions of Quine and Takeuti-Zaring.  Also, it seemed like the 
simplest choice.  See the df-fv description:

http://us.metamath.org/mpeuni/df-fv.html

Outside of some early set theory development, it is rare that we depend 
on the value being the empty set.  Most proofs are about the in-domain 
behavior of the function anyway.  I would usually consider it to be poor 
style for a proof to depend on it gratuitously (for example, showing the 
argument is in-domain if the function value is non-empty), although we 
don't prohibit it.

However, we do depend on heavily on the fact that it is unconditionally 
a set and never a proper class.  Many general-purpose library theorems 
require their variables to be sets.   We have a library theorem fvex 
(function value exists) saying just that, and it is used in over 1900 
proofs:

http://us.metamath.org/mpeuni/fvex.html


An alternate proposal by Alexander van der Vekens is to define the 
out-of-domain function value as the universe (proper class) V.  This has 
a certain appeal to it:  makes it "undefined" in a stronger sense, 
because it doesn't exist as a set.  See

http://us.metamath.org/mpeuni/df-afv.html

and its uses.  A problem with this approach is that the 1900 proofs now 
using fvex would have to be rewritten to show the argument is in-domain 
in each case.  This would make the proofs longer, sometimes considerably 
so.  So we are unlikely to adopt this proposal in the main body of 
set.mm, and it resides in van der Vekens' "mathbox" (a user-specific 
workspace sometimes used to explore alternate ideas).


> 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.)


Norm Megill