feat(Modal): Independency of consistency is undecidable in GL

Foundation.lean

@@ -65,6 +65,7 @@ import Foundation.IntProp.Dialectica.Basic
 
 -- Modal
 
+import Foundation.Modal.Hilbert.GL_Independency
 import Foundation.Modal.Hilbert.Subst
 import Foundation.Modal.Hilbert.Maximal.Unprovability
 

Foundation/Logic/HilbertStyle/Supplemental.lean

@@ -58,6 +58,7 @@ omit [DecidableEq F] in lemma neg_mdp! (hnp : 𝓢 ⊢! ∼φ) (hn : 𝓢 ⊢! 
 -- infixl:90 "⨀" => neg_mdp!
 
 def dneOr [HasAxiomDNE 𝓢] (d : 𝓢 ⊢ ∼∼φ ⋎ ∼∼ψ) : 𝓢 ⊢ φ ⋎ ψ := or₃''' (impTrans'' dne or₁) (impTrans'' dne or₂) d
+omit [DecidableEq F] in lemma dne_or! [HasAxiomDNE 𝓢] (d : 𝓢 ⊢! ∼∼φ ⋎ ∼∼ψ) : 𝓢 ⊢! φ ⋎ ψ := ⟨dneOr d.some⟩
 
 def implyLeftOr' (h : 𝓢 ⊢ φ ➝ χ) : 𝓢 ⊢ φ ➝ (χ ⋎ ψ) := by
   apply deduct';

Foundation/Modal/Hilbert/GL_Independency.lean

@@ -0,0 +1,67 @@
+import Foundation.Modal.Hilbert.Maximal.Unprovability
+import Foundation.Modal.Kripke.GL.MDP
+
+namespace LO.Modal
+
+open System
+open IntProp
+
+variable [DecidableEq α]
+
+def independency (φ : Formula α) := ∼□φ ⋏ ∼□(∼φ)
+
+def higherIndependency (φ : Formula α) : ℕ → Formula α
+  | 0 => φ
+  | n + 1 => independency (higherIndependency φ n)
+
+namespace Hilbert.GL
+
+variable {φ : Formula ℕ}
+
+lemma unprovable_notbox : (Hilbert.GL _) ⊬ ∼□φ := by
+  by_contra hC;
+  have : (Hilbert.GL _) ⊢! ∼□φ ➝ ∼□⊥ := contra₀'! (imply_box_distribute'! efq!)
+  have : Hilbert.GL _ ⊢! ∼□⊥ := this ⨀ hC;
+  have : Hilbert.Cl ℕ ⊢! (⊥ ➝ ⊥) ➝ ⊥ := by simpa using provable_CL_verTranslated this;
+  simpa using Hilbert.Cl.classical_sound this;
+
+lemma unprovable_independency : (Hilbert.GL _) ⊬ independency φ := by
+  by_contra hC;
+  exact unprovable_notbox $ and₁'! hC;
+
+lemma unprovable_not_independency_of_consistency : (Hilbert.GL ℕ) ⊬ ∼(independency (∼□⊥)) := by
+  by_contra hC;
+  rcases modal_disjunctive (dne_or! $ demorgan₄'! hC) with (h | h);
+  . exact unprovable_notbox h;
+  . exact Consistent.not_bot (inferInstance) $ unnec! $ dne'! h
+
+theorem undecidable_independency_of_consistency : Undecidable (Hilbert.GL ℕ) (independency (∼□⊥)) := by
+  constructor;
+  . exact unprovable_independency;
+  . exact unprovable_not_independency_of_consistency;
+
+variable {n : ℕ}
+
+lemma unprovable_higherIndependency_of_consistency : (Hilbert.GL ℕ) ⊬ higherIndependency (∼□⊥) n := by
+  induction n with
+  | zero => exact unprovable_notbox;
+  | succ n ih => exact unprovable_independency;
+
+lemma unprovable_not_higherIndependency_of_consistency : (Hilbert.GL ℕ) ⊬ ∼(higherIndependency (∼□⊥) n) := by
+  by_contra hC;
+  induction n with
+  | zero =>
+    exact Consistent.not_bot (inferInstance) $ unnec! $ dne'! hC;
+  | succ n ih =>
+    rcases modal_disjunctive (dne_or! $ demorgan₄'! hC) with (h | h);
+    . exact unprovable_higherIndependency_of_consistency h;
+    . exact ih h;
+
+theorem undecidable_higherIndependency_of_consistency : Undecidable (Hilbert.GL ℕ) (higherIndependency (∼□⊥) n) := by
+  constructor;
+  . exact unprovable_higherIndependency_of_consistency;
+  . exact unprovable_not_higherIndependency_of_consistency;
+
+end Hilbert.GL
+
+end LO.Modal