Paradoxe de Russell et fin des axiomes de ZF.

Defs.v

@@ -78,7 +78,6 @@ Definition zf_sign :=
   {| Finite.funsymbs := [];
      Finite.predsymbs := [("=",2);("∈",2)] |}.
 
-
 (** Sets of names *)
 
 Module Names.

Peano.v

@@ -193,12 +193,12 @@ Proof.
   + simpl. unfold IsAx. left. assumption.
 Qed.
 
-Lemma rec0_rule l G A_x :
+Lemma rec0_rule l Γ A_x :
   BClosed (∀ A_x) ->
-  In (induction_schema A_x) G ->
-  Pr l (G ⊢ bsubst 0 Zero A_x) ->
-  Pr l (G ⊢ ∀ (A_x -> bsubst 0 (Succ(#0)) A_x)) ->
-  Pr l (G ⊢ ∀ A_x).
+  In (induction_schema A_x) Γ ->
+  Pr l (Γ ⊢ bsubst 0 Zero A_x) ->
+  Pr l (Γ ⊢ ∀ (A_x -> bsubst 0 (Succ(#0)) A_x)) ->
+  Pr l (Γ ⊢ ∀ A_x).
 Proof.
   intros.
   eapply R_Imp_e.
@@ -211,7 +211,7 @@ Proof.
     apply H0.
   + simpl.
     apply R_And_i; cbn.
-    * set (v := fresh (fvars (G ⊢ ∀ bsubst 0 Zero A_x)%form)).
+    * set (v := fresh (fvars (Γ ⊢ ∀ bsubst 0 Zero A_x)%form)).
       apply R_All_i with (x:=v).
       apply fresh_ok.
       rewrite form_level_bsubst_id.
@@ -347,7 +347,7 @@ Proof.
     - trans (Succ (y + x)).
       * ahered.
         assert (Pr Intuiti ((∀ #0 + y = y + #0) :: Γ' ⊢ ∀ #0 + y = y + #0)). { apply R_Ax. apply in_eq. }
-                                                                                                           apply R_All_e with (t := x) in H; auto.
+        apply R_All_e with (t := x) in H; auto.
       * sym.
         inst_axiom ax10 [y; x].
 Qed.

ZF.v

@@ -8,12 +8,31 @@ Import ListNotations.
 Local Open Scope bool_scope.
 Local Open Scope eqb_scope.
 
-(** The Peano axioms *)
+(** On the necessity of a non trivial set theory : Russell's paradox. *)
+
+(*  The naive set theory consists of the non restricted comprehension axiom schema :
+    ∀ x1, ..., ∀ xn, ∃ E, ∀ y (y ∈ E <-> A),
+      forall formula A whose free variable are x1, ..., xn. *)
+
+Definition naive_sign :=
+  (* So as to make the proof easier, we assume there is a constant E in the signature of the theory.
+     This could be avoided by transforming the statement of the paradox into "∃∀ (#0 ∈ #1 <-> ~(#0 ∈ #0))". *)
+  {| Finite.funsymbs := [("E",0)];
+     Finite.predsymbs := [("∈",2)] |}.
+
+Open Scope formula_scope.
+
+(* It is easy to notice that ∀ (#0 ∈ A <-> ~(#0 ∈ #0)) is (almost) an instance of the comprehension axiom schema : it suffices to let A = . *)
+Lemma Russell : Pr Intuiti ([ ∀ (#0 ∈ E <-> ~(#0 ∈ #0)) ] ⊢ False).
+Proof.
+  
+
+(** The ZF axioms *)
 
 Definition ZFSign := Finite.to_infinite zf_sign.
 
 Notation "x = y" := (Pred "=" [x;y]) : formula_scope.
-Notation "x ∈ y" := (Pred "∈" [x;y]) : formula_scope.
+Notation "x ∈ y" := (Pred "∈" [x;y]) (at level 70) : formula_scope.
 
 Module ZFAx.
 Local Open Scope formula_scope.
@@ -24,48 +43,67 @@ Definition eq_trans := ∀∀∀ (#2 = #1 /\ #1 = #0 -> #2 = #0).
 Definition compat_left := ∀∀∀ (#0 = #1 /\ #0 ∈ #2 -> #1 ∈ #2).
 Definition compat_right := ∀∀∀ (#0 ∈ #1 /\ #1 = #2 -> #0 ∈ #2).
 
-Definition ext := ∀∀ (∀ (#2 ∈ #0 <-> #2 ∈ #1) -> #0 = #1).
-Definition pairing := ∀∀∃∀ (#3 ∈ #2 <-> #3 = #0 \/ #3 = #1).
-Definition union := ∀∃∀ (#2 ∈ #1 <-> ∃ (#3 ∈ #0 /\ #2 ∈ #3)).
-Definition powerset := ∀∃∀ (#2 ∈ #1 <-> ∀ (#3 ∈ #2 -> #3 ∈ #0)).
-Definition infinity := ∃ (∃ (#1 ∈ #0 /\ ∀ not #2 ∈ #1) /\ ∀ (#3 ∈ #0 -> (∃ (#4 ∈ #0 /\ (∀ (#5 ∈ #4 <-> #5 = #3 \/ #5 ∈ #3)))))).
+Definition ext := ∀∀ (∀ (#0 ∈ #2 <-> #0 ∈ #1) -> #2 = #1).
+Definition pairing := ∀∀∃∀ (#0 ∈ #1 <-> #0 = #3 \/ #0 = #2).
+Definition union := ∀∃∀ (#0 ∈ #1 <-> ∃ (#0 ∈ #3 /\ #1 ∈ #0)).
+Definition powerset := ∀∃∀ (#0 ∈ #1 <-> ∀ (#0 ∈ #1 -> #0 ∈ #3)).
+Definition infinity := ∃ (∃ (#0 ∈ #1 /\ ∀ ~(#0 ∈ #1)) /\ ∀ (#0 ∈ #1 -> (∃ (#0 ∈ #2 /\ (∀ (#0 ∈ #1 <-> #0 = #2 \/ #0 ∈ #2)))))).
 
 Definition axioms_list :=
- [ eq_refl; eq_symp; eq_trans; compat_left; compat_right; ext; pairing; union; powerset; infinity ].
+ [ eq_refl; eq_sym; eq_trans; compat_left; compat_right; ext; pairing; union; powerset; infinity ].
 
 (** Beware, [bsubst] is ok below for turning [#0] into [Succ #0], but
     only since it contains now a [lift] of substituted terms inside
-    quantifiers.
-    And the unconventional [∀] before [A[0]] is to get the right
-    bounded vars (Hack !). *)
+    quantifiers. *)
 
 Definition comprehension_schema A :=
   nForall
-    (Nat.pred (level A))
-    (
+    (Nat.pred (level A)-2)
+    (∀∃∀ (#0 ∈ #1 <-> #0 ∈ #2 /\ A)).
 
-Definition induction_schema A_x :=
-  let A_0 := bsubst 0 Zero A_x in
-  let A_Sx := bsubst 0 (Succ(#0)) A_x in
+Definition replacement_schema A :=
   nForall
-    (Nat.pred (level A_x))
-    (((∀ A_0) /\ (∀ (A_x -> A_Sx))) -> ∀ A_x).
+    (Nat.pred (level A)-2)
+    (∀(∀ (#0 ∈ #1 -> (∃ (A /\ ∀ ((bsubst 1 (#0) A) -> #0 = #1)))) -> ∃∀ (#0 ∈ #2 -> ∃ (#0 ∈ #3 /\ A)))).
 
 Local Close Scope formula_scope.
 
 Definition IsAx A :=
   List.In A axioms_list \/
-  exists B, A = induction_schema B /\
-            check PeanoSign B = true /\
-            FClosed B.
-
-Lemma WfAx A : IsAx A -> Wf PeanoSign A.
+  (exists B, A = comprehension_schema B /\
+            check ZFSign B = true /\
+            FClosed B).
+  \/
+  (exists B, A = replacement_schema B /\
+             check ZFSign B = true /\
+             FClosed B).
+
+Lemma WfAx A : IsAx A -> Wf ZFSign A.
 Proof.
- intros [ IN | (B & -> & HB & HB')].
+ intros [ IN | (B & -> & HB & HB') ].
  - apply Wf_iff.
    unfold axioms_list in IN.
    simpl in IN. intuition; subst; reflexivity.
- - repeat split; unfold induction_schema; cbn.
+ - repeat split; unfold comprehension_schema; cbn.
+   + rewrite nForall_check. cbn.
+     rewrite !check_bsubst, HB; auto.
+   + red. rewrite nForall_level. cbn.
+     assert (level (bsubst 0 Zero B) <= level B).
+     { apply level_bsubst'. auto. }
+     assert (level (bsubst 0 (Succ(BVar 0)) B) <= level B).
+     { apply level_bsubst'. auto. }
+     omega with *.
+   + apply nForall_fclosed. red. cbn.
+     assert (FClosed (bsubst 0 Zero B)).
+     { red. rewrite bsubst_fvars.
+       intro x. rewrite Names.union_spec. cbn. red in HB'. intuition. }
+     assert (FClosed (bsubst 0 (Succ(BVar 0)) B)).
+     { red. rewrite bsubst_fvars.
+       intro x. rewrite Names.union_spec. cbn - [Names.union].
+       rewrite Names.union_spec.
+       generalize (HB' x) (@Names.empty_spec x). intuition. }
+     unfold FClosed in *. intuition.
+- repeat split; unfold replacement_schema; cbn.
    + rewrite nForall_check. cbn.
      rewrite !check_bsubst, HB; auto.
    + red. rewrite nForall_level. cbn.