Hi Jim, Thank you for your very kind mail and help! For now it is optimized only for ` verify proof * ` and ` verify markup */… ` of Metamath (and you are right: I need quite a lot of theorems from the Mathboxes of other community members in the main part of set.mm, these are the markup failures), I just wanted to have some gut feelings and the widest possible collective wisdom about the whole enterprise at first:)
Peter On 1/17/22, Jim Kingdon <[email protected]> wrote: > Hey, thanks for sending those mathbox contributions. I see that you have > been communicating with various people in the past so you are not a > stranger to our community, but in case any of the following helps with > how we generally manage mathboxes, I hope it is helpful. > > I don't know how familiar you are with submitting pull requests in > github but just to see how close this submission is to being mergeable > (and in case it helps other people review it), I took what you sent to > the list and put it into github at > https://github.com/metamath/set.mm/pull/2435 . There are a number of > failures there which I assume do not surprise you (since you talk about > various issues in your email). We've tried to write an intro at > https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing > in case some or all of this git stuff is new to you. If you end up > making your own pull request I can just close this one. > > I guess my advice would be to try to get the mathbox in a state where it > can pass the checks and be merged as a mathbox, with relatively few > changes to main at first (even if that means some redundant theorems). > But there might be a bit of a case by case basis for some of these > issues. Hopefully there are some people here who are a bit more up on > these issues than I am because I don't really have a point-by-point > reaction without doing a bunch of research into topics I don't know well. > > Glad to hear that metamath has helped you learn set theory. Although I > knew little bits and pieces of set theory (and other topics) before I > got here, contributing to metamath has also been super helpful in terms > of my own understanding, both of topics such as set theory, construction > of real numbers, etc. In particular, my knowledge of constructive > mathematics was quite limited until I started contributing to iset.mm > and I have found that writing theorems there has been quite helpful, but > in aiding my learning directly, and also giving me a push to seek out > sources which I might not otherwise have found. > > On 1/17/22 2:58 AM, Mázsa Péter wrote: >> My purpose in set theory was to reveal the Partition-Equivalence >> Theorem with general ` R `. My results are attached as a Mathbox. >> Proofs and markup are verified, but I need some theorems of Thierry >> Arnoux, Scott Fenton, Frédéric Liné, Rodolfo Medina and Richard >> Penner, and my latexdefs, htmldefs and althtmldefs, in the main part >> of set.mm. Some theorems are slight modifications of theorems of Mario >> Carneiro, Rodolfo Medina and Norman Megill. >> >> Since the attached Mathbox is quite long (600+ necessary and >> sufficient definitions and theorems incl. versions), I‘ll now give you >> a summary. I’d like to discuss my results here on the email-list. >> >> I had to redefine some basic concepts (e.g. reflexivity, symmetry, >> transitivity, equivalence relation and equivalence relation with >> domain part, function, disjointness and partition), and suggest a new >> one (converse reflexivity), in order to reach the >> Partition-Equivalence Theorem. >> This motivation is very important here: I’m aware of the discussion >> https://github.com/metamath/set.mm/pull/1286 with the participation of >> Thierry Arnoux, Benoit Jubin, Normann Megill and David A. Wheeler, and >> if you find better definitions for reflexivity etc. than me, I do not >> oppose them from the outset. However it would be great if >> 1. At least reflexivity, symmetry and transitivity had coherent >> definitions (compare ~ df-refs and ~ df-syms below, as opposed to ~ >> issref with ` A ` vs. ~ cnvsym without ` A ` in set.mm), >> 2. Based on the 2. requirement of the Guidelines at >> http://us.metamath.org/mpeuni/mathbox.html all concepts were defined >> primarily as 0-ary class constants (like ~ df-refrels ), >> 3. Moreover, all class constants had a corresponding predicate for >> proper classes (like ~ df-refrel for _I in ~ refrelid $p |- RefRel _I >> ) so that e.g. in case of reflexive relations, the element of the >> class of all reflexive relations ( ~ elrefrels2 ) and the reflexive >> relation predicate ( ~ df-refrel ) were the same when ` R ` is a set: >> ~ elrefrelsrel $p |- ( R e. V -> ( R e. RefRels <-> RefRel R ) ) , >> 4. You proved that they reproduce at least ~ mpet $p |- ( MembPart A >> <-> MembEr A ) , ~ pet and ~ pets , or their (possible future) >> generalization, ` gpet ` , see below. >> >> After the (new, suggested) definitions you’ll find the (old) >> definitions which are presently in set.mm or in a Mathbox ( >> https://github.com/metamath/set.mm/blob/develop/set.mm ). >> >> _ >> Classes of all reflexive, converse reflexive, symmetric, transitive >> sets (new, suggested definitions, used only once in ~ df-refrels , ~ >> df-cnvrefrels , ~ df-symrels and ~ df-trrels below): >> df-refs $a |- Refs = { x | ( _I i^i ( dom x X. ran x ) ) _S ( x i^i ( >> dom x X. ran x ) ) } >> df-cnvrefs $a |- CnvRefs = { x | ( _I i^i ( dom x X. ran x ) ) `' _S ( >> x i^i ( dom x X. ran x ) ) } (new concept, we need it below at >> functions and disjoints) >> df-syms $a |- Syms = { x | `' ( x i^i ( dom x X. ran x ) ) _S ( x i^i >> ( dom x X. ran x ) ) } >> df-trs $a |- Trs = { x | ( ( x i^i ( dom x X. ran x ) ) o. ( x i^i ( >> dom x X. ran x ) ) ) _S ( x i^i ( dom x X. ran x ) ) } >> where ` _S ` is the subsets class, or the class of the subset >> relations (new, suggested definition): >> df-ssr $a |-_S = { <. x , y >. | x C_ y } , or ` df-ss `, since the >> present ~ df-ss definition of the subclass relation ` A C_ B ` should >> be relabeled as ` df-sc `. >> Scott Fenton's subset class ~ df-sset and ` _S ` are the same >> ssreqsset $p |- _S = SSet , >> however, the notation ` _S ` and the construction of ~ df-ssr reveals >> its similarity to these old definitions in set.mm: >> df-id $a |- _I = { <. x , y >. | x = y } and >> df-eprel $a |- _E = { <. x , y >. | x e. y } . >> >> Classes of all reflexive, etc. relations (new, suggested): >> df-refrels $a |- RefRels = ( Refs i^i Rels ) >> df-cnvrefrels $a |- CnvRefRels = ( CnvRefs i^i Rels ) >> df-symrels $a |- SymRels = ( Syms i^i Rels ) >> df-trrels $a |- TrRels = ( Trs i^i Rels ) >> where the relations class (new, suggested) is >> df-rels $a |- Rels = ~P ( _V X. _V ) . >> >> In predicate form the above definitions give: >> dfrefrel2 $p |- ( RefRel R <-> ( (_I i^i ( dom R X. ran R ) ) C_ R /\ Rel >> R ) ) >> ! dfrefrel3 $p |- ( RefRel R <-> ( A. x e. dom R A. y e. ran R ( x = y >> -> x R y ) /\ Rel R ) ) >> dfcnvrefrel2 $p |- ( CnvRefRel R <-> ( R C_ ( _I i^i ( dom R X. ran R >> ) ) /\ Rel R ) ) >> dfcnvrefrel3 $p |- ( CnvRefRel R <-> ( A. x e. dom R A. y e. ran R ( x >> R y -> x = y ) /\ Rel R ) ) >> dfsymrel2 $p |- ( SymRel R <-> ( `' R C_ R /\ Rel R ) ) >> dfsymrel3 $p |- ( SymRel R <-> ( A. x A. y ( x R y -> y R x ) /\ Rel R ) >> ) >> dftrrel2 $p |- ( TrRel R <-> ( ( R o. R ) C_ R /\ Rel R ) ) >> dftrrel3 $p |- ( TrRel R <-> ( A. x A. y A. z ( ( x R y /\ y R z ) -> >> x R z ) /\ Rel R ) ) >> Note that while ` Rel R ` cancels restriction of ` R ` , it keeps >> restriction of ` _I ` : this is why the very similar definitions ~ >> df-refs , ~ df-syms and ~ df-trs diverge when we switch from (general) >> sets to relations in ~ dfrefrel* , ~ dfsymrel* and ~ dftrrel* . >> >> Reflexivity and symmetry reproduce ` x R x ` for the reflexivity part, >> but only together: >> refsymrel2 $p |- ( ( RefRel R /\ SymRel R ) <-> ( ( (_I |` dom R ) C_ >> R /\ `' R C_ R ) /\ Rel R ) ) >> ! refsymrel3 $p |- ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R x >> R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) ) >> Reflexivity and symmetry are often bound together in equivalence >> relation. Reflexivity may be perceived primarily as a necessary part >> of equivalence. This seems to be the main reason why we thought so far >> that reflexivity on its own should be defined like the reflexivity >> part of ~ dfeqvrel3 below, i.e., by using the apparently self-evident >> ` x R x ` form. >> Another possible reason is that we are inclined to constrain ourselves >> to convenient special cases where the two forms are equivalent, e.g. >> the one with square Cartesian product: >> idinxpssinxp3 $p |- ( (_I i^i ( A X. A ) ) C_ ( R i^i ( A X. A ) ) >> <-> (_I |` A ) C_ R ) and >> idinxpssinxp4 $p |- ( A. x e. A A. y e. A ( x = y -> x R y ) <-> A. x >> e. A x R x ) . >> >> Old reflexivity versions in set.mm or in a Mathbox now, with ` x R x `: >> df-reflexive $a |- ( R Reflexive A <-> ( R C_ ( A X. A ) /\ A. x e. A x R >> x ) ) >> issref $p |- ( (_I |` A ) C_ R <-> A. x e. A x R x ) >> >> Equivalence relations (new, suggested for set.mm, but other math >> sources seem to define it in a way which is similar to this one): >> df-eqvrels $a |- EqvRels = ( ( RefRels i^i SymRels ) i^i TrRels ) >> which gives >> dfeqvrel2 $p |- ( EqvRel R <-> ( ( (_I |` dom R ) C_ R /\ `' R C_ R >> /\ ( R o. R ) C_ R ) /\ Rel R ) ) >> dfeqvrel3 $p |- ( EqvRel R <-> ( ( A. x e. dom R x R x /\ A. x A. y ( >> x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) >> /\ Rel R ) ) >> There is no comparable definition of equivalence relation now in set.mm. >> >> Equivalence relations with domain part (new, suggested): >> df-ers $a |- Ers = ( DomainQss |` EqvRels ) >> where df-dmqss $a |- DomainQss = { <. x , y >. | ( dom x /. x ) = y } >> which gives >> dferALTV2 $p |- ( R ErALTV A <-> ( EqvRel R /\ ( dom R /. R ) = A ) ) >> This definition implies that the natural domain of equivalence relations >> is not ` R Domain A ` (i.e. ` dom R = A ` cf. ~ brdomaing ), like in >> the present ~ df-er in set.mm, >> but ` R DomainQss A ` (i.e. ` ( dom R /. R ) = A ` , cf. ~ brdmqss ), >> "domain quotients". >> The main reason why I think the new ` R DomainQss A ` to be the >> natural domain (and not the old ` R Domain A ` ) is a small set of new >> theorems, the Membership Partition-Equivalence Theorems (see mpet* >> below) and the Partition-Equivalence Theorems (see pet* below). >> Incidentally, with the new definitions above, the old ~ prter3 in set.mm >> prter3 $p |- ( ( R Er U. A /\ ( U. A /. R ) = ( A \ { (/) } ) ) -> .~ = R >> ) >> simplifies to the new >> erALTVimlem $p |- ( R e. V -> ( R ErALTV A -> ~ A = R ) ) >> where the coelements ` ~ A ` are a special case of cosets ` ,~ R ` : >> df-coss $a |- ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) } >> df-coels $a |- ~ A = ,~ ( `' _E |` A ) >> dfcoels $p |- ~ A = { <. x , y >. | E. u e. A ( x e. u /\ y e. u ) } >> While I'm sure we need both equivalence relation ~ df-eqvrels and >> equivalence relation on domain quotient ~ df-ers , I'm not sure >> whether we need a third equivalence relation concept with the present >> ` dom R = A ` component as well: this needs further investigation. >> Using Occam’s razor I suppose that these two concepts ~ df-eqvrels and >> ~ df-ers are enough and named the predicate version of the one on >> domain quotient as the alternate version ~ df-erALTV of the present ~ >> df-er (cf. "Alternative (ALTV) versions", >> http://us.metamath.org/mpeuni/conventions.html ). >> >> The old definition of equivalence relation (with a domain part) in set.mm >> df-er $a |- ( R Er A <-> ( Rel R /\ dom R = A /\ ( `' R u. ( R o. R ) ) C_ >> R ) ) >> "is not standard" , "somewhat cryptic", has no corresponding costant >> 0-ary class, does not follow the traditional transparent >> reflexive-symmetric-transitive relation way of definition of >> equivalence, and fails to deliver the Membership >> Partition-Equivalence Theorems and the Partition-Equivalence Theorems. >> >> With the new definitions above comes the >> Main Theorem of Equivalences: any equivalence relation implies >> equivalent membership as well >> mainer $p |- ( R ErALTV A -> MembEr A ) >> where >> df-member $a |- ( MembEr A <-> ~ A ErALTV A ) >> dfmember3 $p |- ( MembEr A <-> ( EqvRel ~ A /\ ( U. A /. ~ A ) = A ) ) >> >> Now we should define functions and disjoints (new, suggested): >> df-funss $a |- Funss = { x | ,~ x e. CnvRefRels } , used only once in >> df-funsALTV below >> df-funsALTV $a |- FunsALTV = ( Funss i^i Rels ) >> dffunALTV2 $p |- ( FunALTV F <-> ( ,~ F C_ _I /\ Rel F ) ) >> The new definition of the function predicate ~ df-funALTV (based on a >> more general, converse reflexive, relation) and the old definition of >> function in set.mm ~ df-fun , are the same: >> funALTVfun $p |- ( FunALTV F <-> Fun F ) >> >> df-disjss $a |- Disjss = { x | ,~ `' x e. CnvRefRels } , used only >> once in df-disjs below >> df-disjs $a |- Disjs = ( Disjss i^i Rels ) >> We need ` Disjs ` and ` Disj R ` for the definition of ` Parts ` and ` >> R Part A ` for the Partition-Equivalence Theorems: this need for ` >> Parts ` as disjoint relations on their domain quotients is the reason >> why we should define ` Disjs ` instead of simply using converse >> functions, cf. ~ pet2 below. >> dfdisjALTV2 $p |- ( Disj R <-> ( ,~ `' R C_ _I /\ Rel R ) ) , (read: ` >> R ` is a disjoint) >> dfdisjALTV4 $p |- ( Disj R <-> ( A. x E* u u R x /\ Rel R ) ) >> dfdisjALTV5 $p |- ( Disj R <-> ( A. u e. dom R A. v e. dom R ( u = v >> \/ ( [ u ] R i^i [ v ] R ) = (/) ) /\ Rel R ) ) >> The old definition of disjointness in set.mm is >> df-disj $a |- ( Disj_ x e. A B <-> A. y E* x e. A y e. B ) >> >> The disjoint elementhood predicate (read: the elements of ` A ` are >> disjoint) is a special case of disjointness (new, suggested): >> df-eldisj $a |- ( ElDisj A <-> Disj ( `' _E |` A ) ) >> dfeldisj5 $p |- ( ElDisj A <-> A. u e. A A. v e. A ( u = v \/ ( u i^i >> v ) = (/) ) ) >> As of now, disjoint elementhood is defined as "partition" in set.mm : >> df-prt $a |- ( Prt A <-> A. u e. A A. v e. A ( u = v \/ ( u i^i v ) = >> (/) ) ) (cf. the new partition definitions below) >> Disjoint elementhood changes >> prter1 $p |- ( Prt A -> .~ Er U. A ) of the present set.mm to >> mdisjim $p |- ( ElDisj A -> EqvRel ~ A ) >> and in general form, the >> "Divide et Aequivalere" Theorem (new): every disjoint relation >> generates equivalent cosets by the relation >> disjim $p |- ( Disj R -> EqvRel ,~ R ) >> Moreover, this changes >> prter2 $p |- ( Prt A -> ( U. A /. .~ ) = ( A \ { (/) } ) ) of the >> present set.mm to >> eldisjn0el $p |- ( ElDisj A -> ( -. (/) e. A <-> ( U. A /. ~ A ) = A ) ) >> and in general form (new): >> disjdmqseq $p |- ( Disj R -> ( ( dom R /. R ) = A <-> ( dom ,~ R /. ,~ >> R ) = A ) ) >> >> Partitions (new, suggested) are disjoints on domain quotients (or: >> domain quotients restricted to disjoints): >> df-parts $a |- Parts = ( DomainQss |` Disjs ) $. >> dfpart2 $p |- ( R Part A <-> ( Disj R /\ ( dom R /. R ) = A ) ) >> The above definition is a more general meaning of partition than we >> accustomed to: the conventional meaning of partition (e.g. partition >> ` A ` of ` X `, [Halmos] p. 28: "A partition of ` X ` is a disjoint >> collection ` A ` of non-empty subsets of ` X ` whose union is ` X ` ", >> or Definition 35, [Suppes] p. 83., cf.https://oeis.org/A000110 ) is >> what we call here membership partition: >> dfmembpart2 $p |- ( MembPart A <-> ( ElDisj A /\ -. (/) e. A ) ) , defined >> as >> df-membpart $a |- ( MembPart A <-> ( `' _E |` A ) Part A ) >> >> A (somewhat maybe depressing, new) theorem with the membership >> partition concept above is the >> Theorem of Fences by Equivalences: all kinds of equivalence relations >> imaginable (in addition to the membership equivalence relation cf. ~ >> mpet ) generate partition of the members: >> fences $p |- ( R ErALTV A -> MembPart A ) >> >> Now we are ready to prove the (new) Membership Partition-Equivalence >> Theorems: >> mpet3 $p |- ( ( ElDisj A /\ -. (/) e. A ) <-> ( EqvRel ~ A /\ ( U. A >> /. ~ A ) = A ) ) >> mpet2 $p |- ( ( `' _E |` A ) Part A <-> ,~ ( `' _E |` A ) ErALTV A ) >> mpet $p |- ( MembPart A <-> MembEr A ) >> >> and the (new) Partition-Equivalence Theorems, with general ` R `: >> pet2 $p |- ( ( Disj ( R (x) ( `' _E |` A ) ) /\ ( dom ( R (x) ( `' _E >> |` A ) ) /. ( R (x) ( `' _E |` A ) ) ) = A ) <-> ( EqvRel ,~ ( R (x) ( >> `' _E |` A ) ) /\ ( dom ,~ ( R (x) ( `' _E |` A ) ) /. ,~ ( R (x) ( `' >> _E |` A ) ) ) = A ) ) >> pet $p |- ( ( R (x) ( `' _E |` A ) ) Part A <-> ,~ ( R (x) ( `' _E |` >> A ) ) ErALTV A ) >> pets $p |- ( ( A e. V /\ R e. W ) -> >> ( ( R (x) ( `' _E |` A ) ) Parts A <-> ,~ ( R (x) ( `' _E |` A ) ) Ers >> A ) ) >> where >> br1cosstxpcnvepres $p |- ( ( ( B e. V /\ C e. W ) /\ ( D e. X /\ E e. Y ) >> ) -> >> ( <. B , C >. ,~ ( R (x) ( `' _E |` A ) ) <. D , E >. <-> >> E. u e. A ( ( C e. u /\ u R B ) /\ ( E e. u /\ u R D ) ) ) ) >> >> This small set of theorems is the main result of my investigations in >> set theory. ~ pet is not more general than the conventional Membership >> Partition-Equivalence Theorem ~ mpet2 (because you cannot set ` R ` in >> ~ pet in a way that you would get ~ mpet2 ), i.e., this is not the >> hypothetical General Partition-Equivalence Theorem ` gpet |- ( R Part >> A <-> ,~ R ErALTV A ) `. But ~ pet has a general part that ~ mpet2 >> lacks: ` R `, which is well enough for my future application of set >> theory, for my purpose outside of set theory. Motto: "Le meglio è >> l'inimico del bene.":) > > -- > 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/a6e056df-2e1b-0506-9c67-77d26bb5ecbc%40panix.com. > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJJTU5oY7RMsqmME9i50cVhnZA-1wE13%2BNOT3rMbOu9KFRP5MA%40mail.gmail.com.
