-
Notifications
You must be signed in to change notification settings - Fork 0
/
ZF.v
166 lines (108 loc) · 4.54 KB
/
ZF.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
(* * Definition of semantic and deductive ZF-Entailment *)
Require Import Undecidability.FOL.Util.Syntax.
Require Import Undecidability.FOL.Util.FullTarski.
Require Import Undecidability.FOL.Util.FullDeduction.
Import Vector.VectorNotations.
Require Import List.
(* ** Signature for ZF axiomatisation, containing function symbols for set operations *)
Existing Instance falsity_on.
Inductive ZF_Funcs : Type :=
| eset : ZF_Funcs
| pair : ZF_Funcs
| union : ZF_Funcs
| power : ZF_Funcs
| om : ZF_Funcs.
Definition ZF_fun_ar (f : ZF_Funcs) : nat :=
match f with
| eset => 0
| pair => 2
| union => 1
| power => 1
| om => 0
end.
Inductive ZF_Preds : Type :=
| elem : ZF_Preds
| equal : ZF_Preds.
Definition ZF_pred_ar (P : ZF_Preds) : nat :=
match P with _ => 2 end.
Instance ZF_func_sig : funcs_signature :=
{| syms := ZF_Funcs; ar_syms := ZF_fun_ar; |}.
Instance ZF_pred_sig : preds_signature :=
{| preds := ZF_Preds; ar_preds := ZF_pred_ar; |}.
(* ** Axioms *)
Notation "x ∈ y" := (atom _ ZF_pred_sig elem ([x; y])) (at level 35) : syn.
Notation "x ≡ y" := (atom (Σ_preds := ZF_pred_sig) equal ([x; y])) (at level 35) : syn.
Notation "∅" := (func ZF_func_sig eset ([])) : syn.
Notation "'ω'" := (func ZF_func_sig om ([])) : syn.
Notation "{ x ; y }" := (func ZF_func_sig pair ([x; y])) (at level 31) : syn.
Notation "⋃ x" := (func ZF_func_sig union ([x])) (at level 32) : syn.
Notation "'PP' x" := (func ZF_func_sig power ([x])) (at level 31) : syn.
Notation "x ∪ y" := (⋃ {x; y}) (at level 32) : syn.
Notation "'σ' x" := (x ∪ {x; x}) (at level 32) : syn.
Definition sub x y :=
∀ $0 ∈ x`[↑] ~> $0 ∈ y`[↑].
Notation "x ⊆ y" := (sub x y) (at level 34) : syn.
Definition ax_ext :=
∀ ∀ $1 ⊆ $0 ~> $0 ⊆ $1 ~> $1 ≡ $0.
Definition ax_eset :=
∀ ¬ ($0 ∈ ∅).
Definition ax_pair :=
∀ ∀ ∀ $0 ∈ {$1; $2} <~> $0 ≡ $1 ∨ $0 ≡ $2.
Definition ax_union :=
∀ ∀ $0 ∈ ⋃ $1 <~> ∃ $0 ∈ $2 ∧ $1 ∈ $0.
Definition ax_power :=
∀ ∀ $0 ∈ PP $1 <~> $0 ⊆ $1.
Definition inductive x :=
∅ ∈ x ∧ ∀ $0 ∈ x`[↑] ~> σ $0 ∈ x`[↑].
Definition ax_om1 :=
inductive ω.
Definition ax_om2 :=
∀ inductive $0 ~> ω ⊆ $0.
Definition ax_sep phi :=
∀ ∃ ∀ $0 ∈ $1 <~> $0 ∈ $2 ∧ phi[$0.: Nat.add 3 >> var].
Definition fun_rel phi :=
∀ ∀ ∀ phi[$2 .: $1 .: Nat.add 3 >> var] ~> phi[$2 .: $0 .: Nat.add 3 >> var] ~> $1 ≡ $0.
Definition ax_rep phi :=
fun_rel phi ~> ∀ ∃ ∀ $0 ∈ $1 <~> ∃ $0 ∈ $3 ∧ phi[$0 .: $1 .: Nat.add 4 >> var].
(* List of core axioms without schemes for separation and replacement *)
Definition ZF' :=
ax_ext :: ax_eset :: ax_pair :: ax_union :: ax_power :: ax_om1 :: ax_om2 :: nil.
(* Theory of full ZF including the separation and replacement schemes *)
Inductive ZF : form -> Prop :=
| ZF_base phi : In phi ZF' -> ZF phi
| ZF_sep phi : ZF (ax_sep phi)
| ZF_rep phi : ZF (ax_rep phi).
Definition ax_refl :=
∀ $0 ≡ $0.
Definition ax_sym :=
∀ ∀ $1 ≡ $0 ~> $0 ≡ $1.
Definition ax_trans :=
∀ ∀ ∀ $2 ≡ $1 ~> $1 ≡ $0 ~> $2 ≡ $0.
Definition ax_eq_elem :=
∀ ∀ ∀ ∀ $3 ≡ $1 ~> $2 ≡ $0 ~> $3 ∈ $2 ~> $1 ∈ $0.
(* List of core axioms plus equality axioms *)
Definition ZFeq' :=
ax_refl :: ax_sym :: ax_trans :: ax_eq_elem :: ZF'.
(* Theory of full ZF plus equality axioms *)
Inductive ZFeq : form -> Prop :=
| ZFeq_base phi : In phi ZFeq' -> ZFeq phi
| ZFeq_sep phi : ZFeq (ax_sep phi)
| ZFeq_rep phi : ZFeq (ax_rep phi).
(* ** Problems *)
Notation extensional M :=
(forall x y, @i_atom _ ZF_pred_sig _ M equal ([x; y]) <-> x = y).
(* Semantic entailment restricted to core axioms (without sep and rep) with equality axioms. *)
Definition entailment_ZFeq' phi :=
forall D (M : interp D) (rho : nat -> D), (forall sigma psi, In psi ZFeq' -> sigma ⊨ psi) -> rho ⊨ phi.
(* Semantic entailment restricted to extensional models and core axioms (without sep and rep). *)
Definition entailment_ZF' phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi ZF' -> sigma ⊨ psi) -> rho ⊨ phi.
(* Semantic entailment restricted to extensional models. *)
Definition entailment_ZF phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, ZF psi -> sigma ⊨ psi) -> rho ⊨ phi.
(* Deductive entailment restricted to intuitionistic rules and core axioms (without sep and rep). *)
Definition deduction_ZF' phi :=
ZFeq' ⊢I phi.
(* Deductive entailment restricted to intuitionistic rules. *)
Definition deduction_ZF phi :=
ZFeq ⊢TI phi.