Skip to content

Instantly share code, notes, and snippets.

@srbmiy srbmiy/ssrzfc001.v
Created Dec 21, 2014

Embed
What would you like to do?
ZFCカッコ仮
Require Import ssreflect ssrbool.
Axiom SET : Type.
Axiom membership : SET -> SET -> Prop.
Notation "x ∈ y" := (membership x y) (at level 100) : type_scope.
Axiom Extensionality : forall (x y: SET), (forall (z : SET), ((z ∈ x) <-> (z ∈ y))) <-> (x = y).
Axiom emptyset : SET.
Axiom EmptySetAxiom : (forall (z: SET), ~(z ∈ emptyset)).
Axiom pair : SET -> SET -> SET.
Notation "{ x , y }" := (pair x y) (at level 50) : type_scope.
Axiom PairingAxiom : forall (x y : SET), forall (z : SET), (z ∈ { x , y }) <-> (x = z) \/ (y = z).
Notation "{{ x }}" := (pair x x) (at level 49) : type_scope.
Axiom union : SET -> SET.
Notation "∪ x" := (union x) (at level 40) : type_scope.
Axiom UnionAxiom : forall (x : SET), forall (z : SET), (z ∈ (∪ x)) <-> (exists (y : SET), (z ∈ x) /\ (z ∈ y)).
Notation "x ∪ y" := (union (pair x y)) (at level 39) : type_scope.
Definition subset_of (x y : SET) : Prop :=
forall (z : SET), (membership z x) -> (membership z y).
Notation "x ⊆ y" := (subset_of x y) (at level 101) : type_scope.
Axiom PowerSetAxiom : forall (x : SET), exists (y : SET), forall (z : SET), (z ⊆ x) -> (z ∈ y).
Axiom Comprehension : forall (phi : SET -> SET-> Prop), forall (param : SET), forall (x : SET), exists (y : SET), forall (z : SET), (z ∈ y) <-> (z ∈ x) /\ (phi z param).
Axiom ω : SET.
Definition inductive_set (x : SET) : Prop :=
(emptyset ∈ x) /\ forall (y : SET), (y ∈ x) -> ((y ∪ {{ y }}) ∈ x).
Axiom InfinityAxiom : (inductive_set ω) /\ (forall (x : SET), (inductive_set x) -> (ω ⊆ x)).
Lemma 補題_0と1は異なる : ~(emptyset = {{ emptyset }}).
Proof.
assert (emptyset ∈ {{emptyset}}) as H1.
apply PairingAxiom.
left; exact. (* assertion succeeded. *)
assert (~(emptyset ∈ emptyset)) as H0.
apply EmptySetAxiom. (* assertion succeeded. *)
rewrite <- Extensionality.
move => Habs.
destruct H0.
rewrite (Habs emptyset).
exact.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.