[FOM] undefined expressions
Norman Megill
nm at alum.mit.edu
Tue Jun 5 12:05:07 EDT 2018
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
More information about the FOM
mailing list