-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathfol_incompleteness.v
147 lines (114 loc) · 5.21 KB
/
fol_incompleteness.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
(** ** Essential Incompleteness of Q *)
From Undecidability.Shared Require Import Dec.
From Undecidability.Synthetic Require Import Definitions EnumerabilityFacts.
From FOL Require Import FullSyntax Arithmetics.
From FOL.Incompleteness Require Import Axiomatisations utils fol_utils qdec bin_qdec sigma1 epf epf_mu formal_systems abstract_incompleteness ctq.
From FOL.Proofmode Require Import Theories ProofMode.
Require Import Lia String List.
(* * Incompleteness of first-order logic *)
(* first-order logic with an enumerable theory is a formal system *)
Section fol_fs.
Existing Instance PA_funcs_signature.
Existing Instance PA_preds_signature.
Hypothesis (p : peirce).
Definition fol_fs (T : theory) (Tenum : enumerable T) (Tconsis : ~T ⊢T ⊥) : FS form (fun φ => ¬φ).
Proof.
apply mkFS with (fprv := fun φ => T ⊢T φ).
- apply enumerable_semi_decidable.
+ apply form_discrete.
+ unshelve eapply tprv_enumerable.
* apply enumerable_PA_funcs.
* apply enumerable_PA_preds.
* assumption.
- intros φ [T1 [HT1 H1]] [T2 [HT2 H2]]. apply Tconsis. exists (T1 ++ T2). split.
+ intros ψ [?|?]%in_app_or; auto.
+ eapply IE.
* eapply Weak; first apply H2.
apply incl_appr, incl_refl.
* eapply Weak; first apply H1.
apply incl_appl, incl_refl.
Defined.
End fol_fs.
Section fol.
Existing Instance PA_funcs_signature.
Existing Instance PA_preds_signature.
(* ** Q is essentially incomplete and essentially undecidable *)
(* Any theory that strongly separates two recursively inseparable predicates is incompelte *)
Section incomplete_strong_repr.
Hypothesis (p : peirce).
Variable theta : nat -> nat -\ bool.
Hypothesis theta_universal : is_universal theta.
Variable T : theory.
Hypothesis Tenum : enumerable T.
Hypothesis Tconsis : ~T ⊢T ⊥.
Variable T' : theory.
Hypothesis T'_T : T' ⊑ T.
Hypothesis T'enum : enumerable T'.
Variable r : nat -> form.
Hypothesis Hrepr :
(forall c, theta c c ▷ true -> T' ⊢T r c) /\
(forall c, theta c c ▷ false -> T' ⊢T ¬r c).
Lemma fol_undecidable_strong_repr : ~decidable (fun s => T ⊢T s).
Proof.
assert (~T' ⊢T ⊥) as T'consis.
{ contradict Tconsis. now eapply WeakT. }
eapply (insep_essential_undecidability) with (theta := theta) (fs := fol_fs Tenum Tconsis) (fs' := fol_fs T'enum T'consis).
- assumption.
- unfold extension. cbn. intros φ Hφ. now eapply WeakT.
- exact Hrepr.
Qed.
Lemma fol_incomplete_strong_repr : exists n, ~T ⊢T r n /\ ~T ⊢T ¬r n.
Proof.
assert (~T' ⊢T ⊥) as T'consis.
{ contradict Tconsis. now eapply WeakT. }
apply (insep_essential_incompleteness) with (theta := theta) (fs := fol_fs Tenum Tconsis) (fs' := fol_fs T'enum T'consis).
- assumption.
- unfold extension. cbn. intros φ Hφ. now eapply WeakT.
- assumption.
Qed.
End incomplete_strong_repr.
(* Q is essentially incomplete and essentially undecidable *)
Section Q_incomplete.
(* Hypothesis mu_universal : is_universal theta_mu. *)
Hypothesis (p : peirce).
Hypothesis ctq : @CTQ p.
Variable T : theory.
Hypothesis T_Q : list_theory Qeq ⊑ T.
Hypothesis Tenum : enumerable T.
Hypothesis Tconsis : ~@tprv _ _ _ p T ⊥.
Theorem Q_undecidable : ~decidable (@tprv _ _ _ p T).
Proof.
assert (exists theta : nat -> nat -\ bool, is_universal theta) as [theta theta_universal].
{ apply epf_nat_bool, ctq_epfn, ctq. }
assert (forall c, theta c c ▷ true -> theta c c ▷ false -> False) as Hdisj.
{ intros c Ht Hf. enough (true = false) by discriminate. eapply part_functional; eassumption. }
edestruct (ctq_strong_sepr ctq Hdisj) as (ψ & Hb & HΣ & Hψ1 & Hψ2).
1-2: apply theta_self_return_semi_decidable.
eapply (@fol_undecidable_strong_repr p theta theta_universal T Tenum Tconsis (list_theory Qeq) T_Q (list_theory_enumerable Qeq)).
instantiate (1 := fun c => ψ[(num c)..]).
split; intros c H.
- exists Qeq. eauto.
- exists Qeq. eauto.
Qed.
Theorem Q_incomplete : exists φ, bounded 0 φ /\ Σ1 φ /\ ~@tprv _ _ _ p T φ /\ ~@tprv _ _ _ p T (¬φ).
Proof.
assert (exists theta : nat -> nat -\ bool, is_universal theta) as [theta theta_universal].
{ apply epf_nat_bool, ctq_epfn, ctq. }
assert (forall c, theta c c ▷ true -> theta c c ▷ false -> False) as Hdisj.
{ intros c Ht Hf. enough (true = false) by discriminate. eapply part_functional; eassumption. }
edestruct (ctq_strong_sepr ctq Hdisj) as (ψ & Hb & HΣ & Hψ1 & Hψ2).
1-2: apply theta_self_return_semi_decidable.
edestruct (@fol_incomplete_strong_repr p theta theta_universal T Tenum Tconsis (list_theory Qeq) T_Q (list_theory_enumerable Qeq)).
{ instantiate (1 := fun c => ψ[(num c)..]).
split; intros c H.
- exists Qeq. eauto.
- exists Qeq. eauto. }
cbn in H. exists ψ[(num x)..].
repeat apply conj.
- eapply subst_bounded_max; last eassumption. intros [|n] Hn; last lia. apply num_bound.
- now apply Σ1_subst.
- apply H.
- apply H.
Qed.
End Q_incomplete.
End fol.