Excluding (/) from extensible structure to be a function

[Alexander van der Vekens]

I wonder why (/) is/must be excluded from an extensible structure to be a function:

df-struct $a |- Struct = { <. f , x >. | ( x e. ( <_ i^i ( NN X. NN ) ) /\

       Fun ( f \ { (/) } ) /\ dom f C_ ( ... ` x ) ) } $.

Why Fun ( f \ { (/) } ) and not simply Fun f ?

I searched for a justification in set.mm and also in the google group, but I did not find any hint. Formerly, there wasn't such a restriction, see https://groups.google.com/g/metamath/c/BFFSR3b5qEo/m/s6vph-zL_DoJ.

Can anybody explain this restriction? Is there any meaningful structure which contains the empty set, e .g. S = { (/) ,  <. ( Base ` ndx ) , B >. , <. ( E ` ndx ) , .+ >. } (will Fun S not hold in this case?)?

[Mario Carneiro]

It's not excluding `(/)` from being an extensible structure, it is rather the opposite: it asserts that f with (/) removed is a function. It is impossible for any set containing (/) to be a function, because a function is a set of ordered pairs and (/) is not an ordered pair. So this is being unusually relaxed and letting structures that contain (/) still be considered structures even if they are not, strictly speaking, functions.

As for why the unusual allowance, this is a trick used to ensure that expressions like { <. A, B >. , <. C, D >. } are structures without asserting or implying that A,B,C,D are sets. This is used critically in strle1, strle2, strle3, strleun to avoid sethood hypotheses on the "payload" sets: without this, ipsstr and theorems like it will have many sethood assumptions, and may not even be usable in the empty context. Instead, the sethood assumption is deferred until it is actually needed, e.g. ipsbase, which requires that the base set is a set but not any of the other components.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8213c12b-c060-4d15-b1d7-62a58536b724n%40googlegroups.com.

[Alexander van der Vekens]

Thank you, Mario, for your explanation. It sounds reasonable, although it is more difficult to proof certain theorems for arbitrary extensible structures: Since we cannot assume Fun S if S struct X (only Fun ( S \ { (/) } ), see ~  structn0fun, or equivalently Fun `' `'  S, see ~ structfung), special versions of theorems with antecedent Fun F are needed (see, for example, ~fundmge2nop0 vs. ~fundmge2nop).

I plan to add this explanation to the comment within set.mm, so that it is documented for everybody and for the future.

Alexander

[David A. Wheeler]

> On Nov 15, 2021, at 9:49 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
>
> Thank you, Mario, for your explanation. It sounds reasonable, although it is more difficult to proof certain theorems for arbitrary extensible structures: Since we cannot assume Fun S if S struct X (only Fun ( S \ { (/) } ), see ~ structn0fun, or equivalently Fun `' `' S, see ~ structfung), special versions of theorems with antecedent Fun F are needed (see, for example, ~fundmge2nop0 vs. ~fundmge2nop).
>
> I plan to add this explanation to the comment within set.mm, so that it is documented for everybody and for the future.

Excellent! I love to see documentation on *why* things are done,
thanks for offering to do that.

If you could, please include links to examples (e.g., ~ strle1 ).
The more hyperlinks there are between various entries, the easier
It is to see their interrelationships. I also think it’s fun to start in one
place and in a few links discover relationships you hadn’t anticipated.

--- David A. Wheeler

[Mario Carneiro]

I want to add that df-struct is essentially a technical definition made so as to make efficient (linear time) the proofs of n-ary versions of strle3. It is not meant to stake any claim on what a structure "is", and for various reasons you might want to add or remove hypotheses relative to df-struct. The main utility of this particular definition is that you can prove component extraction theorems easily, as long as all the components are written in increasing numerical order.

Historically, the definition of a structure is simply any set; we simply apply (Base`G) and (+g`G) and so on and use what we get without regard to how those operations are computed from G, whether it is a function or anything else. df-struct does not change this; it is a tool meant to help prove the component extraction theorems for particular structures given as finite sets of ordered pairs, and it is not a supertype of every structure - df-mgm does not mention it and is still defined with respect to all sets.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/379C3F57-E834-4B7B-9A38-102548E73743%40dwheeler.com.