Back to school
Nov. 6th, 2019 05:23 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
sassa_nfProve union of sets is commutative.
Ok, there may be a problem with the question - in ZFC Union is defined on a set of sets, so no order is there.
At first I solved for a system where sets are defined through a membership function, and define union as a set where membership is a logical or of two memberships.
But in ZFC Union of a Pair of sets is not defined through membership functions. Let's show then that the two definitions of Union are equivalent.
One problem later, here it goes:
Ok, there may be a problem with the question - in ZFC Union is defined on a set of sets, so no order is there.
At first I solved for a system where sets are defined through a membership function, and define union as a set where membership is a logical or of two memberships.
But in ZFC Union of a Pair of sets is not defined through membership functions. Let's show then that the two definitions of Union are equivalent.
One problem later, here it goes:
data False : Set where
data _==_ {A : Set} (x : A) : A -> Set where
refl : x == x
data Bool : Set where
true : Bool
false : Bool
_||_ : Bool -> Bool -> Bool
true || n = true
false || n = n
-- introduce a Set (well, let's call it type S) consisting of a membership function.
data S {A : Set} : Set where
set : (A -> Bool) -> S {A}
ismember : {A : Set} -> S {A} -> A -> Bool
ismember (set m) = m
-- then a union is a set whose membership function computes a boolean disjunction. Fair?
union : {A : Set} -> S {A} -> S {A} -> S {A}
union (set m) (set n) = set \x -> (m x) || (n x)
-- extensionality axiom: if for all x we can tell that the membership function of set m and n returns the same result,
-- then the two sets are equal
postulate ext : {A : Set} -> (m n : S {A}) -> ((x : A) -> (ismember m x) == (ismember n x)) -> m == n
{-# BUILTIN EQUALITY _==_ #-}
-- lemma: both ways of constructing a union of two sets produces equal membership function.
-- the definition of union can be used to prove that membership functions of unions return the same result
union-comm' : {A : Set} {m n : S {A}} -> (x : A) -> (ismember (union m n) x) == (ismember (union n m) x)
union-comm' {A} {set m} {set n} x with m x | n x
... | false | false = refl -- break down case by case, so Agda can follow different branches in two unions
... | false | true = refl
... | true | false = refl
... | true | true = refl
-- commutativity of union of sets: extensionality axiom combined with the lemma that both ways of
-- constructing a union of two sets produces the same membership result
union-comm : {A : Set} {m n : S {A}} -> (union m n) == (union n m)
union-comm {A} {m} {n} = ext {A} (union m n) (union n m) (union-comm' {A} {m} {n})
postulate set-pair : {A : Set} -> (m n : S {A}) -> S {S {A}}
postulate pair-member-l : {A : Set} -> (m n : S {A}) -> (ismember (set-pair m n) m) == true
postulate pair-member-r : {A : Set} -> (m n : S {A}) -> (ismember (set-pair m n) n) == true
postulate pair-is : {A : Set} {m n : S {A}} {x : S {A}} ->
(ismember (set-pair m n) x) == true ->
(m == x -> False) -> (n == x -> False) -> False
postulate set-union : {A : Set} -> S {S {A}} -> S {A}
postulate union-member : {A : Set} -> (a : S {S {A}}) ->
(x : A) -> (d : S {A}) ->
(ismember d x) == true ->
(ismember a d) == true -> (ismember (set-union a) x) == true
postulate union-set : {A : Set} -> (a : S {S {A}}) -> (x : A) -> (ismember (set-union a) x) == true -> S {A}
postulate union-set-member : {A : Set} {a : S {S {A}}} {x : A} ->
(p : (ismember (set-union a) x) == true) ->
(ismember (union-set a x p) x) == true
postulate union-set-member-set : {A : Set} {a : S {S {A}}} {x : A} ->
(p : (ismember (set-union a) x) == true) ->
(ismember a (union-set a x p)) == true
false-elim : {A : Set} -> False -> A
false-elim ()
bool-mismatch : false == true -> False
bool-mismatch ()
transport : {A : Set} {B : A -> Set} {x y : A} -> x == y -> B x -> B y
transport refl bx = bx
trans : {A : Set} {x y z : A} -> x == y -> y == z -> x == z
trans refl refl = refl
sym : {A : Set} {x y : A} -> x == y -> y == x
sym refl = refl
ext-inv : {A : Set} {m n : S {A}} -> m == n -> (x : A) -> (ismember m x) == (ismember n x)
ext-inv {A} {m} {n} m=n x = transport {B = \n -> (ismember m x) == (ismember n x)} m=n refl
non-eq-set : {A : Set} {m n : S {A}} {x : A} -> (ismember m x) == false -> (ismember n x) == true -> m == n -> False
non-eq-set {A} {m} {n} {x} nxm x-n m=n = bool-mismatch (trans (sym nxm) (trans (ext-inv m=n x) x-n))
union-match : {A : Set} -> (m n : S {A}) -> (x : A) ->
((ismember m x) || (ismember n x)) == (ismember (union m n) x)
union-match (set m) (set n) x with m x | n x
... | false | false = refl
... | true | false = refl
... | false | true = refl
... | true | true = refl
member-|| : {A : Set} {x : A} {a b : Bool} -> (m n : S {A}) ->
(ismember m x) == a -> (ismember n x) == b -> (a || b) == ((ismember m x) || (ismember n x))
member-|| _ _ m=a n=b rewrite m=a | n=b = refl
{-- originally a dumb straightforward christmas tree of cases and matching
-- this does not require defining BUILTIN EQUALITY for rewrite syntax sugar to work
member-|| m n x a b m=a n=b with a | ismember m x | b | ismember n x
... | false | false | false | false = refl
... | false | false | true | true = refl
... | true | true | _ | _ = refl
... | false | true | _ | _ = false-elim (bool-mismatch (sym m=a))
... | true | false | _ | _ = false-elim (bool-mismatch m=a)
... | _ | _ | false | true = false-elim (bool-mismatch (sym n=b))
... | _ | _ | true | false = false-elim (bool-mismatch n=b)
--}
data _==?_ {A : Set} (x y : A) : Set where
yes : x == y -> x ==? y
no : (x == y -> False) -> x ==? y
ismember? : {A : Set} -> (m : S {A}) (x : A) -> (ismember m x) ==? true
ismember? m x with ismember m x
... | true = yes refl
... | false = no \()
not-true : {x : Bool} -> (x == true -> False) -> x == false
not-true {true} nxm = false-elim (nxm refl)
not-true {false} _ = refl
member-union-l : {A : Set} {x : A} -> (m n : S {A}) -> (ismember m x) == true -> true == (ismember (union m n) x)
member-union-l {A} {x} m n x-m with ismember? n x
... | yes x-n = trans (member-|| m n x-m x-n) (union-match m n x)
... | no nxn = trans (member-|| m n x-m (not-true nxn)) (union-match m n x)
member-union-r : {A : Set} {x : A} -> (m n : S {A}) -> (ismember n x) == true -> true == (ismember (union m n) x)
member-union-r {A} {x} m n x-n = transport {B = \u -> true == (ismember u x)}
(union-comm {A} {n} {m})
(member-union-l n m x-n)
member-union-f : {A : Set} {x : A} -> (m n : S {A}) -> (ismember m x) == false ->
(ismember n x) == false -> false == (ismember (union m n) x)
member-union-f {A} {x} m n nxm nxn = trans (member-|| m n nxm nxn)
(union-match m n x)
-- axiom that set equality is decidable
-- this is not needed for the proof of equality of two representations of unions,
-- but it is needed if we were to express union-member-r from union-member-l -
-- that requires pairs-eq
postulate sets-equal? : {A : Set} (m n : S {A}) -> m ==? n
pairs-eq' : {A : Set} -> (m n x : S {A}) -> (ismember (set-pair m n) x) == (ismember (set-pair n m) x)
pairs-eq' m n x with sets-equal? m x | sets-equal? n x
... | yes m=x | _ = trans (transport {B = \x -> ismember (set-pair m n) x == true} m=x (pair-member-l m n))
(sym (transport {B = \x -> ismember (set-pair n m) x == true} m=x (pair-member-r n m)))
... | _ | yes n=x = trans (transport {B = \x -> ismember (set-pair m n) x == true} n=x (pair-member-r m n))
(sym (transport {B = \x -> ismember (set-pair n m) x == true} n=x (pair-member-l n m)))
... | no nxm | no nxn = trans (not-true \p -> pair-is p nxm nxn)
(sym (not-true \p -> pair-is p nxn nxm))
pairs-eq : {A : Set} -> (m n : S {A}) -> (set-pair m n) == (set-pair n m)
pairs-eq m n = ext (set-pair m n) (set-pair n m) (pairs-eq' m n)
union-member-l : {A : Set} {m n : S {A}} {x : A} -> (ismember m x) == true -> (ismember (set-union (set-pair m n)) x) == true
union-member-l {A} {m} {n} {x} x-m = union-member (set-pair m n) x m x-m (pair-member-l m n)
union-member-r : {A : Set} {m n : S {A}} {x : A} -> (ismember n x) == true -> (ismember (set-union (set-pair m n)) x) == true
union-member-r {A} {m} {n} {x} x-n = transport {B = \u -> (ismember (set-union u) x) == true}
(pairs-eq n m)
(union-member-l {A} {n} {m} x-n)
union-pair' : {A : Set} -> (m n : S {A}) -> (x : A) ->
(ismember (set-union (set-pair m n)) x) == (ismember (union m n) x)
union-pair' {A} m n x with ismember? m x | ismember? n x
... | yes x-m | _ = trans (union-member-l x-m) (member-union-l m n x-m)
... | _ | yes x-n = trans (union-member-r x-n) (member-union-r m n x-n)
... | no nxm | no nxn with ismember? (set-union (set-pair m n)) x
... | yes x-u = false-elim (pair-is (union-set-member-set x-u)
(non-eq-set (not-true nxm) (union-set-member x-u))
(non-eq-set (not-true nxn) (union-set-member x-u)))
... | no nxu = trans (not-true nxu)
(member-union-f m n (not-true nxm) (not-true nxn))
-- The two representations of unions of sets are equivalent
union-pair : {A : Set} -> (m n : S {A}) -> (set-union (set-pair m n)) == (union m n)
union-pair m n = ext (set-union (set-pair m n)) (union m n) (union-pair' m n)
no subject
Date: 2019-11-06 06:41 pm (UTC)Do I understand it correct that you have to use underlying sets to define this `Set`?
no subject
Date: 2019-11-06 07:55 pm (UTC)So data Bool : Set only means that "Bool is a Type", and there are two constructors for it: true and false.
I am told this is not a very easy way to express the problem. So I'll ping the guy to see what the canonical way would be. But as for me, I wanted to get through the thick of it to see that I can actually solve it.
The complications may be even not warranted. Just the way I expressed things revolve around equality (_==_), which I can construct from transitivity of equality (here it's trans). Some of the things had to be proven as separate lemmas, because they are not obvious to Agda (and perhaps for a good reason).
The lot of postulates are really different parts of Pairing and Union axioms, and probably could be reduced to a single statement per axiom, if I introduced new types. As such then it becomes seriously clunky - have to pass everything each function needs as separate arguments.
Like, set-pair - is the part of the Pairing axiom that states "for any sets A and B there exists a set C". Then pair-member-l is the part of the axiom that states "...and A is a member of C [constructed for a pair of A and B by the set-pair]".
Then, because there is no way to express "D == A or D == B", because equality in my example is a type, not a boolean function, I have to use "not (D != A and D != B)". (The "(m == x -> False) -> (n == x -> False) -> False" part of pair-is. You shouldn't really use Either (m == x) (n == x) here, because Either not only says "D == A or D == B", but actually provides a Choice - it points which of D == A and D == B it actually is.)
Because I chose the sets membership test function so that it returns Bool, then proof that an element is a member is witnessing that ismember m x == true. Now we are stuck expressing everything using transitivity, symmetry, and transport (transport a dependent value along the path defined by an equality).
Stuff in curly braces {...} are implicits. The values are needed, but Agda may work out what is meant there from the context, so the calls then are less cluttered. But sometimes it can't, so have to pass it explicitly. So I had to add it in places where Agda was stuck unable to solve meta problems. Eg the silly looking {m = m}, or less trivial {B = \n -> (ismember m x) == (ismember n x)}. This latter one says "B is a type that depends on one parameter, n", or "given a value of suitable type, n, B produces a type". So, for example, (B m) produces a type "(ismember m x) == (ismember m x)", and (B n) produces a type "(ismember m x) == (ismember n x)". This can then be used to "cast" or substitute one value for another, if I can show that "m == n".
Or a better example is member-union-r. Instead of copy-pasting member-union-l with subtle changes, I can use member-union-l to prove the needed fact for a slightly different union - for a union with m and n swapped around. Then because the types are actually different, you cannot assign values arbitrarily. But you can transport a value of type "true == ismember _ x" from one dependent type to the other, if you can prove the values of the parameter are equal. That is, a value of type "true == ismember (union n m) x" is transported to a value of type "true == ismember (union m n) x", because I can prove "union n m == union m n" using union-comm. At the spot where transport is called, I provided only the implicit type {B}, and Agda worked out {A}, {m} and {n} from the types of arguments - union-comm's return type "union n m == union m n" identifies the values for {m} and {n} for transport unambiguously.
An example that didn't quite work - data S {A : Set} : Set - it only means "given a type A, S is a type". I wanted A to be implicit, hoping Agda can work out which type is needed in each case (eg then type signature for binary operations would be shorter, S -> S -> S, instead of having to mention {A} everywhere), but it looks like it didn't work.
Anyway, I don't know if this detail is interesting, if you haven't done Agda, but for me it was an interesting exercise.
no subject
Date: 2019-11-06 09:50 pm (UTC)no subject
Date: 2019-11-06 11:41 pm (UTC)By the way, because we are in constructive logic, it may be not possible to prove that Pair is commutative, i.e. can't construct (set-pair m n) == (set-pair n m). It seems to me the most you can hope for, is the double negation of that.
no subject
Date: 2019-11-07 01:14 am (UTC)Interesting about the union. Categorically, they have to be isomorphic.
no subject
Date: 2019-11-07 07:00 am (UTC)But without the additional burden of having the proof the third set is not A and not B, there is not enough information. (For example, extensionality axiom requires the two Pair sets have the same members, and the members are not specified explicitly)
Say, if set equality were decidable, then we could prove Pair(m, n) == Pair(n, m).
Something like:
-- axiom that set equality is decidable postulate sets-equal? : {A : Set} (m n : S {A}) -> m ==? n pairs-eq' : {A : Set} -> (m n x : S {A}) -> (ismember (set-pair m n) x) == (ismember (set-pair n m) x) pairs-eq' m n x with sets-equal? m x | sets-equal? n x ... | yes m=x | _ = trans (transport {B = \x -> ismember (set-pair m n) x == true} m=x (pair-member-l m n)) (sym (transport {B = \x -> ismember (set-pair n m) x == true} m=x (pair-member-r n m))) ... | _ | yes n=x = trans (transport {B = \x -> ismember (set-pair m n) x == true} n=x (pair-member-r m n)) (sym (transport {B = \x -> ismember (set-pair n m) x == true} n=x (pair-member-l n m))) ... | no nxm | no nxn = trans (not-true \p -> pair-is p nxm nxn) (sym (not-true \p -> pair-is p nxn nxm)) pairs-eq : {A : Set} -> (m n : S {A}) -> (set-pair m n) == (set-pair n m) pairs-eq m n = ext (set-pair m n) (set-pair n m) (pairs-eq' m n)It may look verbose, but it's superficial. Just have to carry around all the premises that are needed to construct a proof. Other than that, it reads like a book:
We are given sets m and n that are used to form Pair(m,n) and Pair(n,m), and an arbitrary set x.
Suppose we can decide whether sets m and x are equal (means: introducing a new postulate that we can either find a proof that m == x, or find a proof that m != x).
Suppose m and x are equal, which means we are given a proof m == x. Then we can use this proof to construct an instance of type "(ismember (set-pair m n) x) == (ismember (set-pair n m) x)" - prove that the membership test is equal for both Pair(m, n) and Pair(n, m) in this case. This is achieved through transitivity of equality, if we can show "(ismember (set-pair m n) x) == true" and "true == (ismember (set-pair n m) x)".
Now, we construct a value of type "(ismember (set-pair m n) x) == true" from value of type "(ismember (set-pair m n) m) == true" by transporting it along the equality m == x that we have by supposing that m and x are equal, and "(ismember (set-pair m n) m) == true" is the part of Pairing axiom that talks of the sets used to construct a pair definitely being members of that set (pair-member-l m n provides proof that m∈Pair(m, n)).
Similarly we construct "(ismember (set-pair n m) x) == true", from which we obtain "true == (ismember (set-pair n m) x)" by symmetry of equality.
This all is explaining just the first case of pairs-eq' pattern matching! You see, if everything were to be spelled out, it is quite verbose, I've even skipped some steps by saying "similarly". In fact, Agda made it much more terse. :-)
...Similar trick can be done for the case when we have decided that n == x. Then finally we deal with the only case remaining - in this case we suppose that both m != x and n != x. This, again, obtains the proof "(ismember (set-pair m n) x) == (ismember (set-pair n m) x)" using transitivity of equality, just this time it is "(ismember (set-pair m n) x) == false" and "false == (ismember (set-pair n m) x)". We obtain these from the part of Pairing axiom that says that if x is a member of Pair(m,n), then "m == x or n == x", which in our world is "not (m != x and n != x)". Since we have proofs of m != x and n != x in this case, we can obtain the proof of "(ismember (set-pair m n) x) != true" through currying the part of Pairing axiom that talks about "m == x or n == x" (in our world it is pair-is), and from this proof obtain "(ismember (set-pair m n) x) == false".
Since we dealt with all possible cases of sets-equal?, we know pairs-eq' produces "(ismember (set-pair m n) x) == (ismember (set-pair n m) x)" for all m, n and x.
Now proving the equality of sets constructed by swapping the arguments of Pair around, is just application of Extensionality axiom. It needs a function that for all x of the needed type can show that both sets have the same membership. And (pair-eq' m n) is just such a function.
no subject
Date: 2019-11-07 03:38 pm (UTC)no subject
Date: 2019-11-07 05:03 pm (UTC)So to establish this fact, that there are no more sets in Pair set than m and n, does Pairing axiom imply or require that set equality is decidable?
Or does it then not only prove that for a set x such that x∈Pair(m,n) "m == x or n == x", but also provide the choice which one? That is, produces either "m == x" or "n == x"? In that case set equality does not need to be decidable, and the proof of Pair(m,n) == Pair(n,m) is different.
no subject
Date: 2019-11-07 05:15 pm (UTC)no subject
Date: 2019-11-07 08:56 pm (UTC)How do you propose to use the Separation Axiom? Does it rely on a predicate that needs set equality to be decidable?
(Eg something like construct a subset of Pair(m,n) of sets that are not equal to m and not equal to n - requires the ability to decide which sets are equal to m or n. But if equality of sets is decidable, then Pairing axiom is enough.)
no subject
Date: 2019-11-07 10:41 pm (UTC)no subject
Date: 2019-11-07 10:54 pm (UTC)no subject
Date: 2019-11-07 10:57 pm (UTC)no subject
Date: 2019-11-07 11:16 pm (UTC)But then the formulation of Pairing axiom "∀A∀B∃C∀D(D∈C⇔D==A∨D==B)" alone is enough.
no subject
Date: 2019-11-08 02:05 am (UTC)