forked from uds-psl/coq-library-undecidability
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathZF.v
More file actions
122 lines (74 loc) · 4.19 KB
/
Copy pathZF.v
File metadata and controls
122 lines (74 loc) · 4.19 KB
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
(* * ZF set theory with Skolem function symbols *)
(* ** Axiomatisations *)
Require Export Undecidability.FOL.Utils.FullSyntax.
From Undecidability.FOL.Sets Require Export ZF minZF binZF Signatures.
Import Vector.VectorNotations.
Require Import List.
Declare Scope syn.
Open Scope syn.
(* ** Signature for ZF axiomatisation, containing function symbols for set operations *)
Import ZFSignature.
Export ZFSignature.
(* ** 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 hereditarily finite sets. *)
Definition entailment_HF phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi HF -> sigma ⊨ psi) -> rho ⊨ phi.
Definition entailment_HFN phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, In psi HFN -> 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 for Z restricted to extensional models. *)
Definition entailment_Z phi :=
forall D (M : interp D) (rho : nat -> D), extensional M -> (forall sigma psi, Z psi -> sigma ⊨ psi) -> rho ⊨ phi.
(* Semantic entailment for ZF 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 hereditarily finite sets. *)
Definition deduction_HF phi :=
HFeq ⊢I phi.
Definition deduction_HFN phi :=
HFNeq ⊢I phi.
(* Deductive entailment restricted to intuitionistic rules and core axioms (without sep and rep). *)
Definition deduction_ZF' phi :=
ZFeq' ⊢I phi.
(* Deductive entailment for Z restricted to intuitionistic rules. *)
Definition deduction_Z phi :=
Zeq ⊢TI phi.
(* Deductive entailment for ZF restricted to intuitionistic rules. *)
Definition deduction_ZF phi :=
ZFeq ⊢TI phi.
(* ** MinZF *)
(* 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 for Z restricted to extensional models. *)
Definition entailment_minZ phi :=
forall D (M : @interp sig_empty _ D) (rho : nat -> D), extensional M -> (forall sigma psi, minZ psi -> sigma ⊨ psi) -> rho ⊨ phi.
(* Semantic entailment for ZF 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 for Z restricted to intuitionistic rules. *)
Definition deduction_minZ phi :=
minZeq ⊢TI phi.
(* Deductive entailment for ZF restricted to intuitionistic rules. *)
Definition deduction_minZF phi :=
minZFeq ⊢TI phi.
(* ** BinZF *)
(* Semantic entailment restricted to extensional models and core axioms (without sep and rep). *)
Definition entailment_binZF phi :=
forall D (M : @interp sig_empty _ D) (rho : nat -> D), (forall psi, In psi binZF -> rho ⊨ psi) -> rho ⊨ phi.
(* Deductive entailment restricted to intuitionistic rules and core axioms (without sep and rep). *)
Definition deduction_binZF phi :=
binZF ⊢I phi.