diff --git a/Foundation/Modal/Hilbert/GS.lean b/Foundation/Modal/Hilbert/GS.lean
new file mode 100644
index 000000000..2276b80bf
--- /dev/null
+++ b/Foundation/Modal/Hilbert/GS.lean
@@ -0,0 +1,232 @@
+import Foundation.Modal.Logic.WellKnown
+import Foundation.Modal.Hilbert.WellKnown
+import Foundation.Modal.Entailment.GL
+import Mathlib.Tactic.TFAE
+import Foundation.Modal.Boxdot.GL_Grz
+
+namespace LO.Entailment
+
+open FiniteContext
+
+variable {S F : Type*} [BasicModalLogicalConnective F] [Entailment F S]
+variable {𝓢 : S} {φ ψ : F}
+
+class NecCongr [LogicalConnective F] (𝓢 : S) where
+  nec_congr {φ ψ : F} : 𝓢 ⊢ φ ⭤ ψ → 𝓢 ⊢ □φ ⭤ □ψ
+
+section
+
+variable [NecCongr 𝓢]
+
+alias nec_congr := NecCongr.nec_congr
+lemma nec_congr! {φ ψ : F} : 𝓢 ⊢! φ ⭤ ψ → 𝓢 ⊢! □φ ⭤ □ψ := by rintro ⟨hp⟩; exact ⟨nec_congr hp⟩
+
+end
+
+
+class RosserRule [LogicalConnective F] (𝓢 : S) where
+  rosser {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ ∼□φ
+
+section
+
+variable [RosserRule 𝓢]
+
+alias rosser := RosserRule.rosser
+lemma rosser! : 𝓢 ⊢! φ → 𝓢 ⊢! ∼□φ := by rintro ⟨hp⟩; exact ⟨rosser hp⟩
+
+end
+
+
+protected class Modal.GS (𝓢 : S) extends Entailment.Cl 𝓢, HasDiaDuality 𝓢, HasAxiomT 𝓢, RosserRule 𝓢, NecCongr 𝓢 where
+  Ax2 (φ ψ : F) : 𝓢 ⊢ (φ ⋏ □φ) ➝ □φ ⋎ □(φ ➝ ψ)
+  Ax3 (φ : F) : 𝓢 ⊢ φ ➝ ◇□φ
+  Ax4 (φ : F) : 𝓢 ⊢ □(∼□φ) ➝ □(φ ⋎ □(∼□φ))
+
+section
+
+variable [Modal.GS 𝓢]
+
+namespace Modal.GS
+
+protected def axiomK : 𝓢 ⊢ Axioms.K φ ψ := by
+  sorry;
+instance : HasAxiomK 𝓢 := ⟨fun _ _ ↦ Modal.GS.axiomK⟩
+
+protected def axiomFour : 𝓢 ⊢ Axioms.Four φ := by
+  sorry;
+instance : HasAxiomFour 𝓢 := ⟨fun _ ↦ Modal.GS.axiomFour⟩
+
+end Modal.GS
+
+end
+
+
+end LO.Entailment
+
+
+namespace LO.Modal
+
+namespace Hilbert
+
+open Entailment
+
+variable {α : Type*}
+
+protected structure GS_System (α : Type*) where
+  axioms : Set (Formula α)
+
+namespace GS_System
+
+abbrev axiomInstances (H : Hilbert.GS_System α) : Set (Formula α) := { φ⟦s⟧ | (φ ∈ H.axioms) (s : Substitution α) }
+
+inductive Deduction (H : Hilbert.GS_System α) : (Formula α) → Type _
+  | imply₁ φ ψ   : Deduction H $ Axioms.Imply₁ φ ψ
+  | imply₂ φ ψ χ : Deduction H $ Axioms.Imply₂ φ ψ χ
+  | ec φ ψ       : Deduction H $ Axioms.ElimContra φ ψ
+  | mdp {φ ψ}    : Deduction H (φ ➝ ψ) → Deduction H φ → Deduction H ψ
+  | maxm {φ}      : φ ∈ H.axiomInstances → Deduction H φ
+  | nec_congr {φ ψ}       : Deduction H (φ ⭤ ψ) → Deduction H (□φ ⭤ □ψ)
+  | rosser {φ}         : Deduction H φ → Deduction H (∼□φ)
+
+namespace Deduction
+
+variable {H H₁ H₂ : Hilbert.GS_System α}
+
+instance : Entailment (Formula α) (Hilbert.GS_System α) := ⟨Deduction⟩
+
+instance : Entailment.Lukasiewicz H where
+  mdp := mdp
+  imply₁ := imply₁
+  imply₂ := imply₂
+  elim_contra := ec
+
+instance : Entailment.Cl H where
+
+instance : Entailment.HasDiaDuality H := inferInstance
+instance : Entailment.RosserRule H := ⟨rosser⟩
+instance : Entailment.NecCongr H := ⟨nec_congr⟩
+
+lemma maxm! {φ} (h : φ ∈ H.axiomInstances) : H ⊢! φ := ⟨maxm h⟩
+
+noncomputable def rec!
+  {motive      : (φ : Formula α) → H ⊢! φ → Sort*}
+  (maxm       : ∀ {φ}, (h : φ ∈ H.axiomInstances) → motive φ (maxm! h))
+  (mdp        : ∀ {φ ψ}, {hpq : H ⊢! φ ➝ ψ} → {hp : H ⊢! φ} → motive (φ ➝ ψ) hpq → motive φ hp → motive ψ (mdp! hpq hp))
+  (nec_congr  : ∀ {φ ψ}, {hp : H ⊢! φ ⭤ ψ} → (ihp : motive (φ ⭤ ψ) hp) → motive (□φ ⭤ □ψ) (nec_congr! hp))
+  (rosser     : ∀ {φ}, {hp : H ⊢! φ} → (ihp : motive φ hp) → motive (∼□φ) (rosser! hp))
+  (imply₁     : ∀ {φ ψ}, motive (Axioms.Imply₁ φ ψ) $ ⟨imply₁ φ ψ⟩)
+  (imply₂     : ∀ {φ ψ χ}, motive (Axioms.Imply₂ φ ψ χ) $ ⟨imply₂ φ ψ χ⟩)
+  (ec : ∀ {φ ψ}, motive (Axioms.ElimContra φ ψ) $ ⟨ec φ ψ⟩)
+  : ∀ {φ}, (d : H ⊢! φ) → motive φ d := by
+  intro φ d;
+  induction d.some with
+  | maxm h => exact maxm h
+  | mdp hpq hp ihpq ihp => exact mdp (ihpq ⟨hpq⟩) (ihp ⟨hp⟩)
+  | rosser hp ihp => exact rosser (ihp ⟨hp⟩)
+  | nec_congr hp ihp => exact nec_congr (ihp ⟨hp⟩)
+  | _ => aesop;
+
+def subst! {φ} (s) (h : H ⊢! φ) : H ⊢! φ⟦s⟧ := by
+  induction h using Deduction.rec! with
+  | imply₁ => simp;
+  | imply₂ => simp;
+  | ec => simp;
+  | mdp ihφψ ihφ => exact ihφψ ⨀ ihφ;
+  | nec_congr ihφ => exact nec_congr! ihφ;
+  | rosser ihφ => exact rosser! ihφ;
+  | maxm h =>
+    obtain ⟨ψ, h, ⟨s', rfl⟩⟩ := h;
+    apply maxm!;
+    use ψ;
+    constructor;
+    . assumption;
+    . use s' ∘ s;
+      simp;
+
+end Deduction
+
+end GS_System
+
+protected abbrev GS : Hilbert.GS_System ℕ := ⟨{
+  □(.atom 0) ➝ (.atom 0),
+  ((.atom 0) ⋏ □(.atom 0)) ➝ □(.atom 0) ⋎ □((.atom 0) ➝ (.atom 1)),
+  (.atom 0) ➝ ◇□(.atom 0),
+  □(∼□(.atom 0)) ➝ □((.atom 0) ⋎ □(∼□(.atom 0)))
+}⟩
+instance : Entailment.Modal.GS (Hilbert.GS) where
+  T φ := by
+    apply GS_System.Deduction.maxm;
+    use Axioms.T (.atom 0);
+    constructor;
+    . tauto;
+    . use λ _ => φ; tauto;
+  Ax2 φ ψ := by
+    apply GS_System.Deduction.maxm;
+    use ((.atom 0) ⋏ □(.atom 0)) ➝ □(.atom 0) ⋎ □((.atom 0) ➝ (.atom 1));
+    constructor;
+    . tauto;
+    . use λ b => if b = 0 then φ else ψ; tauto;
+  Ax3 φ := by
+    apply GS_System.Deduction.maxm;
+    use (.atom 0) ➝ ◇□(.atom 0);
+    constructor;
+    . tauto;
+    . use λ _ => φ; tauto;
+  Ax4 φ := by
+    apply GS_System.Deduction.maxm;
+    use □(∼□(.atom 0)) ➝ □((.atom 0) ⋎ □(∼□(.atom 0)));
+    constructor;
+    . tauto;
+    . use λ _ => φ; tauto;
+
+end Hilbert
+
+
+
+def Formula.gsTranslate : Formula ℕ → Formula ℕ
+  | .atom a => .atom a
+  | ⊥ => ⊥
+  | φ ➝ ψ => φ.gsTranslate ➝ ψ.gsTranslate
+  | □φ => φ.gsTranslate ⋏ ∼□(φ.gsTranslate)
+postfix:max "ᴾ" => Formula.gsTranslate
+
+variable {φ : Formula ℕ}
+
+lemma provable_Grz_gsTranslated_of_provable_GS (h : Hilbert.GS ⊢! φ) : Hilbert.Grz ⊢! φᴾ := by sorry
+
+lemma provable_GS_translated_of_provable_Grz (h : Hilbert.Grz ⊢! φ) : Hilbert.GS ⊢! φᴾ := by sorry
+
+lemma iff_provable_Grz_provable_gsTranslated_GS : Hilbert.Grz ⊢! φ ↔ Hilbert.GS ⊢! φᴾ := by
+  constructor;
+  . exact provable_GS_translated_of_provable_Grz;
+  . sorry;
+
+lemma iff_provable_GS_gsTranslated_Grz : Hilbert.GS ⊢! φ ↔ Hilbert.Grz ⊢! φᴾ := by
+  constructor;
+  . exact provable_Grz_gsTranslated_of_provable_GS;
+  . sorry;
+
+lemma iff_provable_gsTranslate_boxdotTranslate_provable_gsTranslate_inside : Hilbert.GL ⊢! φᴾᵇ ⭤ φᴾ := by
+  induction φ using Formula.rec' with
+  | hatom φ => simp [Formula.gsTranslate, Formula.BoxdotTranslation];
+  | hfalsum => simp [Formula.gsTranslate, Formula.BoxdotTranslation];
+  | himp φ ψ ihφ ihψ =>
+    simp [Formula.gsTranslate, Formula.BoxdotTranslation];
+    sorry;
+  | hbox φ ihφ =>
+    simp [Formula.gsTranslate, Formula.BoxdotTranslation];
+    sorry;
+
+lemma iff_provable_gsTranslate_boxdotTranslate_provable_gsTranslate : Hilbert.GL ⊢! φᴾᵇ ↔ Hilbert.GL ⊢! φᴾ := ⟨
+  λ h => (Entailment.and₁'! iff_provable_gsTranslate_boxdotTranslate_provable_gsTranslate_inside) ⨀ h,
+  λ h => (Entailment.and₂'! iff_provable_gsTranslate_boxdotTranslate_provable_gsTranslate_inside) ⨀ h
+⟩
+
+lemma iff_provable_GS_provable_boxdot_GL : Hilbert.GS ⊢! φ ↔ Hilbert.GL ⊢! φᴾ := by
+  apply Iff.trans iff_provable_GS_gsTranslated_Grz;
+  apply Iff.trans Hilbert.iff_boxdotTranslatedGL_Grz.symm;
+  exact iff_provable_gsTranslate_boxdotTranslate_provable_gsTranslate;
+
+def Logic.GS : Modal.Logic := { φ | Hilbert.GS ⊢! φ }
+
+end LO.Modal
diff --git a/Foundation/ProvabilityLogic/GS/Completeness.lean b/Foundation/ProvabilityLogic/GS/Completeness.lean
new file mode 100644
index 000000000..e07294aca
--- /dev/null
+++ b/Foundation/ProvabilityLogic/GS/Completeness.lean
@@ -0,0 +1,69 @@
+import Foundation.ProvabilityLogic.Grz.Completeness
+import Foundation.Modal.Hilbert.GS
+
+namespace LO.ProvabilityLogic
+
+open FirstOrder FirstOrder.DerivabilityCondition
+open Modal
+open Modal.Hilbert
+open FirstOrder
+open Entailment FiniteContext
+
+variable {L} [Semiterm.Operator.GoedelNumber L (Sentence L)] [DecidableEq (Sentence L)]
+         {T₀ T : Theory L} [T₀ ⪯ T] {A : Modal.Formula ℕ}
+
+namespace Realization
+
+variable {𝔅 : ProvabilityPredicate T₀ T} {f : Realization L} {A B : Modal.Formula _}
+
+/-- Interpret `□` as _"True but Unprovable"_ -/
+def gsInterpret (f : Realization L) (𝔅 : ProvabilityPredicate T₀ T) : Formula ℕ → Sentence L
+  | .atom a => f a
+  | ⊥ => ⊥
+  | φ ➝ ψ => (f.gsInterpret 𝔅 φ) ➝ (f.gsInterpret 𝔅 ψ)
+  | □φ => (f.gsInterpret 𝔅 φ) ⋏ ∼𝔅 (f.gsInterpret 𝔅 φ)
+
+lemma iff_interpret_gsTranslate_gsInterpret_inside [𝔅.HBL2] : T ⊢!. f.interpret 𝔅 (Aᴾ) ⭤ f.gsInterpret 𝔅 A := by
+  induction A using Formula.rec' with
+  | hatom φ => simp [Realization.interpret, gsInterpret, Formula.gsTranslate];
+  | hfalsum => simp [Realization.interpret, gsInterpret, Formula.gsTranslate];
+  | himp A B ihA ihB => exact Epq_Ers_EIprIqs! ihA ihB;
+  | hbox A ih =>
+    apply and₃'!;
+    . apply imp_trans''! IIIpIqbbApq! ?_;
+      apply and_replace!;
+      . exact and₁'! ih;
+      . apply imp_trans''! (and₁'! iff_interpret_neg_inside) ?_;
+        apply contra₀'!;
+        apply 𝔅.prov_distribute_imply'';
+        apply and₂'! ih;
+    . apply imp_trans''! ?_ ApqIIpIqbb!;
+      apply and_replace!;
+      . exact and₂'! ih;
+      . apply imp_trans''! ?_ (and₂'! iff_interpret_neg_inside);
+        apply contra₀'!;
+        apply 𝔅.prov_distribute_imply'';
+        apply and₁'! ih;
+
+lemma iff_interpret_gsTranslate_gsInterpret [𝔅.HBL2] : T ⊢!. f.interpret 𝔅 (Aᴾ) ↔ T ⊢!. f.gsInterpret 𝔅 A := by
+  constructor;
+  . intro h; exact (and₁'! iff_interpret_gsTranslate_gsInterpret_inside) ⨀ h;
+  . intro h; exact (and₂'! iff_interpret_gsTranslate_gsInterpret_inside) ⨀ h;
+
+end Realization
+
+variable {T : Theory ℒₒᵣ} [T.Delta1Definable] [𝐈𝚺₁ ⪯ T] [Arith.SoundOn T (Arith.Hierarchy 𝚷 2)]
+
+theorem GS.arithmetical_completeness_iff :
+  (∀ {f : Realization ℒₒᵣ}, T ⊢!. f.gsInterpret ((𝐈𝚺₁).standardDP T) A) ↔ A ∈ Logic.GS := by
+  apply Iff.trans ?_ iff_provable_GS_provable_boxdot_GL.symm;
+  apply Iff.trans ?_ (GL.arithmetical_completeness_iff (T := T));
+  constructor;
+  . intro h f;
+    apply Realization.iff_interpret_gsTranslate_gsInterpret (L := ℒₒᵣ) |>.mpr;
+    apply h;
+  . intro h f;
+    apply Realization.iff_interpret_gsTranslate_gsInterpret (L := ℒₒᵣ) |>.mp;
+    apply h;
+
+end LO.ProvabilityLogic