-
Notifications
You must be signed in to change notification settings - Fork 0
/
PA.v
135 lines (88 loc) · 3.86 KB
/
PA.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
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 PA axiomatisation, containing function symbols for set operations *)
Existing Instance falsity_on.
Inductive PA_funcs : Type :=
Zero : PA_funcs
| Succ : PA_funcs
| Plus : PA_funcs
| Mult : PA_funcs.
Definition PA_funcs_ar (f : PA_funcs ) :=
match f with
| Zero => 0
| Succ => 1
| Plus => 2
| Mult => 2
end.
Inductive PA_preds : Type :=
Eq : PA_preds.
Definition PA_preds_ar (P : PA_preds) :=
match P with
| Eq => 2
end.
Instance PA_funcs_signature : funcs_signature :=
{| syms := PA_funcs ; ar_syms := PA_funcs_ar |}.
Instance PA_preds_signature : preds_signature :=
{| preds := PA_preds ; ar_preds := PA_preds_ar |}.
Declare Scope PA_Notation.
Open Scope PA_Notation.
Notation "'zero'" := (@func PA_funcs_signature Zero ([])) (at level 1) : PA_Notation.
Notation "'σ' x" := (@func PA_funcs_signature Succ ([x])) (at level 37) : PA_Notation.
Notation "x '⊕' y" := (@func PA_funcs_signature Plus ([x ; y]) ) (at level 39) : PA_Notation.
Notation "x '⊗' y" := (@func PA_funcs_signature Mult ([x ; y]) ) (at level 38) : PA_Notation.
Notation "x '==' y" := (@atom PA_funcs_signature PA_preds_signature _ _ Eq ([x ; y])) (at level 40) : PA_Notation.
Notation "x '⧀' y" := (∃ (x[↑] ⊕ σ $0) == y) (at level 42) : PA_Notation.
(* ** Axioms of PA *)
Definition ax_zero_succ := ∀ (zero == σ var 0 ~> falsity).
Definition ax_succ_inj := ∀∀ (σ $1 == σ $0 ~> $1 == $0).
Definition ax_add_zero := ∀ (zero ⊕ $0 == $0).
Definition ax_add_rec := ∀∀ ((σ $0) ⊕ $1 == σ ($0 ⊕ $1)).
Definition ax_mult_zero := ∀ (zero ⊗ $0 == zero).
Definition ax_mult_rec := ∀∀ (σ $1 ⊗ $0 == $0 ⊕ $1 ⊗ $0).
Definition ax_induction (phi : form) :=
phi[zero..] ~> (∀ phi ~> phi[σ $0 .: S >> var]) ~> ∀ phi.
(* Fragment only containing the defining equations for addition and multiplication. *)
Definition FA := ax_add_zero :: ax_add_rec :: ax_mult_zero :: ax_mult_rec :: nil.
(* Full axiomatisation of the theory of PA *)
Inductive PA : form -> Prop :=
PA_FA phi : In phi FA -> PA phi
| PA_discr : PA ax_zero_succ
| PA_inj : PA ax_succ_inj
| PA_induction phi : PA (ax_induction phi).
(* Equality axioms for the PA signature *)
Definition ax_refl := ∀ $0 == $0.
Definition ax_sym := ∀∀ $1 == $0 ~> $0 == $1.
Definition ax_trans := ∀∀∀ $2 == $1 ~> $1 == $0 ~> $2 == $0.
Definition ax_succ_congr := ∀∀ $0 == $1 ~> σ $0 == σ $1.
Definition ax_add_congr := ∀∀∀∀ $0 == $1 ~> $2 == $3 ~> $0 ⊕ $2 == $1 ⊕ $3.
Definition ax_mult_congr := ∀∀∀∀ $0 == $1 ~> $2 == $3 ~> $0 ⊗ $2 == $1 ⊗ $3.
Definition EQ :=
ax_refl :: ax_sym :: ax_trans :: ax_succ_congr :: ax_add_congr :: ax_mult_congr :: nil.
Definition FAeq :=
EQ ++ FA.
Inductive PAeq : form -> Prop :=
PAeq_FA phi : In phi FAeq -> PAeq phi
| PAeq_discr : PAeq ax_zero_succ
| PAeq_inj : PAeq ax_succ_inj
| PAeq_induction phi : PAeq (ax_induction phi).
(* ** Problems *)
Notation extensional M :=
(forall x y, @i_atom _ _ _ M Eq ([x ; y]) <-> x = y).
(* Semantic entailment restricted to extensional models and FA. *)
Definition ext_entailment_PA phi :=
forall D (I : interp D) rho, extensional I -> (forall psi rho, PA psi -> rho ⊨ psi) -> rho ⊨ phi.
(* Semantic entailment restricted to FA *)
Definition entailment_FA phi :=
valid_ctx FAeq phi.
(* Semantic entailment for PA *)
Definition entailment_PA phi :=
forall D (I : interp D) rho, (forall psi rho, PAeq psi -> rho ⊨ psi) -> rho ⊨ phi.
(* Deductive entailment restricted to intuitionistic rules and FA. *)
Definition deduction_FA phi :=
FAeq ⊢I phi.
(* Deductive entailment restricted to intuitionistic rules. *)
Definition deduction_PA phi :=
PAeq ⊢TI phi.