glivenko

Author: SnO2WMaN

Foundation.lean

@@ -361,7 +361,6 @@ public import Foundation.Modal.MaximalConsistentSet
 public import Foundation.Modal.ModalCompanion
 public import Foundation.Modal.ModalCompanion.Corsi
 public import Foundation.Modal.ModalCompanion.Corsi.VF
-public import Foundation.Modal.ModalCompanion.Standard
 public import Foundation.Modal.ModalCompanion.Standard.Basic
 public import Foundation.Modal.ModalCompanion.Standard.Cl
 public import Foundation.Modal.ModalCompanion.Standard.Int
@@ -461,6 +460,7 @@ public import Foundation.Propositional.Hilbert.F.Deduction
 public import Foundation.Propositional.Hilbert.F.Disjunctive
 public import Foundation.Propositional.Hilbert.F_WF
 public import Foundation.Propositional.Hilbert.Minimal.Basic
+public import Foundation.Propositional.Hilbert.Minimal.Glivenko
 public import Foundation.Propositional.Hilbert.Standard
 public import Foundation.Propositional.Hilbert.Standard.Basic
 public import Foundation.Propositional.Hilbert.Standard.Glivenko

Foundation/Modal/ModalCompanion/Standard.lean

@@ -4,6 +4,7 @@ public import Foundation.Logic.Embedding
 public import Foundation.Modal.Boxdot.GL_Grz
 public import Foundation.Modal.ModalCompanion.Standard.Basic
 public import Foundation.Propositional.Kripke.Hilbert.Int.Basic
+public import Foundation.Propositional.Hilbert.Minimal.Glivenko
 
 @[expose] public section
 
@@ -58,24 +59,16 @@ instance : Entailment.FaithfullyEmbeddable Propositional.Int Modal.GL where
 end Propositional.Int
 
 
-/-
 namespace Propositional.Cl
 
 lemma iff_mem_S4_dia : φ ∈ Propositional.Cl ↔ Modal.S4 ⊢ ◇φᵍ := by
   constructor;
   . intro h;
-    suffices Modal.S4 ⊢ □◇φᵍ by exact axiomT'! this;
-    have := glivenko.mpr h;
-    have : Modal.S4 ⊢ (∼∼φ)ᵍ := ModalCompanion.companion.mp $ glivenko.mpr h;
-    cl_prover [this];
+    exact unnec! $ Propositional.Int.modalCompanion_S4.mp $ Hilbert.glivenko.mpr h;
   . intro h;
-    apply glivenko.mp;
-    suffices Modal.S4 ⊢ (∼∼φ)ᵍ by exact ModalCompanion.companion.mpr this;
-    replace h : Modal.S4 ⊢ □◇φᵍ := nec! h;
-    cl_prover [h];
+    exact Hilbert.glivenko.mp $ Propositional.Int.modalCompanion_S4.mpr $ nec! h;
 
 end Propositional.Cl
--/
 
 end LO
 

Foundation/Modal/ModalCompanion/Standard/Int.lean

@@ -0,0 +1,41 @@
+module
+
+public import Foundation.Propositional.Hilbert.Minimal.Basic
+public import Foundation.Meta.IntProver
+public import Foundation.Meta.ClProver
+
+@[expose] public section
+
+namespace LO.Propositional
+
+open LO.Entailment
+open Formula (atom)
+
+variable [DecidableEq α] {φ : Formula α}
+
+namespace Hilbert
+
+instance : (Hilbert.Int : Hilbert α) ⪯ Hilbert.Cl := Hilbert.weakerThan_of_le $ by simp
+
+theorem iff_provable_dn_Int_Cl : Hilbert.Int ⊢ ∼∼φ ↔ Hilbert.Cl ⊢ φ := by
+  constructor;
+  . intro d;
+    exact of_NN! $ WeakerThan.pbl d;
+  . intro ⟨d⟩;
+    induction d with
+    | mdp _ _ ihφψ ihφ => exact (CNNNN!_of_NNC! ihφψ) ⨀ ihφ;
+    | axm h => rcases h with (⟨_, rfl⟩ | ⟨_, rfl⟩) <;> int_prover;
+    | _ => apply dni'! (by simp);
+
+alias glivenko := iff_provable_dn_Int_Cl
+
+theorem iff_provable_neg_Int_neg_Cl : Hilbert.Int ⊢ ∼φ ↔ Hilbert.Cl ⊢ ∼φ := by
+  constructor;
+  . intro d; exact glivenko.mp $ dni'! d;
+  . intro d; exact tne'! $ glivenko.mpr d;
+
+end Hilbert
+
+end LO.Propositional
+
+end