Refactor Provability Predicate and Arithmetical Soundness (#1)

* wip

* upd

* upd deps

* notation fix

* fx by review

.gitignore

@@ -1,3 +1,6 @@
 /build
 /lake-packages/*
-/.lake
+/.lake
+
+# VSCode
+.vscode/settings.json

Incompleteness.lean

@@ -6,4 +6,5 @@ import Incompleteness.Arith.First
 import Incompleteness.Arith.Second
 import Incompleteness.Arith.DC
 import Incompleteness.DC.Basic
-import Incompleteness.Modal.Basic
+
+import Incompleteness.ProvabilityLogic.ProvabilityLogic

Incompleteness/Arith/DC.lean

@@ -18,13 +18,14 @@ instance : Diagonalization T where
   fixpoint := fixpoint
   diag θ := diagonal θ
 
-abbrev _root_.LO.FirstOrder.Theory.standardDP : ProvabilityPredicate ℒₒᵣ ℒₒᵣ := ⟨U.provableₐ⟩
-
-instance : U.standardDP.HBL1 T U := ⟨provableₐ_D1⟩
-instance : U.standardDP.HBL2 T U := ⟨provableₐ_D2⟩
-instance : U.standardDP.HBL3 T U := ⟨provableₐ_D3⟩
-instance : U.standardDP.HBL T U := ⟨⟩
-instance : U.standardDP.GoedelSound T U := ⟨fun h ↦ by simpa using provableₐ_sound h⟩
+abbrev _root_.LO.FirstOrder.Theory.standardDP : ProvabilityPredicate T U where
+  prov := U.provableₐ
+  spec := provableₐ_D1
+
+instance : (Theory.standardDP T U).HBL2 := ⟨provableₐ_D2⟩
+instance : (Theory.standardDP T U).HBL3 := ⟨provableₐ_D3⟩
+instance : (Theory.standardDP T U).HBL := ⟨⟩
+instance : (Theory.standardDP T U).GoedelSound := ⟨fun h ↦ by simpa using provableₐ_sound h⟩
 
 end LO.FirstOrder.Arith
 

Incompleteness/ProvabilityLogic/Basic.lean

@@ -0,0 +1,81 @@
+import Incompleteness.Arith.DC
+import Incompleteness.DC.Basic
+import Logic.Modal.Hilbert
+
+namespace LO
+
+open LO.FirstOrder LO.FirstOrder.DerivabilityCondition
+open LO.Modal
+
+variable {α : Type u} [DecidableEq α]
+variable [Semiterm.Operator.GoedelNumber L (Sentence L)]
+         {T U : Theory L}
+
+
+namespace ProvabilityLogic
+
+/-- Mapping modal prop vars to first-order sentence -/
+def Realization (α : Type u) (L) := α → FirstOrder.Sentence L
+
+/-- Mapping modal formulae to first-order sentence -/
+def Realization.interpret
+  {T U : FirstOrder.Theory L}
+  (f : Realization α L) (𝔅 : ProvabilityPredicate T U) : Formula α → FirstOrder.Sentence L
+  | .atom a => f a
+  | □p => 𝔅 (f.interpret 𝔅 p)
+  | ⊥ => ⊥
+  | p ⟶ q => (f.interpret 𝔅 p) ⟶ (f.interpret 𝔅 q)
+
+variable [Semiterm.Operator.GoedelNumber L (Sentence L)]
+
+class ArithmeticalSound (Λ : Hilbert α) (𝔅 : ProvabilityPredicate T U) where
+  sound : ∀ {p}, (Λ ⊢! p) → (∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 p))
+
+class ArithmeticalComplete (Λ : Hilbert α) (𝔅 : ProvabilityPredicate T U) where
+  complete : ∀ {p}, (∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 p)) → (Λ ⊢! p)
+
+
+section ArithmeticalSoundness
+
+open System
+open ProvabilityPredicate
+
+variable {L : FirstOrder.Language} [Semiterm.Operator.GoedelNumber L (Sentence L)]
+         [DecidableEq (Sentence L)]
+         {T U : FirstOrder.Theory L} [T ≼ U] [Diagonalization T]
+         {𝔅 : ProvabilityPredicate T U}
+
+lemma arithmetical_soundness_N (h : 𝐍 ⊢! p) : ∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 p) := by
+  intro f;
+  induction h using Deduction.inducition_with_necOnly! with
+  | hMaxm hp => simp at hp;
+  | hNec ihp => exact D1_shift ihp;
+  | hMdp ihpq ihp =>
+    simp only [Realization.interpret] at ihpq;
+    exact ihpq ⨀ ihp;
+  | _ => dsimp [Realization.interpret]; trivial;
+
+lemma arithmetical_soundness_GL [𝔅.HBL] (h : 𝐆𝐋 ⊢! p) : ∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 p) := by
+  intro f;
+  induction h using Deduction.inducition_with_necOnly! with
+  | hMaxm hp =>
+    rcases hp with (⟨_, _, rfl⟩ | ⟨_, rfl⟩)
+    . exact D2_shift;
+    . exact FLT_shift;
+  | hNec ihp => exact D1_shift ihp;
+  | hMdp ihpq ihp =>
+    simp [Realization.interpret] at ihpq;
+    exact ihpq ⨀ ihp;
+  | _ => dsimp [Realization.interpret]; trivial;
+
+end ArithmeticalSoundness
+
+
+section
+
+instance (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : ArithmeticalSound (𝐆𝐋 : Hilbert α) (T.standardDP T) := ⟨arithmetical_soundness_GL⟩
+
+end
+
+
+end LO.ProvabilityLogic

Incompleteness/ProvabilityLogic/ProvabilityLogic.lean

@@ -0,0 +1 @@
+import Incompleteness.ProvabilityLogic.Basic

lake-manifest.json

@@ -79,7 +79,7 @@
    "name": "logic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
-   "inherited": true,
+   "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/FormalizedFormalLogic/Arithmetization",
    "type": "git",

lakefile.lean

@@ -8,6 +8,8 @@ package «Incompleteness» where
   ]
   -- add any additional package configuration options here
 
+require «logic» from git "https://github.com/FormalizedFormalLogic/Foundation" @ "master"
+
 require arithmetization from git "https://github.com/FormalizedFormalLogic/Arithmetization" @ "master"
 
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.39"