-
Notifications
You must be signed in to change notification settings - Fork 0
/
minZF.v
155 lines (96 loc) · 4.45 KB
/
minZF.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
(* * Definition of semantic and deductive ZF-Entailment in minimal signature *)
Require Import Undecidability.FOL.Util.Syntax.
Require Import Undecidability.FOL.Util.FullTarski.
Require Import Undecidability.FOL.Util.FullDeduction.
Require Import Undecidability.FOL.ZF.
Import Vector.VectorNotations.
Require Import List.
(* ** Minimal signature only containing membership and equality, no function symbols *)
Instance sig_empty : funcs_signature :=
{| syms := False; ar_syms := False_rect nat |}.
Existing Instance ZF_func_sig.
Notation term' := (term sig_empty).
Notation form' := (form sig_empty _ _ falsity_on).
Notation "x ∈' y" := (atom sig_empty ZF_pred_sig elem ([x; y])) (at level 35) : syn.
Notation "x ≡' y" := (atom sig_empty ZF_pred_sig equal ([x; y])) (at level 35) : syn.
(* ** Characterisations of set operations *)
Fixpoint shift `{funcs_signature} `{preds_signature} n (t : term) :=
match n with
| O => t
| S n => subst_term ↑ (shift n t)
end.
Definition is_eset (t : term') :=
∀ ¬ ($0 ∈ t`[↑]).
Definition is_pair (x y t : term') :=
∀ $0 ∈ t`[↑] <~> $0 ≡ x`[↑] ∨ $0 ≡ y`[↑].
Definition is_union (x t : term') :=
∀ $0 ∈ t`[↑] <~> ∃ $0 ∈ shift 2 x ∧ $1 ∈ $0.
Definition sub' (x y : term') :=
∀ $0 ∈ x`[↑] ~> $0 ∈ y`[↑].
Definition is_power (x t : term') :=
∀ $0 ∈ t`[↑] <~> sub' $0 x`[↑].
Definition is_sigma (x t : term') :=
∀ $0 ∈ t`[↑] <~> $0 ∈ x`[↑] ∨ $0 ≡ x`[↑].
Definition is_inductive (t : term') :=
(∃ is_eset $0 ∧ $0 ∈ t`[↑]) ∧ ∀ $0 ∈ t`[↑] ~> (∃ is_sigma $1 $0 ∧ $0 ∈ shift 2 t).
Definition is_om (t : term') :=
is_inductive t ∧ ∀ is_inductive $0 ~> sub' t`[↑] $0.
(* ** Symbol-free axiomatisation *)
Definition ax_ext' :=
∀ ∀ sub' $1 $0 ~> sub' $0 $1 ~> $1 ≡' $0.
Definition ax_eset' :=
∃ is_eset $0.
Definition ax_pair' :=
∀ ∀ ∃ is_pair $2 $1 $0.
Definition ax_union' :=
∀ ∃ is_union $1 $0.
Definition ax_power' :=
∀ ∃ is_power $1 $0.
Definition ax_om' :=
∃ is_om $0.
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 without schemes for separation and replacement *)
Definition minZF' :=
ax_ext' :: ax_eset' :: ax_pair' :: ax_union' :: ax_power' :: ax_om' :: nil.
(* List of core axioms plus equality axioms *)
Definition minZFeq' :=
ax_refl' :: ax_sym' :: ax_trans' :: ax_eq_elem' :: minZF'.
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].
(* Theory of full ZF including the separation and replacement schemes *)
Inductive minZF : form' -> Prop :=
| minZF_base phi : In phi minZF' -> minZF phi
| minZF_sep phi : minZF (ax_sep' phi)
| minZF_rep phi : minZF (ax_rep' phi).
(* Theory of full ZF plus equality axioms *)
Inductive minZFeq : form' -> Prop :=
| minZFeq_base phi : In phi minZFeq' -> minZFeq phi
| minZFeq_sep phi : minZFeq (ax_sep' phi)
| minZFeq_rep phi : minZFeq (ax_rep' phi).
(* ** Problems *)
(* Semantic entailment restricted to core axioms (without sep and rep) with equality axioms. *)
Definition entailment_minZFeq' phi :=
forall D (M : interp D) (rho : nat -> D), (forall sigma psi, In psi minZFeq' -> sigma ⊨ psi) -> rho ⊨ phi.
(* Semantic entailment restricted to extensional models and core axioms (without sep and rep). *)
Definition entailment_minZF' phi :=
forall D (M : @interp sig_empty _ D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi minZF' -> sigma ⊨ psi) -> rho ⊨ phi.
(* Semantic entailment restricted to extensional models. *)
Definition entailment_minZF phi :=
forall D (M : @interp sig_empty _ D) (rho : nat -> D), extensional M -> (forall sigma psi, minZF psi -> sigma ⊨ psi) -> rho ⊨ phi.
(* Deductive entailment restricted to intuitionistic rules and core axioms (without sep and rep). *)
Definition deduction_minZF' phi :=
minZFeq' ⊢I phi.
(* Deductive entailment restricted to intuitionistic rules. *)
Definition deduction_minZF phi :=
minZFeq ⊢TI phi.