latte-sets.powerset
Notions about the powerset construction.
In the predicate-as-set encoding of set-theoretic notions, the powerset construction (i.e. building a set of sets) is not immediate. The reason is that the set constructor `(set T)’ is not itself a type (but a kind). Hence we need to replicate some part of the type theory (e.g. the existential quantifier) to deal with powersets.
empty-powerset
(empty-powerset [T :type])(lambda [x (set T)] p/absurd)
Definition: The empty powerset.
empty-powerset-prop
(empty-powerset-prop [T :type])(forall [x (set T)] (not (set-elem x (empty-powerset T))))
Theorem:
fetch-powerset-type
(fetch-powerset-type def-env ctx s-type)full-powerset
(full-powerset [T :type])(lambda [x (set T)] p/truth)
Definition: The powerset containing all the subsets of type T.
full-powerset-prop
(full-powerset-prop [T :type])(forall [x (set T)] (set-elem x (full-powerset T)))
Theorem:
intersections
(intersections [X (powerset T)])(lambda [y T] (forall [x (set T)] (==> (set-elem x X) (elem y x))))
Definition: Generalize intersections. This is the set {y:T | ∀x∈X, y∈x}.
intersections-lower-bound
(intersections-lower-bound [X (powerset T)])(forall [x (set T)] (==> (set-elem x X) (subset (intersections X) x)))
Theorem: The generalized intersection is a lower bound wrt. the subset relation.
intersections-prop
(intersections-prop [P (==> T :type)] [X (powerset T)])(forall
[x (set T)]
(==>
(set-elem x X)
(forall [y T] (==> (elem y x) (P y)))
(forall [z T] (==> (elem z (intersections X)) (P z)))))
Theorem: Preservation of properties on intersections.
powerset
(powerset [T :type])(==> (set T) :type)
Definition: The powerset constructor.
The term (powerset T)' is the type
of sets whose elements are sets of typeT`.
powerset1
(powerset1 [T :type])(lambda [x (set T)] (not (s/set-equal x (s/emptyset T))))
Definition: The powerset of all the non-empty subsets of type T.
powerset1-prop
(powerset1-prop [x (set T)])(==> (not (s/set-equal x (s/emptyset T))) (set-elem x (powerset1 T)))
Theorem:
powerset1-prop-conv
(powerset1-prop-conv [x (set T)])(==> (set-elem x (powerset1 T)) (not (s/set-equal x (s/emptyset T))))
Theorem:
powerset1-prop-equiv
(powerset1-prop-equiv [x (set T)])(<=> (set-elem x (powerset1 T)) (not (s/set-equal x (s/emptyset T))))
Theorem:
set-elem
(set-elem [x (set T)] [X (powerset T)])(X x)
Definition: Membership for powersets. Th set x is an element of the powerset X.
set-ex
(set-ex [X (powerset T)])(forall [α :type] (==> (forall [x (set T)] (==> (set-elem x X) α)) α))
Definition: The powerset existential. There exists a set s element of the powerset X such that… This is the definition of latte.quant/ex but adpated for sets.
set-ex-elim
(set-ex-elim [X (powerset T)] [A :type])(==> (set-ex X) (forall [x (set T)] (==> (set-elem x X) A)) A)
Theorem: The elimination rule for the set existential.
set-ex-intro
(set-ex-intro [X (powerset T)] [x (set T)])(==> (set-elem x X) (set-ex X))
Theorem: Introduction rule for set-ex.
set-single
(set-single [X (powerset T)])(forall [x y (set T)] (==> (set-elem x X) (set-elem y X) (seteq x y)))
Definition: The powerset version of latte-prelude.quant/single. There exists at most one set in X such that…
set-unique
(set-unique [X (powerset T)])(and (set-ex X) (set-single X))
Definition: The powerset version of latte-prelude.quant/unique. There exists a unique set in X such that …
the-set
(the-set [X (powerset T)] [u (set-unique X)])(set T)
Axiom: The unique set in powerset X such that … With u the uniqueness proof.
This is the powerset version of latte-prelude.quant/the.
the-set-lemma
(the-set-lemma [X (powerset T)] [u (set-unique X)])(forall [y (set T)] (==> (set-elem y X) (seteq y (the-set X u))))
Theorem: The unique set … is unique.
the-set-prop
(the-set-prop [X (powerset T)] [u (set-unique X)])(set-elem (the-set X u) X)
Axiom: The property of the unique set descriptor the-set.
unions
(unions [X (powerset T)])(lambda
[y T]
(set-ex (lambda [x (set T)] (and (set-elem x X) (elem y x)))))
Definition: Generalized union. This is the set {y:T | ∃x∈X, y∈x}.
unions-upper-bound
(unions-upper-bound [X (powerset T)])(forall [x (set T)] (==> (set-elem x X) (subset x (unions X))))
Theorem: The generalized union is an upper bound wrt. the subset relation.