Created
December 21, 2014 15:30
-
-
Save srbmiy/270d8b24ec784b54fa48 to your computer and use it in GitHub Desktop.
ZFCカッコ仮
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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