Library HistoricalExamples.Tarski

Section AND.

Variable p q : Prop.

Definition AND := forall r : Prop, (p -> q -> r) -> r.

Variable h1 : p.
Variable h2 : q.

Theorem and : AND.
Proof fun (r : Prop) (h : p -> q -> r) => h h1 h2.

End AND.

Notation "A /\ B" := (AND A B) : type_scope.

Section Tarski.

Variable A : Type.
Variable R : A -> A -> Prop.
Variable Rtrans : forall x y z : A, R x y -> R y z -> R x z.
Variable F : (A -> Prop) -> A.
Variable Upperb : forall (P : A -> Prop) (x : A), P x -> R x (F P).
Variable
Least :
forall (P : A -> Prop) (x : A),
(forall y : A, P y -> R y x) -> R (F P) x.
Variable f : A -> A.
Variable Incr : forall x y : A, R x y -> R (f x) (f y).

Definition P0 (x : A) := R x (f x).
Definition x0 := F P0.

Section lemme1.

Variable x : A.
Variable h1 : R x (f x).
Theorem lemme1 : R x (f x0).
Proof Rtrans x (f x) (f x0) h1 (Incr x x0 (Upperb P0 x h1)).

End lemme1.

Lemma fact1 : R x0 (f x0).
Proof Least P0 (f x0) lemme1.

Lemma fact2 : R (f x0) x0.
Proof Upperb P0 (f x0) (Incr x0 (f x0) fact1).

Theorem Tarski : R x0 (f x0) /\ R (f x0) x0.
Proof and (R x0 (f x0)) (R (f x0) x0) fact1 fact2.

End Tarski.

Section Knaster.

Variable U : Type.

Definition set := U -> Prop.
Definition Subset (x y : set) := forall u : U, x u -> y u.
Definition Equal (x y : set) := Subset x y /\ Subset y x.
Definition Class := set -> Prop.
Definition Map := set -> set.
Variable Phi : Map.
Variable Incr : forall x y : set, Subset x y -> Subset (Phi x) (Phi y).

Definition Over (C : Class) (x : set) := forall y : set, C y -> Subset y x.
Definition Union (C : Class) (u : U) := forall x : set, Over C x -> x u.

Definition Subset_trans (x y z : set) (h1 : Subset x y)
(h2 : Subset y z) (u : U) (h3 : x u) := h2 u (h1 u h3).
Definition Union_upperb (C : Class) (x : set) (h1 : C x)
(u : U) (h2 : x u) (y : set) (h3 : Over C y) :=
h3 x h1 u h2.
Definition Union_least (C : Class) (x : set)
(h1 : forall y : set, C y -> Subset y x) (u : U)
(h2 : Union C u) := h2 x h1.

Definition Stable (x : set) := Subset x (Phi x).
Definition S := Union Stable.

Lemma Knaster : Equal S (Phi S).
Proof Tarski set Subset Subset_trans Union Union_upperb Union_least Phi Incr.

End Knaster.