Skip to content

Commit 42b9d06

Browse files
SnO2WMaNSnO2WMaN
committed
provability logic
1 parent bcf31c0 commit 42b9d06

12 files changed

Lines changed: 578 additions & 1 deletion

File tree

‎SeqPL/Arithmetic/Completeness.lean‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
module
2+
3+
public import SeqPL.Arithmetic.Soundness
4+
public import SeqPL.Arithmetic.SolovaySentences
5+
6+
@[expose] public section
7+
8+
open Classical
9+
open LO
10+
open LO.FirstOrder.ProvabilityAbstraction
11+
12+
variable {T : FirstOrder.ArithmeticTheory} [T.Δ₁] [𝗜𝚺₁ ⪯ T]
13+
14+
variable {κ : Type*} [Nonempty κ]
15+
{α : Type*}
16+
{A B : _root_.Formula α}
17+
{M : RootedModel κ α}
18+
19+
@[grind]
20+
def LO.FirstOrder.ArithmeticTheory.provabilityLogicRelativeTo (T U : FirstOrder.ArithmeticTheory) [T.Δ₁] : Logic α := {A | ∀ f : StandardRealization α T, U ⊢ f A}
21+
22+
abbrev LO.FirstOrder.ArithmeticTheory.provabilityLogic (T : FirstOrder.ArithmeticTheory) [T.Δ₁] : Logic α := T.provabilityLogicRelativeTo T
23+
24+
theorem unprovable_realization_exists
25+
(M : RootedModel κ α) [Fintype M.World] [M.IsGL]
26+
(hA : M.root.1 ⊮ A) (h : M.height < T.height)
27+
: ∃ f : StandardRealization α T, T ⊬ f A := by
28+
let S := LO.FirstOrder.Theory.standardProvability.solovaySentences (M := M.extendRoot 1) (T := T);
29+
use S.realization;
30+
contrapose! h;
31+
apply Order.le_of_lt_add_one;
32+
calc
33+
T.height < (M.extendRoot 1).height := S.theory_height (T.standardProvability.syntactical_sound ℕ) (A := A) ?_ h
34+
_ = _ := by
35+
have := RootedModel.extendRoot.Ext1.eq_height_original_height_succ (M := M);
36+
simp_all only [ne_eq, PNat.val_ofNat, Nat.cast_add, Nat.cast_one];
37+
. apply Model.World.forces_dia.mpr;
38+
use M.root;
39+
constructor;
40+
. tauto;
41+
. exact RootedModel.extendRoot.same_forces_embed.not.mpr hA;
42+
43+
namespace LogicGL
44+
45+
theorem arithmetical_completeness_of_infinity_height (height : T.height = (⊤ : ℕ∞)) :
46+
(∀ f : StandardRealization α T, T ⊢ f A) → A ∈ LogicGL _ := by
47+
contrapose!;
48+
intro hA;
49+
replace h := LogicGL_semantical_TFAE.out 0 2 |>.not.mp hA;
50+
push Not at h;
51+
obtain ⟨κ, _, M, _, hA⟩ := h;
52+
have : Fintype M.World := Fintype.ofFinite _;
53+
exact unprovable_realization_exists M hA (by simp_all);
54+
55+
theorem arithmetical_completeness_of_finite_le {n : ℕ} (height : n ≤ T.height)
56+
: (∀ f : StandardRealization α T, T ⊢ f A) → □^[n] ⊥ 🡒 A ∈ LogicGL _ := by
57+
contrapose!;
58+
intro hA;
59+
replace h := LogicGL_semantical_TFAE.out 0 2 |>.not.mp hA;
60+
push Not at h;
61+
obtain ⟨κ, _, M, _, hA⟩ := h;
62+
replace hA := Model.World.not_forces_imp.mp hA;
63+
have : Fintype M.World := Fintype.ofFinite _;
64+
apply unprovable_realization_exists M hA.2;
65+
apply lt_of_lt_of_le;
66+
. apply Nat.cast_lt.mpr $ RootedModel.iff_height_lt_root_forces_boxItr_bot |>.mpr hA.1;
67+
. exact height;
68+
69+
lemma arithmetical_completeness_iff_of_infinity_height (height : T.height = (⊤ : ℕ∞))
70+
: A ∈ LogicGL _ ↔ (∀ f : StandardRealization α T, T ⊢ f A) := by
71+
constructor;
72+
. intro h f;
73+
exact arithmetical_soundness (f := f) h;
74+
. exact arithmetical_completeness_of_infinity_height height;
75+
76+
lemma arithmetical_completeness_iff_of_sigma1_sound [T.SoundOnHierarchy 𝚺 1]
77+
: A ∈ LogicGL _ ↔ (∀ f : StandardRealization α T, T ⊢ f A) :=
78+
arithmetical_completeness_iff_of_infinity_height (FirstOrder.Arithmetic.height_eq_top_of_sigma1_sound T)
79+
80+
theorem eq_provabilityLogic_sigma1_sound [T.SoundOnHierarchy 𝚺 1] : LogicGL α = T.provabilityLogic := by
81+
ext A;
82+
exact LogicGL.arithmetical_completeness_iff_of_sigma1_sound;
83+
84+
theorem eq_provabilityLogic_peano_arithmetic : LogicGL α = (𝗣𝗔.provabilityLogic) := LogicGL.eq_provabilityLogic_sigma1_sound
85+
86+
end LogicGL
87+
88+
89+
namespace LogicGLPlusBoxBot
90+
91+
theorem arithmetical_completeness {n : ℕ∞} (hn : n ≤ T.height)
92+
(h : ∀ f : StandardRealization α T, T ⊢ f A) : A ∈ LogicGLPlusBoxBot n := by
93+
match n with
94+
| .none =>
95+
apply LogicGL.arithmetical_completeness_of_infinity_height (T := T) ?_ h;
96+
exact eq_top_iff.mpr hn;
97+
| .some n =>
98+
apply LogicGLPlusBoxBot.iff_provable_provable_GL.mpr;
99+
apply LogicGL.arithmetical_completeness_of_finite_le (T := T) ?_ h;
100+
exact hn;
101+
102+
theorem arithmetical_completeness_iff
103+
: A ∈ LogicGLPlusBoxBot T.height ↔ (∀ f : StandardRealization α T, T ⊢ f A) := by
104+
constructor;
105+
. intro h f; exact arithmetical_soundness h;
106+
. exact arithmetical_completeness (by simp);
107+
108+
lemma eq_provabilityLogic : LogicGLPlusBoxBot (α := α) T.height = T.provabilityLogic := by
109+
ext A;
110+
exact arithmetical_completeness_iff;
111+
112+
end LogicGLPlusBoxBot
113+
114+
115+
end

‎SeqPL/Arithmetic/Interpret.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,14 @@ def interpret (f : Realization α 𝔅) : Formula α → FirstOrder.Sentence L
2929

3030
instance : CoeFun (Realization α 𝔅) (fun _ ↦ Formula α → FirstOrder.Sentence L) := ⟨interpret⟩
3131

32+
variable {f : Realization α 𝔅} {A : Formula α}
33+
34+
@[simp, grind =]
35+
lemma interpret_boxItr {n : ℕ} : (□^[n]A).interpret f = 𝔅^[n] (f A) := by
36+
induction n with
37+
| zero => simp [Formula.boxItr];
38+
| succ n ih => simp only [boxItr, Function.iterate_succ_apply', interpret, ih];
39+
3240
end Formula
3341

3442

‎SeqPL/Arithmetic/SolovaySentences.lean‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
module
2+
3+
public import SeqPL.Kripke.Rank
4+
public import SeqPL.Arithmetic.Soundness
5+
public import Foundation.Vorspiel.List.ChainI
6+
7+
@[expose] public section
8+
9+
open Classical
10+
open LO
11+
open LO.FirstOrder.ProvabilityAbstraction
12+
13+
variable {L : FirstOrder.Language} [L.ReferenceableBy L]
14+
{T₀ T : FirstOrder.Theory L} [T₀ ⪯ T] {𝔅 : Provability T₀ T} [𝔅.HBL]
15+
16+
variable {κ : Type*} [Nonempty κ]
17+
{α : Type*}
18+
{A B : _root_.Formula α}
19+
{M : RootedModel κ α}
20+
21+
structure LO.FirstOrder.ProvabilityAbstraction.Provability.SolovaySentences
22+
(𝔅 : Provability T₀ T) (M : RootedModel κ α) [Fintype M.World] where
23+
σ : M.World → FirstOrder.Sentence L
24+
protected SC1 : ∀ i j, i ≠ j → T₀ ⊢ σ i 🡒 ∼σ j
25+
protected SC2 : ∀ i j, i ≺ j → T₀ ⊢ σ i 🡒 𝔅.dia (σ j)
26+
protected SC3 : ∀ i : M.World, M.root ≠ i → T₀ ⊢ σ i 🡒 𝔅 (⩖ j ∈ { j : M.World | i ≺ j }, σ j)
27+
protected SC4 : T₀ ⊢ ⩖ j, σ j
28+
29+
namespace LO.FirstOrder.ProvabilityAbstraction.Provability.SolovaySentences
30+
31+
attribute [coe] σ
32+
33+
variable {M : RootedModel κ α} [Fintype M.World] [M.IsGL] {i : M.World}
34+
{S : SolovaySentences 𝔅 M}
35+
36+
noncomputable def realization : Realization α 𝔅 := ⟨fun a ↦ ⩖ i ∈ { i : M.World | i ⊩ (.atom a) }, S.σ i⟩
37+
38+
private lemma mainlemma_aux (hri : M.root ≠ i)
39+
: (i ⊩ A → T₀ ⊢ S.σ i 🡒 S.realization A) ∧ (i ⊮ A → T₀ ⊢ S.σ i 🡒 ∼(S.realization A)) := by
40+
induction A generalizing i with
41+
| bot => simp [Formula.interpret];
42+
| atom a =>
43+
constructor;
44+
. intro h;
45+
sorry;
46+
. intro h;
47+
sorry;
48+
| imp A B ihA ihB =>
49+
sorry;
50+
| box A ihA =>
51+
sorry;
52+
53+
theorem mainlemma (hri : M.root ≠ i) : i ⊩ A → T₀ ⊢ S.σ i 🡒 A.interpret S.realization := (mainlemma_aux hri).1
54+
theorem mainlemma_neg (hri : M.root ≠ i) : i ⊮ A → T₀ ⊢ S.σ i 🡒 ∼(A.interpret S.realization) := (mainlemma_aux hri).2
55+
56+
lemma root_of_iterated_inconsistency : T₀ ⊢ (∼𝔅^[M.height] ⊥) 🡒 (S.σ M.root) := by sorry;
57+
58+
lemma theory_height (hSound : ∀ {σ}, T₀ ⊢ 𝔅 σ → T ⊢ σ) (h : M.root.1 ⊩ ◇(∼A)) (b : T ⊢ S.realization A) : 𝔅.height < M.height := by
59+
sorry;
60+
61+
end LO.FirstOrder.ProvabilityAbstraction.Provability.SolovaySentences
62+
63+
variable (T : FirstOrder.ArithmeticTheory) [T.Δ₁]
64+
65+
def LO.FirstOrder.Theory.standardProvability.solovaySentences (M : RootedModel κ α) [Fintype M.World] : T.standardProvability.SolovaySentences M := by sorry
66+
67+
end

‎SeqPL/Arithmetic/Soundness.lean‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
module
2+
3+
public import Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Height
4+
public import SeqPL.Logic.Basic
5+
public import SeqPL.Logic.SumQuasiNormal
6+
public import SeqPL.Arithmetic.Interpret
7+
8+
@[expose] public section
9+
10+
open Classical
11+
open LO
12+
open LO.FirstOrder.ProvabilityAbstraction
13+
14+
variable {L : FirstOrder.Language} [L.ReferenceableBy L]
15+
[L.DecidableEq]
16+
{T U : FirstOrder.Theory L} [Diagonalization T] [T ⪯ U]
17+
{𝔅 : Provability T U} [𝔅.HBL]
18+
variable {A : Formula α}
19+
{f : Realization α 𝔅}
20+
21+
def LogicGLPlusBoxBot {α} : ℕ∞ → Logic α
22+
| .some n => LogicGL α +ᴸ □^[n]⊥
23+
| .none => LogicGL α
24+
25+
lemma LogicGL.arithmetical_soundness (hA : A ∈ LogicGL _) : U ⊢ f A := by
26+
replace hA := LogicGL_TFAE.out 0 1 |>.mp hA;
27+
induction hA with
28+
| nec _ ihA => exact Entailment.WeakerThan.pbl $ 𝔅.D1 ihA;
29+
| mdp _ _ ihAB ihA => exact ihAB ⨀ ihA;
30+
| modalK => exact Entailment.WeakerThan.pbl $ 𝔅.D2;
31+
| modal4 => exact Entailment.WeakerThan.pbl $ 𝔅.D3;
32+
| modalL => exact Entailment.WeakerThan.pbl $ formalized_löb_theorem;
33+
| _ =>
34+
dsimp [Formula.interpret];
35+
cl_prover;
36+
37+
lemma LogicGLPlusBoxBot.iff_provable_provable_GL {n : ℕ} : A ∈ LogicGLPlusBoxBot n ↔ (□^[n]⊥ 🡒 A) ∈ LogicGL _ := by
38+
constructor;
39+
. intro h;
40+
induction h with
41+
| mem₁ hA =>
42+
sorry;
43+
| mem₂ hB =>
44+
sorry;
45+
| mdp _ _ ihAB ihA =>
46+
sorry;
47+
| subst _ ihA => sorry;
48+
. intro h;
49+
apply Logic.sumQuasiNormal.mdp;
50+
. exact Logic.sumQuasiNormal.mem₁ h;
51+
. exact Logic.sumQuasiNormal.mem₂ rfl;
52+
53+
lemma LogicGLPlusBoxBot.arithmetical_soundness (hA : A ∈ LogicGLPlusBoxBot 𝔅.height) {f : Realization α 𝔅} : U ⊢ f A := by
54+
cases h : 𝔅.height
55+
case _ =>
56+
simp [LogicGLPlusBoxBot, h] at hA;
57+
exact LogicGL.arithmetical_soundness $ hA;
58+
case _ n =>
59+
have : U ⊢ f (□^[n]⊥) 🡒 f A := LogicGL.arithmetical_soundness $ LogicGLPlusBoxBot.iff_provable_provable_GL.mp $ h ▸ hA;
60+
apply this ⨀ ?_;
61+
rw [Formula.interpret_boxItr];
62+
apply 𝔅.height_le_iff_boxBot.mp;
63+
simp_all;
64+
65+
end

‎SeqPL/Classification/Full.lean‎

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
module
2+
3+
public import SeqPL.Classification.Letterless
4+
5+
@[expose]
6+
public section
7+
8+
universe u
9+
variable {α : Type u}
10+
11+
12+
namespace Formula
13+
14+
end Formula
15+
16+
17+
namespace Formula
18+
19+
variable {n : ℕ} {A B : Formula α}
20+
21+
@[grind]
22+
def trace (A : Formula α) : Set ℕ := { n |
23+
∃ κ : Type u, ∃ _ : Nonempty κ, ∃ M : RootedModel κ α, ∃ _ : Fintype M.World, ∃ _ : M.IsGL,
24+
(M.height = n ∧ M.root.1 ⊮ A)
25+
}
26+
27+
@[grind =]
28+
lemma iff_mem_trace :
29+
n ∈ A.trace ↔
30+
∃ κ : Type u, ∃ _ : Nonempty κ, ∃ M : RootedModel κ α, ∃ _ : Fintype M.World, ∃ _ : M.IsGL, M.height = n ∧ M.root.1 ⊮ A := by
31+
grind;
32+
33+
@[grind =]
34+
lemma iff_mem_not_trace :
35+
n ∉ A.trace ↔
36+
∀ κ : Type u, ∀ _ : Nonempty κ, ∀ M : RootedModel κ α, ∀ _ : Fintype M.World, ∀ _ : M.IsGL, M.height = n → M.root.1 ⊩ A := by
37+
grind;
38+
39+
variable {α : Type 0} {A B : Formula α}
40+
41+
@[grind =]
42+
lemma eq_trace_toLetterless_trace (hA : A.Letterless) : A.trace = LetterlessFormula.trace (A.toLetterless hA) := by
43+
ext n;
44+
45+
apply Iff.trans ?_ $ spectrum_TFAE.out 1 0 |>.not;
46+
push Not;
47+
rw [iff_mem_trace];
48+
constructor;
49+
. sorry;
50+
. rintro ⟨κ, _, _, M, _, x, rfl, h⟩;
51+
use κ, ‹_›;
52+
sorry;
53+
54+
@[simp, grind =]
55+
lemma trace_top : (⊤ : Formula α).trace = ∅ := by grind;
56+
57+
@[simp, grind =]
58+
lemma trace_bot : (⊥ : Formula α).trace = Set.univ := by
59+
rw [eq_trace_toLetterless_trace (A := ⊥) (by simp [Letterless])];
60+
exact LetterlessFormula.trace_bot;
61+
62+
@[simp, grind =]
63+
lemma trace_and : (A ⋏ B).trace = A.trace ∪ B.trace := by ext n; grind;
64+
65+
@[simp, grind =]
66+
lemma trace_lconj {Γ : FormulaList α} : (⋀Γ).trace = ⋃ A ∈ Γ, A.trace := by
67+
match Γ with
68+
| [] => simp;
69+
| [A] => simp;
70+
| A :: B :: Γ => simp [FormulaList.conj, trace_and, trace_lconj];
71+
72+
@[simp, grind =]
73+
lemma trace_fconj {Γ : FormulaFinset α} : (⋀Γ).trace = ⋃ A ∈ Γ, A.trace := by
74+
simp [FormulaFinset.conj, trace_lconj]
75+
76+
lemma subset_trace_of_provable_GL (h : A 🡒 B ∈ LogicGL _) : B.trace ⊆ A.trace := by
77+
intro n;
78+
simp only [iff_mem_trace];
79+
rintro ⟨κ, _, M, _, _, rfl, hB⟩;
80+
use κ, ‹_›, M, ‹_›, ‹_›, rfl;
81+
revert hB;
82+
contrapose!;
83+
show M.root.1 ⊩ A 🡒 B;
84+
sorry;
85+
86+
end Formula
87+
88+
89+
90+
end

0 commit comments

Comments
 (0)