About values returned by partial functions

[fl]

In fact I'm not sure I appreciate partial functions such as supw
returns a value not in the
base set in case there is no solution. The reason is that I find
idioms such as

(R supw A) e. X

counterintuitive. Its exact meaning is "A has a supremum". But the
idiom looks like
as if it means "the supremum is an element of X".

I think it would be better if we accepted the values of such functions
is a collection of
values. This collection would be empty in case the supremum doesn't
exist. And it would
be a singleton in case the supremum exists. Thus to write that a
supremum exists we would
write (R supw A) =/= (/). And in case the supremum exists one would
extract it with a
union S = U. (R supw A) and would use S then.

The same problem exists with the concept of limits or with the concept
of greatest element.

--
FL

[Norman Megill]

> In fact I'm not sure I appreciate partial functions such as supw
> returns a value not in the
> base set in case there is no solution. The reason is that I find
> idioms such as
>
> (R supw A) e. X
>
> counterintuitive. Its exact meaning is "A has a supremum". But the
> idiom looks like
> as if it means "the supremum is an element of X".

Well, to me they say the same thing. If the supw isn't an
element of the domain of discourse X, then it is not a valid
value. What else could not being in the domain of discourse
possibly mean?

Anyway, I propose a solution with the Undef function below.

> I think it would be better if we accepted the values of such functions
> is a collection of
> values. This collection would be empty in case the supremum doesn't
> exist. And it would
> be a singleton in case the supremum exists. Thus to write that a
> supremum exists we would
> write (R supw A) =/= (/). And in case the supremum exists one would
> extract it with a
> union S = U. (R supw A) and would use S then.

I think this would be too restrictive. It would mean we
can't, for example, have partial functions on sets of
ordinals, since (/) is an ordinal. In addition, not having
(/) in a base set is an unnatural restriction that isn't
required by the literature and would require an additional
restrictive condition on the base set of all structures.

One solution (but wrong IMO) is to have a partial function
evaluate to the universe V when it is undefined. Then there
will be no ambiguity, since it won't exist at all! Although
that may be theoretically elegant in some sense, practically
speaking it would make a lot of theorems very awkward.
Imagine if we had to prove "E! ..." every time we wanted
to use theorem 'fvex'.

What I propose is the function Undef - see df-undef in my
mathbox on us2.metamath.org. I use it to return the
undefined value of the restricted iota function, which in
turn is used by my mathbox version of supremum, df-lub. If
the base set is X and S is a sup, we can say either "S e. X"
or "S =/= (Undef ` X)" to say that S is defined, according
to your preference. Hopefully this will satisfy your your
objection.

Over time, I may replace the current Poset and
supw with the PosetNEW and lub in my mathbox. I want to be
satisfied that the new df-struct is a useful approach,
though.

Note, by the way, that the current supw already returns
( Undef ` X ), just not explicitly. I think I am going to
put Undef and restricted iota functions in the main set.mm
for general use in a few days, since I think they will be
generally useful (and are not dependent on the new df-struct
stuff). Then you can say "(R supw A) =/= ( Undef ` X )"
instead of "(R supw A) e. X", if you want.

Norm http://us.metamath.org/email.html

[fl]

On 25 sep, 23:17, Norman Megill <n...@alum-2.mit.edu> wrote:
> > counterintuitive. Its exact meaning is "A has a supremum". But the
> > idiom looks like
> > as if it means "the supremum is an element of X".
>
> Well, to me they say the same thing.  

Technically speaking yes. But the aim is not the same. The intuitive
semantic is not the same.

> > I think it would be better if we accepted the values of such functions
> > is a collection of
> > values. This collection would be empty in case the supremum doesn't
> > exist. And it would
> > be a singleton in case the supremum exists. Thus to write that a
> > supremum exists we would
> > write (R supw A) =/= (/). And in case the supremum exists one would
> > extract it with a
> > union S = U. (R supw A) and would use S then.
>
> I think this would be too restrictive.  It would mean we
> can't, for example, have partial functions on sets of
> ordinals, since (/) is an ordinal.  In addition, not having
> (/) in a base set is an unnatural restriction that isn't
> required by the literature and would require an additional
> restrictive condition on the base set of all structures.

Of course (/) could be a value. You would return { (/) } in that case.

We could also uniformize the concept of partial function and of
multi-valued function. In the latter case with my proposal we
would return more than one element.

A function such as the function that returns the limit of a function
would gain in clarity with such a convention in my opinion.

> What I propose is the function Undef - see df-undef in my
> mathbox on us2.metamath.org.  I use it to return the
> undefined value of the restricted iota function, which in
> turn is used by my mathbox version of supremum, df-lub.  If
> the base set is X and S is a sup, we can say either "S e. X"
> or "S =/= (Undef ` X)" to say that S is defined, according
> to your preference.  Hopefully this will satisfy your your
> objection.

That's better. It definitely ressembles the bottom type used
by some computer languages.

http://en.wikipedia.org/wiki/Partial_function

But it wouldn't unify the partial functions with the multi-valued
functions.

> Over time, I may replace the current Poset and
> supw with the PosetNEW and lub in my mathbox.  I want to be
> satisfied that the new df-struct is a useful approach,
> though.

> Note, by the way, that the current supw already returns
> ( Undef ` X ), just not explicitly.  I think I am going to
> put Undef and restricted iota functions in the main set.mm
> for general use in a few days, since I think they will be
> generally useful (and are not dependent on the new df-struct
> stuff).  Then you can say "(R supw A) =/= ( Undef ` X )"
> instead of "(R supw A) e. X", if you want.

About iota functions there are also Hilbert's tau function that
you might want to consider. Theorically they look nice and practically
I found Lamport uses it a lot in its system (calling it "choose").

--
FL

[Norman Megill]

On Sep 26, 5:23 am, fl <frederic.l...@laposte.net> wrote:
[...]

> We could also uniformize the concept of partial function and of
> multi-valued function. In the latter case with my proposal we
> would return more than one element.

This won't work in general. For example, if the values of a
function are ordinals, there is no way to distinguish an
ordinal from the set of preceding ordinals, because they are
one and the same.

A standard way to handle multi-valued functions in e.g.
trignometry is to define a single-valued function on a
restricted "principal range".

I don't know what application you have in mind. But if you
really need to deal with multiple values, you can simply to
redefine it as a single-valued function, where single values
become singletons, two values become pairs, etc. The number
of values would be the cardinality of the value of this
redefined function. Then all values, whether single or
multiple, can be treated uniformly and within the existing
framework for functions.

> About iota functions there are also Hilbert's tau function that
> you might want to consider. Theorically they look nice and practically
> I found Lamport uses it a lot in its system (calling it "choose").

I assume you mean what is usually called Hilbert's epsilon.
It cannot be expressed as a definition in the language of
ZFC, but you would need to extend the syntax of ZFC and add
an axiom called the Transfinite Axiom. However, any theorem
that can be proved with Hilbert's epsilon can also be proved
in ZFC, as long as it doesn't contain the epsilon in the
statement of the theorem.

I wrote up a way to translate a proof using Hilbert's
epsilon into a pure ZFC proof:
http://us.metamath.org/downloads/megillaward2005he.pdf
(All the theorems mentioned there are in set.mm, although
some may have been renamed.)

Norm http://us.metamath.org/email.html

[fl]

> This won't work in general.  For example, if the values of a
> function are ordinals, there is no way to distinguish an
> ordinal from the set of preceding ordinals, because they are
> one and the same.

I don't understand. Suppose we have the ordinal (/), 1o, 2o, 3o

And a partial multi-valued function f with the domain { 1, 2, 3}

(f ` 1) not defined.
(f ` 2) returning 2o
(f ` 3) returning 1o and 2o
then we would have

(f ` 1) = (/)
(f ` 2) = { 2o }
(f ` 3) = { 1o , 2o }

> I don't know what application you have in mind.  

Simply the normal definition of limit always bothers me. This
function should return a collection (maybe empty of limits)
and the usual definition returns a value. I think the
consequence is we have to add extra conditions in the hypotheses
to ensure the limit exists and is unique whereas some theorem
could be expressed more compactly if we adopted my convention.

> I assume you mean what is usually called Hilbert's epsilon.

Curiously enough here it's called Hilbert's tau. Don't ask me why.

> It cannot be expressed as a definition in the language of
> ZFC, but you would need to extend the syntax of ZFC and add
> an axiom called the Transfinite Axiom.  However, any theorem
> that can be proved with Hilbert's epsilon can also be proved
> in ZFC, as long as it doesn't contain the epsilon in the
> statement of the theorem.

Well so we won't have the pleasure to see it in of set.mm

> I wrote up a way to translate a proof using Hilbert's
> epsilon into a pure ZFC proof:http://us.metamath.org/downloads/megillaward2005he.pdf
> (All the theorems mentioned there are in set.mm, although
> some may have been renamed.)

Thanks I will read it.

--
FL

[fl]

> Impressive.

But all that means we have something we can use as Hilbert's epsilon?


--
FL

[Norman Megill]

On Sep 26, 1:17 pm, fl <frederic.l...@laposte.net> wrote:
> > This won't work in general. For example, if the values of a
> > function are ordinals, there is no way to distinguish an
> > ordinal from the set of preceding ordinals, because they are
> > one and the same.
>
> I don't understand. Suppose we have the ordinal (/), 1o, 2o, 3o
>
> And a partial multi-valued function f with the domain { 1, 2, 3}
>
> (f ` 1) not defined.
> (f ` 2) returning 2o
> (f ` 3) returning 1o and 2o
> then we would have
>
> (f ` 1) = (/)
> (f ` 2) = { 2o }
> (f ` 3) = { 1o , 2o }

I misunderstood, sorry. I thought your idea was to extend
the behavior of standard single-valued functions, but you
are implementing nonstandard behavior since (f ` 2) returns
{ 2o } and not 2o like a standard function. So if you are
redefining functions so as to always return a set of values,
then an empty set of values makes sense for "not defined".

This is in fact what I had in mind in my sentence, "But if

you really need to deal with multiple values, you can simply
to redefine it as a single-valued function, where single
values become singletons, two values become pairs, etc."

The new Undef function is intended to be used with standard
single-valued functions. BTW I moved it to the main part of
set.mm for general use.

> > It cannot be expressed as a definition in the language of
> > ZFC, but you would need to extend the syntax of ZFC and add
> > an axiom called the Transfinite Axiom. However, any theorem
> > that can be proved with Hilbert's epsilon can also be proved
> > in ZFC, as long as it doesn't contain the epsilon in the
> > statement of the theorem.
>
> Well so we won't have the pleasure to see it in of set.mm

We can have it in the form of set B in theorem "hta".
http://us2.metamath.org:443/mpegif/hta.html
B works just like Hilbert's epsilon except that it must be
accompanied by the antecendent "R We A" in every
application. In fact, theorem "hta" is just Hilbert's
Transfinite Axiom with the antecedent "R We A".

> > I wrote up a way to translate a proof using Hilbert's
> > epsilon into a pure ZFC proof:http://us.metamath.org/downloads/megillaward2005he.pdf
> > (All the theorems mentioned there are in set.mm, although
> > some may have been renamed.)
>

> But all that means we have something we can use as Hilbert's epsilon?

Again, theorem "hta" provides that. Its purpose is to
provide a way to automate the translation of e.g. HOL
proofs. As long as the final theorem to be proved doesn't
itself contain epsilon, the antecedent "R We A" can be
discarded using "19.23aiv", "weth", and "ax-mp".

My guess is that "hta" won't be generally useful as a normal
proof method in set.mm because I think proofs will be
longer. But I may be wrong, and it is there if you want
to try.

Norm

[Marnix Klooster]

On Mon, Sep 26, 2011 at 6:24 PM, Norman Megill <n...@alum-2.mit.edu> wrote:

I wrote up a way to translate a proof using Hilbert's
epsilon into a pure ZFC proof:
http://us.metamath.org/downloads/megillaward2005he.pdf
(All the theorems mentioned there are in set.mm, although
some may have been renamed.)

A small note: this pdf links to page http://www.ghilbert.org/choice.txt which is not available anymore, but an archived copy is at http://web.archive.org/web/20061010113318/http://www.ghilbert.org/choice.txt.

Groetjes,
 <><
Marnix
--
Marnix Klooster
marnix....@gmail.com

[fl]

> an archived copy is at ...

I have began to read this interesting piece of Metamath's history.

To be complete on the subject let's add a presentation of HOL logic
(in Isabelle).

http://isabelle.in.tum.de/doc/logics-HOL.pdf

epsilon is denoted @ or SOME p. 5.

Hilbert's transfinite axiom is called rule someI p. 8.

--
FL