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.":)
