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.