Alternative definitions for function's and operations's values

[Alexander van der Vekens]

I just created a pull request to update my mathbox with the results of my investigations concerning alternative definitions for function's and operations's values:
Instead of evaluating to the empty set if the involved classes are not meaningful or the function/operation is not defined for the given argument(s), as it is the case for the current definitions df-fv and df-ov,  I provided alternative definitions df-afv and df-aov which evaluate to the universal class in this case.
This has the advantage that there is no ambiguity if the function's/operation's value is defined or not (from (F`X) = (/) this cannot be concluded, e.g. if (/) e. ran F). Especially for working with partial functions this would be helpful.

More explanations/results will be available in my mathbox.

Since the whole current set.mm is based on this fundamental concepts like functions and operations, I think the current definitions are essential for Methamath. But it would be interesting which (of the advanced) theorems could be proven with the alternative definition (in addition to the basic theorems I proved).

However, I wonder if there were discussions already in the past about the advantages and disadvantages of the current convention, and how it was decided that the functions/operations should evaluate to the empty set. As already said in the comment on df-fv in set.mm, "our definition apparently does not appear in the literature"...

Is there more (historical) information available about this topic?

Regards,
Alexander

[Norman Megill]

While there isn't a specific thread I could find on this topic, "fvex" is a good search term to use.  For example:

See the last line of
https://groups.google.com/d/msg/metamath/cELWj7viywk/IJvnOyOGAAAJ

In a discussion of partial functions
https://groups.google.com/d/msg/metamath/rIivIz9YTCY/cA5hMi2vWdIJ

In a discussion of riota return value
https://groups.google.com/d/msg/metamath/NajM4onD26A/u4L5Dw-aEgAJ

I understand the issue you are raising, and we have considered your approach in the past.  The problem is that instead of being able to us fvex to show immediately the function value is a set, we have to prove that the argument belongs to the domain every time we require it to be a set.  This will result in a significant size increase of many proofs.  There are currently 1828 proofs that use fvex.

From a practical point of view, in most theorems we are already working with values in the domain, so the fact that (F ` A) is (/) outside of the domain is not important.  I think about all we lose is the ability to do tricks like (F ` A) e. _V telling us that the value is in the domain, but that would probably be rarely used, and the overhead associated with doing that would be about the same as that needed to show (F ` A) e. dom F.

Norm

[Norman Megill]

On Saturday, August 5, 2017 at 4:28:03 PM UTC-4, Norman Megill wrote:

From a practical point of view, in most theorems we are already working with values in the domain, so the fact that (F ` A) is (/) outside of the domain is not important.  I think about all we lose is the ability to do tricks like (F ` A) e. _V telling us that the value is in the domain, but that would probably be rarely used, and the overhead associated with doing that would be about the same as that needed to show (F ` A) e. dom F.

Oops, I meant "show A e. dom F".
 

Norm

[Norman Megill]

Alexander,

Here are Gérard's comments on your alternative function and operation value definition.  You can update your mathbox accordingly if you agree.

For the function value df-afv, I would propose ''' (apostrophes) so that it's easier to distinguish from df-fv and df-ima.  And not ``` (backticks) since that would  be annoying to escape in a comment, requiring ` ( F `````` A ) `.

A minor thing is the use of @ in def@ ("defined at", df-dfat).  I have been using the @ informally as a replacement for $ in commented out sections that may be deleted some day, as you can see in many places by searching for @, and I think other people have also.  While there is no violation of any standard to use the @ in a token, my only concern is that it makes the search for such commented-out sections slightly more difficult.  I will leave it up to you whether to change def@ to something else, though.

Norm

[begin quote]

Dear Norm,
I have been somewhat disturbed to see in the recent update of the Matchbox of Alexander van der Vekens 18.21.10 (2.5 Alternative definition of a function) that the new syntax item cafv (27370) uses exactly the same symbolism "class (F’A)" that is already used by the far older syntax item cdv (5221), when the new definition df-afv (27271) is most similar but not exactly identical with the old df-fv (5229).
So that, in my opinion, reading some theorems in the section 18.21.10 may cause real psychological disease. This is typically the case for theorem dfafv2 (27372), where this alternative new definition seems to be an autoreference at first look, when a closer look proves that this is not the case in fact. But others theorems also look odd, like the series from afvpcfv0 (27386) to  afvfv0bi (27392).
I would like to suggest that maybe a symbolic like class (F’’’A) could be preferable for the syntax item cdv.
Moreover, in the comment for the theorems ndmaovass (27445) and ndmaovdistr (27446), the respective references ndmovass (5969) and ndmovdistr (5970) should replace the current 
autoreferences.
Très amicalement.
Gérard Lang

P.S.: I like the symmetry of the current (quasi-) symmetric formulation of ax-7 and would not like this to change.
I also like the proposition by Scott Fenton « Axiom of distinctness » as a name for ax-17.
[end quote]

On Saturday, August 5, 2017 at 3:13:45 PM UTC-4, Alexander van der Vekens wrote:

[Alexander van der Vekens]

Hi Norman,
thank you for the hints, I will update my mathbox accordingly. However, see my comments below.

Regards,
Alexander

Am Donnerstag, 10. August 2017 13:55:13 UTC+2 schrieb Norman Megill:

Alexander,

Here are Gérard's comments on your alternative function and operation value definition.  You can update your mathbox accordingly if you agree.

For the function value df-afv, I would propose ''' (apostrophes) so that it's easier to distinguish from df-fv and df-ima.  And not ``` (backticks) since that would  be annoying to escape in a comment, requiring ` ( F `````` A ) `.

OK - although it was my intention to find a symbol similar to ` , and that ( F ` A ) and ( F ' A ) should be almost identical, I understand that it is confusing (and I had problems to read some theorems by myself), so I will follow your suggestion.

A minor thing is the use of @ in def@ ("defined at", df-dfat).  I have been using the @ informally as a replacement for $ in commented out sections that may be deleted some day, as you can see in many places by searching for @, and I think other people have also.  While there is no violation of any standard to use the @ in a token, my only concern is that it makes the search for such commented-out sections slightly more difficult.  I will leave it up to you whether to change def@ to something else, though.

 

I expected such a remark, but I wanted to give it a try. But, of course, you are right, I'll change the token to "defAt" ...