update

FormalizedFormalLogic · Sep 5, 2024 · 773fd52 · 773fd52
1 parent 6b5e0b9
commit 773fd52
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 4 deletions.
diff --git a/Incompleteness/Modal/Basic.lean b/Incompleteness/Modal/Basic.lean
@@ -1,5 +1,5 @@
 import Incompleteness.DC.Basic
-import Logic.Modal.Standard.Deduction
+import Logic.Modal.Hilbert
 
 namespace LO.Modal.Standard.Provability
 
@@ -91,6 +91,7 @@ lemma arithmetical_soundness_K4Loeb [𝔟.HBL T₀ T] (h : 𝐊𝟒(𝐋) ⊢! p
     exact ihpq ⨀ ihp;
   | _ => dsimp [interpretation]; trivial;
 
+/-
 theorem arithmetical_soundness_GL [𝔟.HBL T₀ T] (h : 𝐆𝐋 ⊢! p) : ∀ {f : realization L α}, T ⊢!. (f[𝔟] p) := by
   apply arithmetical_soundness_K4Loeb (T₀ := T₀);
   exact (System.weakerThan_iff.mp reducible_GL_K4Loeb) h;
@@ -109,7 +110,7 @@ lemma arithmetical_soundness_N [𝔟.HBL T₀ T] (h : 𝐍 ⊢! p) : ∀ {f : re
     simp only [interpretation] at ihpq;
     exact ihpq ⨀ ihp;
   | _ => dsimp [interpretation]; trivial;
-
+-/
 end ArithmeticalSoundness
 
 end Modal.Standard.Provability

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b090504b6c2ac5f36060662a91d8230ea421946d",
+   "rev": "24006582e25395fb5fa3da38181905cff44d0f36",
    "name": "logic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2406be6bc8f37bc92373d5f9534dbb79218bc2cb",
+   "rev": "1805c5a19a4fa5987d02b0d47b006c7cc6d810b6",
    "name": "arithmetization",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",