Library ZFdef
This module defines interfaces implementing various flavour
of set theory, from Zermelo to IZF_R and IZF_C (ZF)
Reserved Notation "x ∈ y" (at level 60).
Reserved Notation "x == y" (at level 70).
Reserved Notation "x ⊆ y" (at level 70).
Reserved Notation "x == y" (at level 70).
Reserved Notation "x ⊆ y" (at level 70).
Module Type SetTheory.
Parameter
(set : Type)
(eq_set : set -> set -> Prop)
(in_set : set -> set -> Prop).
Notation "x ∈ y" := (in_set x y).
Notation "x == y" := (eq_set x y).
Parameter
(eq_set_ax : ∀ a b, a == b <-> (∀ x, x ∈ a <-> x ∈ b))
(in_reg : ∀ a a' b, a == a' -> a ∈ b -> a' ∈ b).
End SetTheory.
...and with well-foundation axiom.
Plays the role of regularity axiom, but in an intutionistic
setting (regularity is classical).
Module Type WfSetTheory (L:SublogicTheory).
Include SetTheory.
Parameter
(wf_ax: ∀ P:set->Prop,
(∀ x, L.isL (P x)) ->
(∀ x, (∀ y, y ∈ x -> P y) -> P x) ->
∀ x, P x).
End WfSetTheory.
Include SetTheory.
Parameter
(wf_ax: ∀ P:set->Prop,
(∀ x, L.isL (P x)) ->
(∀ x, (∀ y, y ∈ x -> P y) -> P x) ->
∀ x, P x).
End WfSetTheory.
Module Type Zermelo_sig (L:SublogicTheory).
Include WfSetTheory L.
Import L.
Parameter
(empty : set)
(pair : set -> set -> set)
(union : set -> set)
(subset : set -> (set -> Prop) -> set)
(infinite : set)
(power : set -> set).
Parameter
(empty_ax: ∀ x, x ∈ empty -> #False)
(pair_ax: ∀ a b x, x ∈ pair a b <-> #(x == a \/ x == b))
(union_ax: ∀ a x, x ∈ union a <-> #exists2 y, x ∈ y & y ∈ a)
(subset_ax : ∀ a P x,
x ∈ subset a P <-> (x ∈ a /\ #exists2 x', x==x' & P x'))
(infinity_ax1: empty ∈ infinite)
(infinity_ax2: ∀ x,
x ∈ infinite -> union (pair x (pair x x)) ∈ infinite)
(power_ax: ∀ a x, x ∈ power a <-> (∀ y, y ∈ x -> y ∈ a)).
End Zermelo_sig.
Module Type Zermelo_Ex_sig (L:SublogicTheory).
Include WfSetTheory L.
Import L.
Parameter
(empty_ex: L.Tr(exists empty, ∀ x, x ∈ empty -> #False))
(pair_ex: ∀ a b, #exists c, ∀ x, x ∈ c <-> #(x == a \/ x == b))
(union_ex: ∀ a, #exists b,
∀ x, x ∈ b <-> #exists2 y, x ∈ y & y ∈ a)
(subset_ex : ∀ a P, #exists b,
∀ x, x ∈ b <-> (x ∈ a /\ exists2 x', x==x' & P x'))
(infinity_ex: #exists2 infinite,
#exists2 empty, (∀ x, x ∈ empty -> L.Tr False) &
empty ∈ infinite &
(∀ x, x ∈ infinite ->
#exists2 y, (∀ z, z ∈ y <-> (z == x \/ z ∈ x)) &
y ∈ infinite))
(power_ex: ∀ a, #exists b,
∀ x, x ∈ b <-> (∀ y, y ∈ x -> y ∈ a)).
End Zermelo_Ex_sig.
Include WfSetTheory L.
Import L.
Parameter
(empty_ex: L.Tr(exists empty, ∀ x, x ∈ empty -> #False))
(pair_ex: ∀ a b, #exists c, ∀ x, x ∈ c <-> #(x == a \/ x == b))
(union_ex: ∀ a, #exists b,
∀ x, x ∈ b <-> #exists2 y, x ∈ y & y ∈ a)
(subset_ex : ∀ a P, #exists b,
∀ x, x ∈ b <-> (x ∈ a /\ exists2 x', x==x' & P x'))
(infinity_ex: #exists2 infinite,
#exists2 empty, (∀ x, x ∈ empty -> L.Tr False) &
empty ∈ infinite &
(∀ x, x ∈ infinite ->
#exists2 y, (∀ z, z ∈ y <-> (z == x \/ z ∈ x)) &
y ∈ infinite))
(power_ex: ∀ a, #exists b,
∀ x, x ∈ b <-> (∀ y, y ∈ x -> y ∈ a)).
End Zermelo_Ex_sig.
IZF_R, Myhill's version of IZF:
- regularity is stated as a well-foundation axiom
- we use replacement, not collection
Module Type IZF_R_sig (L:SublogicTheory).
Include Zermelo_sig L.
Import L.
Parameter
(repl : set -> (set -> set -> Prop) -> set).
Parameter
(repl_mono: ∀ a a',
(∀ z, z ∈ a -> z ∈ a') ->
∀ (R R':set->set->Prop),
(∀ x x', x==x' -> ∀ y y', y==y' -> (R x y <-> R' x' y')) ->
∀ z, z ∈ repl a R -> z ∈ repl a' R')
(repl_ax: ∀ a (R:set->set->Prop),
(∀ x x' y y', x ∈ a -> x == x' -> y == y' -> R x y -> R x' y') ->
(∀ x y y', x ∈ a -> R x y -> R x y' -> y == y') ->
∀ x, x ∈ repl a R <-> #exists2 y, y ∈ a & R y x).
End IZF_R_sig.
Existential versions (Zermelo still skolemized)
Module Type IZF_R_HalfEx_sig (L:SublogicTheory).
Include Zermelo_sig L.
Import L.
Parameter
(repl_ex : ∀ a (R:set->set->Prop),
(∀ x x' y y', x ∈ a -> x == x' -> y == y' -> R x y -> R x' y') ->
(∀ x y y', x ∈ a -> R x y -> R x y' -> y == y') ->
#exists b, ∀ x, x ∈ b <-> #exists2 y, y ∈ a & R y x).
End IZF_R_HalfEx_sig.
Fully existential version
Module Type IZF_R_Ex_sig (L:SublogicTheory).
Include Zermelo_Ex_sig L.
Import L.
Parameter
(repl_ex : ∀ a (R:set->set->Prop),
(∀ x x' y y', x ∈ a -> x == x' -> y == y' -> R x y -> R x' y') ->
(∀ x y y', x ∈ a -> R x y -> R x y' -> y == y') ->
#exists b, ∀ x, x ∈ b <-> #exists2 y, y ∈ a & R y x).
End IZF_R_Ex_sig.
Module Type IZF_C_sig (L:SublogicTheory).
Include Zermelo_sig L.
Import L.
Parameter
(coll_ex : ∀ A (R:set->set->Prop),
Proper (eq_set ==> eq_set ==> iff) R ->
#exists B, ∀ x, x ∈ A ->
(#exists y, R x y) -> #exists2 y, y ∈ B & R x y).
End IZF_C_sig.
With skolemized collection