(s x)

Definition: Set membership.

(elem x s) means that x (of implicit type T) is an element of set s. The standard mathematical notation is: x∊s.

Replaces sterm by its element type (if it is a set type).

(set-of [x T] p/absurd)

Definition: The empty set of a type.

(forall [x T] (not (elem x (emptyset T))))

Theorem: The main property of the empty set.

The elimination rule for the exists-in existential quantifier over a set s (of elements of type T). A typical proof instance is of the form ((ex-elim s P A) ex-proof A-proof) with ex-term a proof of (exists-in [x s] (P x)) and A-proof a proof of (==> (forall-in [x s] (==> (P x) A))). See ex-in-elem-thm.

(==> (exists-in [x s] (P x)) (forall-in [y s] (==> (P y) A)) A)

Theorem: Elimination rule for exists-in existentials, a simple variant of latte-prelude.quant/ex-elim-thm.

Existential quantification over sets.

(exists-in [x s] (P x)) is a shortcut for (exists [x (element-type-of s)] (and (elem x s) (P x))).

Universal quantification over sets.

(forall-in [x s] (P x)) is a shortcut for (forall [x (element-type-of s)] (==> (elem x s) (P x))).

(set-of [x T] p/truth)

Definition: The full set of a type (all the inhabitants of the type are element of the full set).

(forall [x T] (elem x (fullset T)))

Theorem: Introduction rule for the full set.

(and (subset s1 s2) (not (seteq s1 s2)))

Definition: The anti-reflexive variant of the subset relation.

The expression (psubset T s1 s2) means that the set s1 is a subset of s2, but that the two sets are distinct, i.e. s1⊂s2 (or more explicitely s1⊊s2).

(not (psubset s s))

Theorem:

(not (and (psubset s1 s2) (psubset s2 s1)))

Theorem:

(==> (psubset (emptyset T) s) (not (seteq s (emptyset T))))

Theorem:

(==> (not (seteq s (emptyset T))) (psubset (emptyset T) s))

Theorem:

(<=> (psubset (emptyset T) s) (not (seteq s (emptyset T))))

Theorem:

(==> (psubset s1 s2) (psubset s2 s3) (psubset s1 s3))

Theorem: The proper subset relation is transitive.

(==> T :type)

Definition: The type of sets whose elements are of type T.

(forall [P (==> (set T) :type)] (<=> (P s1) (P s2)))

Definition: A Leibniz-style equality for sets.

It says that two sets s1 and s2 are equal iff for any predicate P then (P s1) if and only if (P s2).

Note that the identification with seteq is non-trivial, and requires an axiom.

(==> (set-equal s1 s2) (seteq s1 s2))

Theorem: Subset-based equality implies Leibniz-style equality on sets.

(==> (set-equal s1 s2) (subset s1 s2))

Theorem: Going from Leibniz equality on sets to the subset relation is easy.

(==> (set-equal s1 s2) (P s1) (P s2))

Theorem:

(set-equal s s)

Theorem: Reflexivity of set equality.

(<=> (seteq s1 s2) (set-equal s1 s2))

Theorem: Set equality and subset-based equality (should) coincide (axiomatically).

(==> (set-equal s1 s2) (set-equal s2 s1))

Theorem: Symmetry of set equality.

(==> (set-equal s1 s2) (set-equal s2 s3) (set-equal s1 s3))

Theorem: Transitivity of set equality.

Definition of a set by comprehension.

(set-of [x T] (P x)) is the set of all x’s of type T such that (P x). This is similar to the notation {x : T | P(x) } in classical mathematics.

Note that it is exactly the same as (lambda [x T] (P x))

(and (subset s1 s2) (subset s2 s1))

Definition: Set equivalence. Set s1 is equal to s2 This is a natural notion of “equal sets” based on the subset relation.

(==> (seteq s1 s2) (set-equal s1 s2))

Axiom: Going from subset-based equality to Leibniz-style equality requires this axiom. This is because we cannot lift membership to an arbitrary predicate.

(seteq s s)

Theorem: Set equality is reflexive.

(==> (seteq s1 s2) (seteq s2 s1))

Theorem: Set equality is symmetric.

(==> (seteq s1 s2) (seteq s2 s3) (seteq s1 s3))

Theorem: Set equality is transitive.

(forall [x T] (==> (elem x s1) (elem x s2)))

Definition: The subset relation for type T. The expression (subset-def T s1 s2) means that the set s1 is a subset of s2, i.e. s1⊆s2.

(==> (elem x s1) (subset s1 s2) (elem x s2))

Theorem: Elimination rule for subset relation.

(subset (emptyset T) s)

Theorem: The emptyset is a subset of every other sets.

(subset s (fullset T))

Theorem: The fullset is a superset of every other sets.

(==> (forall [x T] (==> (elem x s1) (elem x s2))) (subset s1 s2))

Theorem: Introduction rule for subset relation.

(==>
 (forall [x T] (==> (elem x s2) (P x)))
 (subset s1 s2)
 (forall [x T] (==> (elem x s1) (P x))))

Theorem: Preservation of properties on subsets.

(subset s s)

Theorem: The subset relation is reflexive.

(==> (subset s1 s2) (subset s2 s3) (subset s1 s3))

Theorem: The subset relation is transitive.