diff --git a/Cslib.lean b/Cslib.lean
index 3ec5b03f6..4071b90af 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -69,6 +69,7 @@ public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
+public import Cslib.Foundations.Logic.Connectives
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
 public import Cslib.Foundations.Semantics.FLTS.Basic
@@ -142,6 +143,10 @@ public import Cslib.Logics.Modal.Denotation
 public import Cslib.Logics.Modal.LogicalEquivalence
 public import Cslib.Logics.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+public import Cslib.Logics.Temporal.Syntax.BigConj
+public import Cslib.Logics.Temporal.Syntax.Context
+public import Cslib.Logics.Temporal.Syntax.Formula
+public import Cslib.Logics.Temporal.Syntax.Subformulas
 public import Cslib.MachineLearning.PACLearning.Defs
 public import Cslib.MachineLearning.PACLearning.VCDimension
 public import Cslib.MachineLearning.PACLearning.VersionSpace
diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean
new file mode 100644
index 000000000..0cd746c9d
--- /dev/null
+++ b/Cslib/Foundations/Logic/Connectives.lean
@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Brast-McKie
+-/
+
+module
+
+import Cslib.Init
+
+/-! # Connective Typeclasses for Composable Logics
+
+This module defines a typeclass hierarchy for logical connectives, shared across the four
+logic levels (Propositional, Modal, Temporal, Bimodal). Each formula type registers itself
+as an instance of the appropriate connective class, enabling polymorphic axiom definitions
+and notation.
+
+## Design
+
+The hierarchy follows the Foundation pattern (FormalizedFormalLogic/Foundation):
+- **Atomic classes**: `HasBot`, `HasImp`, `HasBox`, `HasUntil`, `HasSince`
+- **Bundled classes**: `PropositionalConnectives`, `ModalConnectives`,
+  `TemporalConnectives`, `BimodalConnectives`
+- **Derived connectives**: `LukasiewiczDerived` for `neg`, `top`, `or`, `and` from `bot`/`imp`
+
+Each concrete formula type duplicates its constructors (Lean 4 cannot extend inductives)
+and registers as an instance of the appropriate bundled class.
+
+## References
+
+* [A. Church, *Introduction to Mathematical Logic*][Church1956]
+* [A. Heyting, *Die formalen Regeln der intuitionistischen Logik*][Heyting1930]
+* [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935]
+* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- A type has a falsum (bottom) connective. -/
+class HasBot (F : Type*) where
+  /-- The falsum/bottom connective. -/
+  bot : F
+
+/-- A type has an implication connective. -/
+class HasImp (F : Type*) where
+  /-- The implication connective. -/
+  imp : F → F → F
+
+/-- A type has a necessity (box) modality. -/
+class HasBox (F : Type*) where
+  /-- The necessity/box modality. -/
+  box : F → F
+
+/-- A type has an until temporal operator. -/
+class HasUntil (F : Type*) where
+  /-- The until temporal operator. -/
+  untl : F → F → F
+
+/-- A type has a since temporal operator. -/
+class HasSince (F : Type*) where
+  /-- The since temporal operator. -/
+  snce : F → F → F
+
+/-- Propositional connectives: falsum and implication. -/
+class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F
+
+/-- Modal connectives: propositional connectives plus necessity. -/
+class ModalConnectives (F : Type*) extends PropositionalConnectives F, HasBox F
+
+/-- Temporal connectives: propositional connectives plus until and since. -/
+class TemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F, HasSince F
+
+/-- Bimodal connectives: modal connectives plus until and since.
+    Note: we extend `ModalConnectives` and add `HasUntil`/`HasSince` directly
+    rather than extending `TemporalConnectives`, to avoid a typeclass diamond. -/
+class BimodalConnectives (F : Type*) extends ModalConnectives F, HasUntil F, HasSince F
+
+/-- Lukasiewicz-style derived connectives from `bot` and `imp`.
+
+Provides `neg`, `top`, `or`, `and` as abbreviations following the standard Lukasiewicz
+encoding: negation is implication to falsum, verum is `bot → bot`, disjunction is
+`¬φ → ψ`, and conjunction is `¬(φ → ¬ψ)`.
+
+**Status**: This class is intentionally uninstantiated. Each concrete formula type
+(PL.Proposition, Modal.Proposition, Temporal.Formula, Bimodal.Formula) defines its
+own `abbrev` connectives directly on the inductive constructors, which are
+definitionally equal to these defaults. Registering typeclass instances would add
+resolution overhead at every use site with no benefit, since the `abbrev` definitions
+already compute. The class is retained as a specification artifact and for potential
+future use in polymorphic proof-system abstractions that need to quantify over derived
+connectives generically. -/
+class LukasiewiczDerived (F : Type*) [HasBot F] [HasImp F] where
+  /-- Negation: `neg φ := imp φ bot` -/
+  neg : F → F := fun φ => HasImp.imp φ HasBot.bot
+  /-- Top/verum: `top := imp bot bot` -/
+  top : F := HasImp.imp HasBot.bot HasBot.bot
+  /-- Disjunction: `or φ ψ := imp (neg φ) ψ` where `neg φ := imp φ bot` -/
+  or : F → F → F := fun φ ψ => HasImp.imp (HasImp.imp φ HasBot.bot) ψ
+  /-- Conjunction: `and φ ψ := neg (imp φ (neg ψ))` -/
+  and : F → F → F := fun φ ψ =>
+    HasImp.imp (HasImp.imp φ (HasImp.imp ψ HasBot.bot)) HasBot.bot
+
+end Cslib.Logic
diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean
index 854b8deb1..3a111589f 100644
--- a/Cslib/Foundations/Logic/InferenceSystem.lean
+++ b/Cslib/Foundations/Logic/InferenceSystem.lean
@@ -6,9 +6,9 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Init
+import Cslib.Init
 
-/-! -/
+/-! # Inference System Typeclass -/
 
 @[expose] public section
 
diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index fa3caf53e..01a07b7d2 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -1,22 +1,24 @@
 /-
-Copyright (c) 2025 Thomas Waring. All rights reserved.
+Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Thomas Waring
+Authors: Thomas Waring, Benjamin Brast-McKie
 -/
 
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Logic.Connectives
 public import Mathlib.Data.FunLike.Basic
-public import Mathlib.Data.Set.Image
+public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.TypeTags
 
 /-! # Propositions and theories
 
 ## Main definitions
 
-- `Proposition` : the type of propositions over a given type of atom. This type has a `Bot`
-instance whenever `Atom` does, and a `Top` whenever `Atom` is inhabited.
+- `Proposition` : the type of propositions over a given type of atom. Primitives are `atom`,
+  `bot` (falsum), and `imp` (implication). Conjunction, disjunction, negation, and verum are
+  derived connectives following the Lukasiewicz convention.
 - `Theory` : set of `Proposition`.
 - `IsIntuitionistic` : a theory is intuitionistic if it contains the principle of explosion.
 - `IsClassical` : an intuitionistic theory is classical if it further contains double negation
@@ -32,6 +34,11 @@ theory.
 
 We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,
 conjunction, disjunction, implication and negation.
+
+## References
+
+* [A. Church, *Introduction to Mathematical Logic*][Church1956]
+* [A. Chagrov, M. Zakharyaschev, *Modal Logic*][ChagrovZakharyaschev1997], Chapter 1
 -/
 
 @[expose] public section
@@ -42,44 +49,54 @@ variable {Atom : Type u} [DecidableEq Atom]
 
 namespace Cslib.Logic.PL
 
-/-- Propositions. -/
+/-- Propositions. Primitives are atoms, falsum, and implication. -/
 inductive Proposition (Atom : Type u) : Type u where
   /-- Propositional atoms -/
   | atom (x : Atom)
-  /-- Conjunction -/
-  | and (a b : Proposition Atom)
-  /-- Disjunction -/
-  | or (a b : Proposition Atom)
+  /-- Falsum / bottom -/
+  | bot
   /-- Implication -/
-  | impl (a b : Proposition Atom)
+  | imp (a b : Proposition Atom)
 deriving DecidableEq, BEq
 
-instance instBotProposition [Bot Atom] : Bot (Proposition Atom) := ⟨.atom ⊥⟩
-instance instInhabitedOfBot [Bot Atom] : Inhabited Atom := ⟨⊥⟩
+/-- Negation as a derived connective: ¬A := A → ⊥ -/
+abbrev Proposition.neg : Proposition Atom → Proposition Atom := (Proposition.imp · .bot)
 
-/-- We view negation as a defined connective ~A := A → ⊥ -/
-abbrev Proposition.neg [Bot Atom] : Proposition Atom → Proposition Atom := (Proposition.impl · ⊥)
+/-- Verum / top as a derived connective: ⊤ := ⊥ → ⊥ -/
+abbrev Proposition.top : Proposition Atom := .imp .bot .bot
 
-/-- A fixed choice of a derivable proposition (of course any two are equivalent). -/
-abbrev Proposition.top [Inhabited Atom] : Proposition Atom := impl (.atom default) (.atom default)
+/-- Disjunction as a derived connective: A ∨ B := ¬A → B -/
+abbrev Proposition.or (A B : Proposition Atom) : Proposition Atom :=
+  .imp (.imp A .bot) B
 
-instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top⟩
+/-- Conjunction as a derived connective: A ∧ B := ¬(A → ¬B) -/
+abbrev Proposition.and (A B : Proposition Atom) : Proposition Atom :=
+  .imp (.imp A (.imp B .bot)) .bot
 
-example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl
+/-- Biconditional as a derived connective: A ↔ B := (A → B) ∧ (B → A) -/
+abbrev Proposition.iff (A B : Proposition Atom) : Proposition Atom :=
+  (A.imp B).and (B.imp A)
+
+instance : Bot (Proposition Atom) := ⟨.bot⟩
+instance : Top (Proposition Atom) := ⟨.top⟩
 
 @[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
 @[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
+@[inherit_doc] scoped infix:30 " → " => Proposition.imp
 @[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg
 
+/-- Register `Proposition` as an instance of `PropositionalConnectives`. -/
+instance : PropositionalConnectives (Proposition Atom) where
+  bot := .bot
+  imp := .imp
+
 /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic
 language. -/
 def Proposition.subst {Atom Atom' : Type u} (f : Atom → Proposition Atom') :
     Proposition Atom → Proposition Atom'
   | atom x => f x
-  | and A B => (A.subst f) ∧ (B.subst f)
-  | or A B => (A.subst f) ∨ (B.subst f)
-  | impl A B => (A.subst f) → (B.subst f)
+  | bot => .bot
+  | imp A B => .imp (A.subst f) (B.subst f)
 
 -- This is probably a lawful monad, but that doesn't seem to be important.
 instance : Monad Proposition where
@@ -102,45 +119,45 @@ instance : Functor Theory where
 abbrev MPL : Theory (Atom) := ∅
 
 /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/
-abbrev IPL [Bot Atom] : Theory Atom :=
-  Set.range (⊥ → ·)
+abbrev IPL : Theory Atom :=
+  Set.range (Proposition.imp ⊥ ·)
 
 /-- Classical logic further adds double negation elimination. -/
-abbrev CPL [Bot Atom] : Theory Atom :=
+abbrev CPL : Theory Atom :=
   Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A)
 
 /-- A theory is intuitionistic if it validates ex falso quodlibet. -/
 @[scoped grind]
-class IsIntuitionistic [Bot Atom] (T : Theory Atom) where
+class IsIntuitionistic (T : Theory Atom) where
   efq (A : Proposition Atom) : (⊥ → A) ∈ T
 
 omit [DecidableEq Atom] in
 @[scoped grind =]
-theorem isIntuitionisticIff [Bot Atom] (T : Theory Atom) : IsIntuitionistic T ↔ IPL ⊆ T := by grind
+theorem isIntuitionisticIff (T : Theory Atom) : IsIntuitionistic T ↔ IPL ⊆ T := by grind
 
 /-- A theory is classical if it validates double-negation elimination. -/
 @[scoped grind]
-class IsClassical [Bot Atom] (T : Theory Atom) where
+class IsClassical (T : Theory Atom) where
   dne (A : Proposition Atom) : (¬¬A → A) ∈ T
 
 omit [DecidableEq Atom] in
 @[scoped grind =]
-theorem isClassicalIff [Bot Atom] (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind
+theorem isClassicalIff (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind
 
-instance instIsIntuitionisticIPL [Bot Atom] : IsIntuitionistic (Atom := Atom) IPL where
+instance instIsIntuitionisticIPL : IsIntuitionistic (Atom := Atom) IPL where
   efq A := Set.mem_range.mpr ⟨A, rfl⟩
 
-instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where
+instance instIsClassicalCPL : IsClassical (Atom := Atom) CPL where
   dne A := Set.mem_range.mpr ⟨A, rfl⟩
 
 omit [DecidableEq Atom] in
 @[scoped grind →]
-theorem instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T]
+theorem instIsIntuitionisticExtention {T T' : Theory Atom} [IsIntuitionistic T]
     (h : T ⊆ T') : IsIntuitionistic T' := by grind
 
 omit [DecidableEq Atom] in
 @[scoped grind →]
-theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') :
+theorem instIsClassicalExtention {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') :
     IsClassical T' := by grind
 
 /-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
index b1a8947e2..844bfab4b 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2025 Thomas Waring. All rights reserved.
+Copyright (c) 2025 Thomas Waring, 2026 Benjamin Brast-McKie. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Thomas Waring
+Authors: Thomas Waring, Benjamin Brast-McKie
 -/
 module
 
@@ -42,21 +42,18 @@ abbreviates a derivation of `A` in the empty context: `T⇓(∅ ⊢ A)`.
 
 ## Implementation notes
 
-We formalise here a single type of derivations, meaning there is a single collection of inference
-rules (those for minimal logic). The extension to intuitionistic and classical logic are modelled
-by adding *axioms* --- for instance, intuitionistic derivations are allowed to appeal to axioms of
-the form `⊥ → A` for any proposition `A`. This differs from many on-paper presentations, which add
-that principle as a deduction rule: from `Γ ⊢ ⊥` derive `Γ ⊢ A`. Discussion on proper way to
-capture such developments in cslib is ongoing, see the following
-[zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/513188-CSLib/topic/Logic/with/585843520).
+The primitive inference rules are: axiom (from theory), assumption (from context),
+implication introduction and elimination, and ex falso quodlibet (bottom elimination).
+Conjunction and disjunction rules are derivable from these primitives together with
+the Lukasiewicz definitions of `∧` and `∨` in terms of `→` and `⊥`.
 
 ## References
 
-- Dag Prawitz, *Natural Deduction: a proof-theoretical study*.
-- The sequent-style natural deduction I present here doesn't seem to be common, but it is tersely
-presented in §10.4 of Troelstra & van Dalen's *Constructivism in Mathematics: an introduction*, and
-in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (Suggestions of better
-references welcome!)
+* [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965]
+* [A. S. Troelstra, D. van Dalen,
+  *Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988], Section 10.4
+* [G. Gentzen,
+  *Untersuchungen über das logische Schließen*][Gentzen1935]
 -/
 
 @[expose] public section
@@ -83,32 +80,22 @@ abbrev Sequent {Atom} := Ctx Atom × Proposition Atom
 scoped notation Γ:60 " ⊢ " A => (⟨Γ, A⟩ : Sequent)
 
 /-- A `T`-derivation of {A₁, ..., Aₙ} ⊢ B demonstrates B using (undischarged) assumptions among Aᵢ,
-possibly appealing to axioms from `T`. -/
+possibly appealing to axioms from `T`. Primitives: axiom, assumption, implication intro/elim,
+and ex falso quodlibet (bottom elimination). -/
 inductive Theory.Derivation {T : Theory Atom} : Ctx Atom → Proposition Atom → Type u where
   /-- Axiom -/
   | ax {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ T) : Derivation Γ A
   /-- Assumption -/
   | ass {Γ : Ctx Atom} {A : Proposition Atom} (_ : A ∈ Γ) : Derivation Γ A
-  /-- Conjunction introduction -/
-  | andI {Γ : Ctx Atom} {A B : Proposition Atom} :
-      Derivation Γ A → Derivation Γ B → Derivation Γ (A ∧ B)
-  /-- Conjunction elimination left -/
-  | andE₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ A
-  /-- Conjunction elimination right -/
-  | andE₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ (A ∧ B) → Derivation Γ B
-  /-- Disjunction introduction left -/
-  | orI₁ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ A → Derivation Γ (A ∨ B)
-  /-- Disjunction introduction right -/
-  | orI₂ {Γ : Ctx Atom} {A B : Proposition Atom} : Derivation Γ B → Derivation Γ (A ∨ B)
-  /-- Disjunction elimination -/
-  | orE {Γ : Ctx Atom} {A B C : Proposition Atom} : Derivation Γ (A ∨ B) →
-      Derivation (insert A Γ) C → Derivation (insert B Γ) C → Derivation Γ C
   /-- Implication introduction -/
-  | implI {A B : Proposition Atom} (Γ : Ctx Atom) :
+  | impI {A B : Proposition Atom} (Γ : Ctx Atom) :
       Derivation (insert A Γ) B → Derivation Γ (A → B)
-  /-- Implication elimination -/
-  | implE {Γ : Ctx Atom} {A B : Proposition Atom} :
+  /-- Implication elimination (modus ponens) -/
+  | impE {Γ : Ctx Atom} {A B : Proposition Atom} :
       Derivation Γ (A → B) → Derivation Γ A → Derivation Γ B
+  /-- Ex falso quodlibet (bottom elimination) -/
+  | botE {Γ : Ctx Atom} {A : Proposition Atom} :
+      Derivation Γ ⊥ → Derivation Γ A
 
 /-- Inference system for derivations under the theory `T`. -/
 instance (T : Theory Atom) : InferenceSystem T (Sequent (Atom := Atom)) where
@@ -170,17 +157,9 @@ def Theory.Derivation.weak {T T' : Theory Atom} {Γ Δ : Ctx Atom} {A : Proposit
     (hTheory : T ⊆ T') (hCtx : Γ ⊆ Δ) : T.Derivation Γ A → T'.Derivation Δ A
   | ax hA => ax <| hTheory hA
   | ass hA => ass <| hCtx hA
-  | andI D D' => andI (D.weak hTheory hCtx) (D'.weak hTheory hCtx)
-  | andE₁ D => andE₁ <| D.weak hTheory hCtx
-  | andE₂ D => andE₂ <| D.weak hTheory hCtx
-  | orI₁ D => orI₁ <| D.weak hTheory hCtx
-  | orI₂ D => orI₂ <| D.weak hTheory hCtx
-  | orE D D' D'' =>
-    orE (D.weak hTheory hCtx)
-      (D'.weak hTheory <| Finset.insert_subset_insert _ hCtx)
-      (D''.weak hTheory <| Finset.insert_subset_insert _ hCtx)
-  | @implI _ _ _ A B Γ D => implI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx
-  | implE D D' => implE (D.weak hTheory hCtx) (D'.weak hTheory hCtx)
+  | @impI _ _ _ A B Γ D => impI (Δ) <| D.weak hTheory <| Finset.insert_subset_insert _ hCtx
+  | impE D D' => impE (D.weak hTheory hCtx) (D'.weak hTheory hCtx)
+  | botE D => botE <| D.weak hTheory hCtx
 
 /-- Weakening the theory only. -/
 def Theory.Derivation.weakTheory {T T' : Theory Atom} {Γ : Ctx Atom} {A : Proposition Atom}
@@ -213,9 +192,9 @@ substitution, which would replace appeals to `A` in `E` by the whole derivation
 -/
 def Theory.Derivation.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom}
     (D : T⇓(Γ ⊢ A)) (E : T⇓(insert A Δ ⊢ B)) : T⇓((Γ ∪ Δ) ⊢ B) := by
-  refine implE (A := A) ?_ (D.weakCtx Finset.subset_union_left)
+  refine impE (A := A) ?_ (D.weakCtx Finset.subset_union_left)
   have : insert A Δ ⊆ insert A (Γ ∪ Δ) := by grind
-  exact implI (Γ ∪ Δ) <| E.weakCtx this
+  exact impI (Γ ∪ Δ) <| E.weakCtx this
 
 /-- Proof irrelevant cut rule. -/
 theorem DerivableIn.cut {Γ Δ : Ctx Atom} {A B : Proposition Atom} :
@@ -249,22 +228,12 @@ def Theory.Derivation.subs {Γ Γ' Δ : Ctx Atom} {B : Proposition Atom}
       exact (Ds B h).weakCtx <| by grind
     case neg h =>
       exact ass <| by grind
-  | andI E E' => andI (E.subs Ds) (E'.subs Ds)
-  | andE₁ E => andE₁ <| E.subs Ds
-  | andE₂ E => andE₂ <| E.subs Ds
-  | orI₁ E => orI₁ <| E.subs Ds
-  | orI₂ E => orI₂ <| E.subs Ds
-  | @orE _ _ _ _ C C' _ E E' E'' .. => by
-    apply orE (E.subs Ds)
-    · rw [show insert C (Γ \ Γ' ∪ Δ) = (insert C Γ \ Γ') ∪ insert C Δ by grind]
-      exact E'.subs Ds |>.weakCtx (by grind)
-    · rw [show insert C' (Γ \ Γ' ∪ Δ) = (insert C' Γ \ Γ') ∪ insert C' Δ by grind]
-      exact E''.subs Ds |>.weakCtx (by grind)
-  | @implI _ _ _ A' _ _ E .. => by
-    apply implI
+  | @impI _ _ _ A' _ _ E .. => by
+    apply impI
     rw [show insert A' (Γ \ Γ' ∪ Δ) = (insert A' Γ \ Γ') ∪ insert A' Δ by grind]
     exact E.subs Ds |>.weakCtx (by grind)
-  | implE E E' => implE (E.subs Ds) (E'.subs Ds)
+  | impE E E' => impE (E.subs Ds) (E'.subs Ds)
+  | botE E => botE <| E.subs Ds
 
 /-- Transport a derivation along a substitution of atoms. -/
 def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
@@ -272,16 +241,9 @@ def Theory.Derivation.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decida
     T.Derivation Γ B → (T.subst f).Derivation (Γ.subst f) (B >>= f)
   | ax h => ax <| Set.mem_image_of_mem (· >>= f) h
   | ass h => ass <| Finset.mem_image_of_mem (· >>= f) h
-  | andI D E => andI (D.substAtom f) (E.substAtom f)
-  | andE₁ D => andE₁ (D.substAtom f)
-  | andE₂ D => andE₂ (D.substAtom f)
-  | orI₁ D => orI₁ (D.substAtom f)
-  | orI₂ D => orI₂ (D.substAtom f)
-  | orE D E E' => orE (D.substAtom f)
-    ((Finset.image_insert (· >>= f) _ _) ▸ E.substAtom f)
-    ((Finset.image_insert (· >>= f) _ _) ▸ E'.substAtom f)
-  | implI _ D => implI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f)
-  | implE D E => implE (D.substAtom f) (E.substAtom f)
+  | impI _ D => impI _ <| (Finset.image_insert (· >>= f) _ _) ▸ (D.substAtom f)
+  | impE D E => impE (D.substAtom f) (E.substAtom f)
+  | botE D => botE (D.substAtom f)
 
 theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [DecidableEq Atom']
     {T : Theory Atom}
@@ -292,12 +254,12 @@ theorem DerivableIn.substAtom {Atom Atom' : Type u} [DecidableEq Atom] [Decidabl
 /-! ### Properties of equivalence -/
 
 /-- A derivation of the canonical tautology. -/
-def Theory.derivationTop [Inhabited Atom] : T⇓(⊤ : Proposition Atom) :=
-  implI ∅ <| ass <| by grind
+def Theory.derivationTop : T⇓(⊤ : Proposition Atom) :=
+  impI ∅ <| ass <| by grind
 
-theorem derivableIn_top [Inhabited Atom] : DerivableIn T (⊤ : Proposition Atom) := ⟨derivationTop⟩
+theorem derivableIn_top : DerivableIn T (⊤ : Proposition Atom) := ⟨derivationTop⟩
 
-theorem derivable_iff_equiv_top [Inhabited Atom] (A : Proposition Atom) :
+theorem derivable_iff_equiv_top (A : Proposition Atom) :
     DerivableIn T A ↔ A ≡[T] ⊤ := by
   constructor <;> intro h
   · refine ⟨derivationTop.weakCtx <| by grind, ?_⟩
diff --git a/Cslib/Logics/Temporal/Syntax/BigConj.lean b/Cslib/Logics/Temporal/Syntax/BigConj.lean
new file mode 100644
index 000000000..92917a6e2
--- /dev/null
+++ b/Cslib/Logics/Temporal/Syntax/BigConj.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Brast-McKie
+-/
+
+module
+
+public import Cslib.Logics.Temporal.Syntax.Formula
+
+/-!
+# Big Conjunction over Lists of Formulas
+
+Defines `bigconj : List (Formula Atom) → Formula Atom` folding conjunction over a list,
+with base case `⊤` (represented as `¬⊥`, i.e. `Formula.neg Formula.bot`), plus the derived
+negation `negBigconj`.
+
+## Main Definitions
+
+- `bigconj : List (Formula Atom) → Formula Atom`
+- `negBigconj : List (Formula Atom) → Formula Atom`
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Temporal
+
+variable {Atom : Type u}
+
+/-- Big conjunction over a list of formulas: `bigconj [φ₁, …, φₙ] = φ₁ ∧ … ∧ φₙ`.
+    Base case: the empty list folds to `⊤`, represented as `¬⊥ = bot.imp bot`. -/
+def bigconj : List (Formula Atom) → Formula Atom
+  | []      => Formula.neg Formula.bot  -- `⊤` = `¬⊥`
+  | [φ]     => φ
+  | φ :: ψ :: rest => Formula.and φ (bigconj (ψ :: rest))
+
+/-- Negated big conjunction. -/
+def negBigconj (L : List (Formula Atom)) : Formula Atom := (bigconj L).neg
+
+@[simp] theorem bigconj_nil :
+    bigconj (Atom := Atom) [] = Formula.neg Formula.bot := rfl
+
+@[simp] theorem bigconj_singleton (φ : Formula Atom) :
+    bigconj [φ] = φ := rfl
+
+@[simp] theorem bigconj_cons_cons (φ ψ : Formula Atom) (rest : List (Formula Atom)) :
+    bigconj (φ :: ψ :: rest) = Formula.and φ (bigconj (ψ :: rest)) := rfl
+
+@[simp] theorem negBigconj_def (L : List (Formula Atom)) :
+    negBigconj L = (bigconj L).neg := rfl
+
+end Cslib.Logic.Temporal
diff --git a/Cslib/Logics/Temporal/Syntax/Context.lean b/Cslib/Logics/Temporal/Syntax/Context.lean
new file mode 100644
index 000000000..287ca4d8c
--- /dev/null
+++ b/Cslib/Logics/Temporal/Syntax/Context.lean
@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Brast-McKie
+-/
+
+module
+
+public import Cslib.Logics.Temporal.Syntax.Formula
+
+/-!
+# Context - Formula Lists for Proof Contexts
+
+This module defines the Context type used to represent assumptions in derivations.
+
+## Main Definitions
+
+- `Context`: Type alias for `List (Formula Atom)`
+- `Context.map`: Apply a transformation to all formulas in a context
+- `Context.isEmpty`: Check if a context is empty
+- `Context.singleton`: Create a context with a single formula
+
+## Main Results
+
+- Contexts inherit all list operations (membership, subset, append, etc.)
+- Map operation preserves structural properties (length, composition)
+- Map operation is equivalent to `List.map` for formulas
+
+## Implementation Notes
+
+- Context is simply `List (Formula Atom)`, leveraging Lean's built-in list operations
+- Parameterized over a generic `Atom` type for composability
+- The `map` operation is essential for temporal K inference rules
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Temporal
+
+/--
+Context type representing a list of formula assumptions.
+
+Used in the derivability relation `Γ ⊢ φ` where `Γ` is a context of assumptions.
+-/
+abbrev Context (Atom : Type u) := List (Formula Atom)
+
+namespace Context
+
+variable {Atom : Type u}
+
+/--
+Apply a transformation to all formulas in a context.
+
+This is used in inference rules like:
+- Temporal K: If `Γ.map allFuture ⊢ φ` then `Γ ⊢ allFuture φ`
+-/
+def map (f : Formula Atom → Formula Atom) : Context Atom → Context Atom := List.map f
+
+/-- Check if a context is empty. -/
+def isEmpty : Context Atom → Bool
+  | [] => true
+  | _ :: _ => false
+
+/-- Create a context containing a single formula. -/
+def singleton (φ : Formula Atom) : Context Atom := [φ]
+
+/-- Mapping a function over a context preserves length. -/
+theorem map_length (f : Formula Atom → Formula Atom) (Γ : Context Atom) :
+    (map f Γ).length = Γ.length := by
+  simp [map]
+
+/-- Mapping functions compose: `map f (map g Γ) = map (f ∘ g) Γ`. -/
+theorem map_comp (f g : Formula Atom → Formula Atom) (Γ : Context Atom) :
+    map f (map g Γ) = map (f ∘ g) Γ := by
+  simp [map, List.map_map]
+
+/-- Mapping the identity function leaves the context unchanged. -/
+theorem map_id (Γ : Context Atom) : map id Γ = Γ := by
+  simp [map]
+
+/-- Mapping over an empty context yields an empty context. -/
+theorem map_nil (f : Formula Atom → Formula Atom) : map f [] = [] := by
+  rfl
+
+/-- Mapping distributes over cons. -/
+theorem map_cons (f : Formula Atom → Formula Atom) (φ : Formula Atom) (Γ : Context Atom) :
+    map f (φ :: Γ) = f φ :: map f Γ := by
+  rfl
+
+/-- Mapping distributes over append. -/
+theorem map_append (f : Formula Atom → Formula Atom) (Γ Δ : Context Atom) :
+    map f (Γ ++ Δ) = map f Γ ++ map f Δ := by
+  simp [map]
+
+/-- Membership in mapped context comes from mapping a member. -/
+theorem mem_map_iff {f : Formula Atom → Formula Atom} {Γ : Context Atom}
+    {φ : Formula Atom} :
+    φ ∈ map f Γ ↔ ∃ ψ ∈ Γ, f ψ = φ := by
+  simp [map]
+
+/-- If `ψ ∈ Γ`, then `f ψ ∈ map f Γ`. -/
+theorem mem_map_of_mem {f : Formula Atom → Formula Atom} {Γ : Context Atom}
+    {ψ : Formula Atom} (h : ψ ∈ Γ) : f ψ ∈ map f Γ := by
+  rw [mem_map_iff]
+  exact ⟨ψ, h, rfl⟩
+
+/-- Empty context has no members. -/
+theorem not_mem_nil (φ : Formula Atom) : φ ∉ ([] : Context Atom) := by
+  simp
+
+/-- Singleton context contains exactly one formula. -/
+theorem mem_singleton_iff {φ ψ : Formula Atom} :
+    φ ∈ singleton ψ ↔ φ = ψ := by
+  simp [singleton]
+
+/-- isEmpty is true iff the context equals []. -/
+theorem isEmpty_iff_eq_nil (Γ : Context Atom) : isEmpty Γ = true ↔ Γ = [] := by
+  cases Γ with
+  | nil => simp [isEmpty]
+  | cons _ _ => simp [isEmpty]
+
+/-- A non-empty context has at least one element. -/
+theorem exists_mem_of_ne_nil {Γ : Context Atom} (h : Γ ≠ []) :
+    ∃ φ, φ ∈ Γ := by
+  cases Γ with
+  | nil => contradiction
+  | cons φ _ => exact ⟨φ, List.mem_cons_self ..⟩
+
+end Context
+
+end Cslib.Logic.Temporal
diff --git a/Cslib/Logics/Temporal/Syntax/Formula.lean b/Cslib/Logics/Temporal/Syntax/Formula.lean
new file mode 100644
index 000000000..3e3b36a47
--- /dev/null
+++ b/Cslib/Logics/Temporal/Syntax/Formula.lean
@@ -0,0 +1,580 @@
+/-
+Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Brast-McKie
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Logic.Connectives
+public import Mathlib.Logic.Encodable.Basic
+public import Mathlib.Logic.Denumerable
+public import Mathlib.Data.Finset.Basic
+
+/-! # Temporal Logic Formula
+
+This module defines the formula type for temporal logic with primitives
+`{atom, bot, imp, untl, snce}`. The `untl` (until) and `snce` (since) operators
+are the basic temporal modalities from which all other temporal operators
+(globally, eventually, etc.) are derived.
+
+## Derived Temporal Operators
+
+The derived operators use the Burgess convention: in `untl event guard` and `snce event guard`,
+the first argument is the **event** (holds at the witness point) and the second is the **guard**
+(holds at all intermediate points). This matches the abstract typeclass expansion in `Axioms.lean`.
+
+- `someFuture φ` (F φ): `φ U ⊤` — φ holds at some future point (Burgess: `untl φ ⊤`)
+- `allFuture φ` (G φ): `¬F ¬φ` — φ holds at all future points
+- `somePast φ` (P φ): `φ S ⊤` — φ held at some past point (Burgess: `snce φ ⊤`)
+- `allPast φ` (H φ): `¬P ¬φ` — φ held at all past points
+
+## References
+
+* [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968]
+* [D. Gabbay et al., *On the Temporal Analysis of Fairness*][GabbayPnueliShelahStavi1980]
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Temporal
+
+/-- Temporal logic formula type. Primitives: atoms, falsum, implication, until, and since. -/
+inductive Formula (Atom : Type u) : Type u where
+  /-- Atomic proposition. -/
+  | atom (p : Atom)
+  /-- Falsum / bottom. -/
+  | bot
+  /-- Implication. -/
+  | imp (φ₁ φ₂ : Formula Atom)
+  /-- Until temporal operator: φ₁ U φ₂. -/
+  | untl (φ₁ φ₂ : Formula Atom)
+  /-- Since temporal operator: φ₁ S φ₂. -/
+  | snce (φ₁ φ₂ : Formula Atom)
+deriving DecidableEq, BEq
+
+/-- Negation: ¬φ := φ → ⊥ -/
+abbrev Formula.neg (φ : Formula Atom) : Formula Atom := .imp φ .bot
+
+/-- Verum / top: ⊤ := ⊥ → ⊥ -/
+abbrev Formula.top : Formula Atom := .imp .bot .bot
+
+/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/
+abbrev Formula.or (φ₁ φ₂ : Formula Atom) : Formula Atom :=
+  .imp (.imp φ₁ .bot) φ₂
+
+/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/
+abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom :=
+  .imp (.imp φ₁ (.imp φ₂ .bot)) .bot
+
+/-- Biconditional: φ₁ ↔ φ₂ := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -/
+abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom :=
+  (φ₁.imp φ₂).and (φ₂.imp φ₁)
+
+/-- Some future (eventually): F φ := φ U ⊤.
+    Note: uses Burgess convention where `untl event guard` — φ is the event (holds at witness),
+    ⊤ is the trivial guard. Equivalent to standard LTL `F φ = ⊤ U φ` semantically. -/
+abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom :=
+  .untl φ .top
+
+/-- All future (globally): G φ := ¬F ¬φ -/
+abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom :=
+  .neg (.someFuture (.neg φ))
+
+/-- Some past: P φ := φ S ⊤.
+    Note: uses Burgess convention where `snce event guard` — φ is the event (holds at witness),
+    ⊤ is the trivial guard. Equivalent to standard LTL `P φ = ⊤ S φ` semantically. -/
+abbrev Formula.somePast (φ : Formula Atom) : Formula Atom :=
+  .snce φ .top
+
+/-- All past (historically): H φ := ¬P ¬φ -/
+abbrev Formula.allPast (φ : Formula Atom) : Formula Atom :=
+  .neg (.somePast (.neg φ))
+
+@[inherit_doc] scoped prefix:40 "¬" => Formula.neg
+@[inherit_doc] scoped infix:36 " ∧ " => Formula.and
+@[inherit_doc] scoped infix:35 " ∨ " => Formula.or
+@[inherit_doc] scoped infix:30 " → " => Formula.imp
+@[inherit_doc] scoped infix:30 " ↔ " => Formula.iff
+@[inherit_doc] scoped infix:40 " U " => Formula.untl
+@[inherit_doc] scoped infix:40 " S " => Formula.snce
+@[inherit_doc] scoped prefix:40 "𝐅" => Formula.someFuture
+@[inherit_doc] scoped prefix:40 "𝐆" => Formula.allFuture
+@[inherit_doc] scoped prefix:40 "𝐏" => Formula.somePast
+@[inherit_doc] scoped prefix:40 "𝐇" => Formula.allPast
+
+/-- Register `Temporal.Formula` as an instance of `TemporalConnectives`. -/
+instance : TemporalConnectives (Formula Atom) where
+  bot := .bot
+  imp := .imp
+  untl := .untl
+  snce := .snce
+
+instance : Bot (Formula Atom) := ⟨.bot⟩
+instance : Top (Formula Atom) := ⟨.top⟩
+
+end Cslib.Logic.Temporal
+
+@[expose] public section
+
+/-! ## Structural Properties and Derived Operators
+
+Extensions to `Temporal.Formula` providing:
+- Countable, Infinite, Denumerable instances
+- BEq reflexivity and lawfulness
+- Complexity measure
+- Temporal depth and implication count
+- Additional derived temporal operators
+- Swap temporal duality transformation
+- Atom collection function
+- Positive hypothesis predicate
+-/
+
+namespace Cslib.Logic.Temporal
+
+/-! ### Countable, Infinite, Denumerable Instances -/
+
+section Countability
+
+variable {Atom : Type*}
+
+/-- `Formula.atom` is injective. -/
+theorem Formula.atom_injective : Function.Injective (Formula.atom (Atom := Atom)) := by
+  intro a b h
+  injection h
+
+namespace Formula
+
+/-- Encode a formula into a natural number using Cantor pairing.
+    Used to establish countability of formulas. -/
+noncomputable def encodeNat [Encodable Atom] : Formula Atom → ℕ
+  | .atom a => Nat.pair 0 (Encodable.encode a)
+  | .bot => Nat.pair 1 0
+  | .imp φ ψ => Nat.pair 2 (Nat.pair φ.encodeNat ψ.encodeNat)
+  | .untl φ ψ => Nat.pair 3 (Nat.pair φ.encodeNat ψ.encodeNat)
+  | .snce φ ψ => Nat.pair 4 (Nat.pair φ.encodeNat ψ.encodeNat)
+
+theorem nat_pair_inj {a b c d : ℕ} (h : Nat.pair a b = Nat.pair c d) :
+    a = c ∧ b = d := by
+  have := congr_arg Nat.unpair h
+  simp only [Nat.unpair_pair] at this
+  exact Prod.mk.inj this
+
+/-- The encoding is injective. -/
+theorem encodeNat_injective [Encodable Atom] :
+    Function.Injective (encodeNat (Atom := Atom)) := by
+  intro φ ψ h
+  induction φ generalizing ψ with
+  | atom a =>
+    cases ψ with
+    | atom b =>
+      have ⟨_, h2⟩ := nat_pair_inj h
+      exact congrArg Formula.atom (Encodable.encode_injective h2)
+    | bot => exact absurd (nat_pair_inj h).1 (by decide)
+    | imp _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | untl _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | snce _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+  | bot =>
+    cases ψ with
+    | bot => rfl
+    | atom _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | imp _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | untl _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | snce _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+  | imp a b iha ihb =>
+    cases ψ with
+    | imp c d =>
+      have ⟨_, h2⟩ := nat_pair_inj h
+      have ⟨h3, h4⟩ := nat_pair_inj h2
+      exact congrArg₂ Formula.imp (iha h3) (ihb h4)
+    | atom _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | bot => exact absurd (nat_pair_inj h).1 (by decide)
+    | untl _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | snce _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+  | untl a b iha ihb =>
+    cases ψ with
+    | untl c d =>
+      have ⟨_, h2⟩ := nat_pair_inj h
+      have ⟨h3, h4⟩ := nat_pair_inj h2
+      exact congrArg₂ Formula.untl (iha h3) (ihb h4)
+    | atom _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | bot => exact absurd (nat_pair_inj h).1 (by decide)
+    | imp _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | snce _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+  | snce a b iha ihb =>
+    cases ψ with
+    | snce c d =>
+      have ⟨_, h2⟩ := nat_pair_inj h
+      have ⟨h3, h4⟩ := nat_pair_inj h2
+      exact congrArg₂ Formula.snce (iha h3) (ihb h4)
+    | atom _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | bot => exact absurd (nat_pair_inj h).1 (by decide)
+    | imp _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+    | untl _ _ => exact absurd (nat_pair_inj h).1 (by decide)
+
+end Formula
+
+/-- Formula is countable when Atom is countable. -/
+instance [Countable Atom] : Countable (Formula Atom) := by
+  have : Encodable Atom := Encodable.ofCountable Atom
+  exact Countable.mk ⟨Formula.encodeNat, Formula.encodeNat_injective⟩
+
+/-- Formula is infinite when Atom is infinite (via injection from Atom). -/
+instance [Infinite Atom] : Infinite (Formula Atom) :=
+  Infinite.of_injective Formula.atom Formula.atom_injective
+
+/-- Formula is denumerable when Atom is both countable and infinite. -/
+noncomputable instance [Countable Atom] [Infinite Atom] :
+    Denumerable (Formula Atom) :=
+  Classical.choice (nonempty_denumerable (Formula Atom))
+
+end Countability
+
+/-! ### BEq Reflexivity and Lawfulness -/
+
+section BEqLaws
+
+variable {Atom : Type*} [BEq Atom]
+
+namespace Formula
+
+/-- Helper: BEq on imp reduces to component BEq. -/
+theorem beq_imp_eq (a b c d : Formula Atom) :
+    (imp a b == imp c d) = ((a == c) && (b == d)) := rfl
+
+/-- Helper: BEq on untl reduces to component BEq. -/
+theorem beq_untl_eq (a b c d : Formula Atom) :
+    (untl a b == untl c d) = ((a == c) && (b == d)) := rfl
+
+/-- Helper: BEq on snce reduces to component BEq. -/
+theorem beq_snce_eq (a b c d : Formula Atom) :
+    (snce a b == snce c d) = ((a == c) && (b == d)) := rfl
+
+/-- BEq on Formula is reflexive. -/
+theorem beq_refl [ReflBEq Atom] (φ : Formula Atom) : (φ == φ) = true := by
+  induction φ with
+  | atom p => exact @beq_self_eq_true Atom _ _ p
+  | bot => rfl
+  | imp a b iha ihb => rw [beq_imp_eq, iha, ihb]; rfl
+  | untl a b iha ihb => rw [beq_untl_eq, iha, ihb]; rfl
+  | snce a b iha ihb => rw [beq_snce_eq, iha, ihb]; rfl
+
+/-- BEq on Formula is sound: if `φ == ψ = true` then `φ = ψ`. -/
+theorem eq_of_beq [LawfulBEq Atom] {φ ψ : Formula Atom}
+    (h : (φ == ψ) = true) : φ = ψ := by
+  induction φ generalizing ψ with
+  | atom p =>
+    match ψ with
+    | atom q =>
+      have heq : (atom p == atom q) = (p == q) := rfl
+      rw [heq] at h; exact congrArg atom (beq_iff_eq.mp h)
+    | bot | imp _ _ | untl _ _ | snce _ _ => exact nomatch h
+  | bot =>
+    match ψ with
+    | bot => rfl
+    | atom _ | imp _ _ | untl _ _ | snce _ _ => exact nomatch h
+  | imp a b iha ihb =>
+    match ψ with
+    | imp c d =>
+      have heq : (imp a b == imp c d) = ((a == c) && (b == d)) := rfl
+      rw [heq] at h; simp only [Bool.and_eq_true] at h
+      exact congrArg₂ imp (iha h.1) (ihb h.2)
+    | atom _ | bot | untl _ _ | snce _ _ => exact nomatch h
+  | untl a b iha ihb =>
+    match ψ with
+    | untl c d =>
+      have heq : (untl a b == untl c d) = ((a == c) && (b == d)) := rfl
+      rw [heq] at h; simp only [Bool.and_eq_true] at h
+      exact congrArg₂ untl (iha h.1) (ihb h.2)
+    | atom _ | bot | imp _ _ | snce _ _ => exact nomatch h
+  | snce a b iha ihb =>
+    match ψ with
+    | snce c d =>
+      have heq : (snce a b == snce c d) = ((a == c) && (b == d)) := rfl
+      rw [heq] at h; simp only [Bool.and_eq_true] at h
+      exact congrArg₂ snce (iha h.1) (ihb h.2)
+    | atom _ | bot | imp _ _ | untl _ _ => exact nomatch h
+
+end Formula
+
+instance [ReflBEq Atom] : ReflBEq (Formula Atom) where
+  rfl := Formula.beq_refl _
+
+instance [LawfulBEq Atom] : LawfulBEq (Formula Atom) where
+  eq_of_beq := Formula.eq_of_beq
+  rfl := Formula.beq_refl _
+
+end BEqLaws
+
+/-! ### Complexity Measure -/
+
+namespace Formula
+
+variable {Atom : Type*}
+
+/--
+Structural complexity of a formula (number of connectives + 1).
+
+Pattern-aware cases for derived temporal operators (Burgess convention: `untl event guard`):
+- `F(φ) = φ U ⊤` → treated as overhead 1, not 4
+- `P(φ) = φ S ⊤` → treated as overhead 1, not 4
+- `G(φ) = ¬F(¬φ)` → treated as overhead 1, not 8
+- `H(φ) = ¬P(¬φ)` → treated as overhead 1, not 8
+- `next(φ) = ⊥ U φ` → treated as overhead 1
+- `prev(φ) = ⊥ S φ` → treated as overhead 1
+- `R(φ, ψ) = ¬(¬ψ U ¬φ)` → treated as overhead 1
+- `T(φ, ψ) = ¬(¬ψ S ¬φ)` → treated as overhead 1
+-/
+def complexity : Formula Atom → Nat
+  | .atom _ => 1
+  | .bot => 1
+  -- G(φ) = imp (untl (imp φ bot) (imp bot bot)) bot  [¬(¬φ U ⊤) in Burgess]
+  | .imp (.untl (.imp φ .bot) (.imp .bot .bot)) .bot => 1 + complexity φ
+  -- H(φ) = imp (snce (imp φ bot) (imp bot bot)) bot  [¬(¬φ S ⊤) in Burgess]
+  | .imp (.snce (.imp φ .bot) (.imp .bot .bot)) .bot => 1 + complexity φ
+  -- R(φ, ψ) = release = imp (untl (imp ψ bot) (imp φ bot)) bot  [¬(¬ψ_event U ¬φ_guard)]
+  | .imp (.untl (.imp ψ .bot) (.imp φ .bot)) .bot =>
+    1 + complexity φ + complexity ψ
+  -- T(φ, ψ) = trigger = imp (snce (imp ψ bot) (imp φ bot)) bot  [¬(¬ψ_event S ¬φ_guard)]
+  | .imp (.snce (.imp ψ .bot) (.imp φ .bot)) .bot =>
+    1 + complexity φ + complexity ψ
+  -- generic imp
+  | .imp φ ψ => 1 + complexity φ + complexity ψ
+  -- F(φ) = untl φ (imp bot bot)  [φ U ⊤ in Burgess]
+  | .untl φ (.imp .bot .bot) => 1 + complexity φ
+  -- next(φ) = untl φ bot  [φ U ⊥ in Burgess: guard ⊥ impossible, forces immediate step]
+  | .untl φ .bot => 1 + complexity φ
+  -- generic untl
+  | .untl φ ψ => 1 + complexity φ + complexity ψ
+  -- P(φ) = snce φ (imp bot bot)  [φ S ⊤ in Burgess]
+  | .snce φ (.imp .bot .bot) => 1 + complexity φ
+  -- prev(φ) = snce φ bot  [φ S ⊥ in Burgess: guard ⊥ impossible, forces immediate step]
+  | .snce φ .bot => 1 + complexity φ
+  -- generic snce
+  | .snce φ ψ => 1 + complexity φ + complexity ψ
+
+/-! ### Temporal Depth -/
+
+/--
+Temporal depth: nesting level of temporal operators.
+
+Computes the maximum nesting depth of temporal operators (U, S) in a formula.
+-/
+def temporalDepth : Formula Atom → Nat
+  | .atom _ => 0
+  | .bot => 0
+  | .imp φ ψ => max φ.temporalDepth ψ.temporalDepth
+  | .untl φ ψ => 1 + max φ.temporalDepth ψ.temporalDepth
+  | .snce φ ψ => 1 + max φ.temporalDepth ψ.temporalDepth
+
+/--
+Count implication operators in a formula.
+
+Useful for heuristic scoring in proof search.
+-/
+def countImplications : Formula Atom → Nat
+  | .atom _ => 0
+  | .bot => 0
+  | .imp φ ψ => 1 + φ.countImplications + ψ.countImplications
+  | .untl φ ψ => φ.countImplications + ψ.countImplications
+  | .snce φ ψ => φ.countImplications + ψ.countImplications
+
+/-! ### Additional Derived Temporal Operators -/
+
+/-- Next-step operator: X(φ) = φ U ⊥.
+    X(φ) at t means φ holds at t+1. Uses Burgess convention: φ is the event,
+    ⊥ is the guard (impossible), forcing the witness to be immediately next. -/
+def next (φ : Formula Atom) : Formula Atom := .untl φ .bot
+
+/-- Previous-step operator: Y(φ) = φ S ⊥.
+    Y(φ) at t means φ holds at t-1. Uses Burgess convention: φ is the event,
+    ⊥ is the guard (impossible), forcing the witness to be immediately previous. -/
+def prev (φ : Formula Atom) : Formula Atom := .snce φ .bot
+
+/-- Derived reflexive future operator: G'φ := φ ∧ Gφ. -/
+def weakFuture (φ : Formula Atom) : Formula Atom :=
+  φ ∧ 𝐆φ
+
+/-- Derived reflexive past operator: H'φ := φ ∧ Hφ. -/
+def weakPast (φ : Formula Atom) : Formula Atom :=
+  φ ∧ 𝐇φ
+
+/-- Temporal 'always' operator (△φ): Hφ ∧ φ ∧ Gφ.
+    φ holds at all times (past, present, and future). -/
+def always (φ : Formula Atom) : Formula Atom :=
+  𝐇φ ∧ (φ ∧ 𝐆φ)
+
+/-- Temporal 'sometimes' operator (▽φ): ¬△¬φ.
+    φ holds at some time (past, present, or future). -/
+def sometimes (φ : Formula Atom) : Formula Atom :=
+  ¬(always (¬φ))
+
+/-- Release operator R(φ, ψ) := ¬(¬φ U ¬ψ). Dual of Until.
+    In Burgess convention: `untl (neg ψ) (neg φ)` where ¬ψ is the event and ¬φ is the guard,
+    corresponding to `¬φ U ¬ψ` in standard LTL notation. -/
+def release (φ ψ : Formula Atom) : Formula Atom :=
+  ¬((¬ψ) U (¬φ))
+
+/-- Trigger operator T(φ, ψ) := ¬(¬φ S ¬ψ). Dual of Since (past analog of Release).
+    In Burgess convention: `snce (neg ψ) (neg φ)` where ¬ψ is the event and ¬φ is the guard,
+    corresponding to `¬φ S ¬ψ` in standard LTL notation. -/
+def trigger (φ ψ : Formula Atom) : Formula Atom :=
+  ¬((¬ψ) S (¬φ))
+
+/-- Weak Until operator W(φ, ψ) := (φ U ψ) ∨ G(φ). Until without the liveness requirement. -/
+def weakUntil (φ ψ : Formula Atom) : Formula Atom :=
+  (φ U ψ) ∨ 𝐆φ
+
+/-- Weak Since operator WS(φ, ψ) := (φ S ψ) ∨ H(φ). Since without the liveness requirement. -/
+def weakSince (φ ψ : Formula Atom) : Formula Atom :=
+  (φ S ψ) ∨ 𝐇φ
+
+/-- Strong Release operator M(φ, ψ) := ψ U (ψ ∧ φ). Dual of weak until.
+    In Burgess convention: `untl (and ψ φ) ψ` where ψ∧φ is the event and ψ is the guard. -/
+def strongRelease (φ ψ : Formula Atom) : Formula Atom :=
+  (ψ ∧ φ) U ψ
+
+/-- Strong Trigger operator ST(φ, ψ) := ψ S (ψ ∧ φ). Past dual of strong release.
+    In Burgess convention: `snce (and ψ φ) ψ` where ψ∧φ is the event and ψ is the guard. -/
+def strongTrigger (φ ψ : Formula Atom) : Formula Atom :=
+  (ψ ∧ φ) S ψ
+
+/-- Notation for temporal 'always' operator using upward triangle. -/
+scoped prefix:80 "△" => Formula.always
+
+/-- Notation for temporal 'sometimes' operator using downward triangle. -/
+scoped prefix:80 "▽" => Formula.sometimes
+
+/-! ### Swap Temporal Duality -/
+
+/--
+Swap temporal operators (past ↔ future) in a formula.
+
+This transformation is used in the temporal duality inference rule (TD):
+if `⊢ φ` then `⊢ swapTemporal φ`.
+-/
+def swapTemporal : Formula Atom → Formula Atom
+  | .atom s => .atom s
+  | .bot => .bot
+  | .imp φ ψ => .imp (swapTemporal φ) (swapTemporal ψ)
+  | .untl φ ψ => .snce (swapTemporal φ) (swapTemporal ψ)
+  | .snce φ ψ => .untl (swapTemporal φ) (swapTemporal ψ)
+
+/-- swapTemporal is an involution (applying it twice gives identity). -/
+theorem swapTemporal_involution (φ : Formula Atom) :
+    φ.swapTemporal.swapTemporal = φ := by
+  induction φ with
+  | atom _ => rfl
+  | bot => rfl
+  | imp _ _ ihp ihq => simp only [swapTemporal, ihp, ihq]
+  | untl _ _ ih1 ih2 => simp only [swapTemporal, ih1, ih2]
+  | snce _ _ ih1 ih2 => simp only [swapTemporal, ih1, ih2]
+
+/-- swapTemporal distributes over negation: swap(¬φ) = ¬(swap φ). -/
+theorem swapTemporal_neg (φ : Formula Atom) :
+    (Formula.neg φ).swapTemporal = Formula.neg φ.swapTemporal := by
+  simp only [Formula.neg, swapTemporal]
+
+/-- swapTemporal exchanges someFuture and somePast: swap(Fφ) = P(swap φ). -/
+@[simp]
+theorem swapTemporal_someFuture (φ : Formula Atom) :
+    (Formula.someFuture φ).swapTemporal = Formula.somePast φ.swapTemporal := by
+  simp only [Formula.somePast, Formula.top, swapTemporal]
+
+/-- swapTemporal exchanges somePast and someFuture: swap(Pφ) = F(swap φ). -/
+@[simp]
+theorem swapTemporal_somePast (φ : Formula Atom) :
+    (Formula.somePast φ).swapTemporal = Formula.someFuture φ.swapTemporal := by
+  simp only [Formula.someFuture, Formula.top, swapTemporal]
+
+/-- swapTemporal exchanges allFuture and allPast: swap(Gφ) = H(swap φ). -/
+@[simp]
+theorem swapTemporal_allFuture (φ : Formula Atom) :
+    (Formula.allFuture φ).swapTemporal = Formula.allPast φ.swapTemporal := by
+  simp only [Formula.allPast, swapTemporal]
+
+/-- swapTemporal exchanges allPast and allFuture: swap(Hφ) = G(swap φ). -/
+@[simp]
+theorem swapTemporal_allPast (φ : Formula Atom) :
+    (Formula.allPast φ).swapTemporal = Formula.allFuture φ.swapTemporal := by
+  simp only [Formula.allFuture, swapTemporal]
+
+/-- swapTemporal distributes over next/prev: swap(X(φ)) = Y(swap(φ)). -/
+theorem swapTemporal_next (φ : Formula Atom) :
+    (next φ).swapTemporal = prev φ.swapTemporal := by
+  simp [next, prev, swapTemporal]
+
+/-- swapTemporal distributes over prev/next: swap(Y(φ)) = X(swap(φ)). -/
+theorem swapTemporal_prev (φ : Formula Atom) :
+    (prev φ).swapTemporal = next φ.swapTemporal := by
+  simp [prev, next, swapTemporal]
+
+/-- swapTemporal distributes over strongRelease: swap(M(φ,ψ)) = ST(swap φ, swap ψ). -/
+theorem swapTemporal_strongRelease (φ ψ : Formula Atom) :
+    (strongRelease φ ψ).swapTemporal =
+      strongTrigger φ.swapTemporal ψ.swapTemporal := by
+  simp [strongRelease, strongTrigger, Formula.and, swapTemporal]
+
+/-- swapTemporal distributes over strongTrigger: swap(ST(φ,ψ)) = M(swap φ, swap ψ). -/
+theorem swapTemporal_strongTrigger (φ ψ : Formula Atom) :
+    (strongTrigger φ ψ).swapTemporal =
+      strongRelease φ.swapTemporal ψ.swapTemporal := by
+  simp [strongRelease, strongTrigger, Formula.and, swapTemporal]
+
+/-! ### Positive Hypothesis Predicate -/
+
+/--
+Whether a formula requires the single-family/single-time hypotheses.
+All non-imp formulas need these for propagation.
+-/
+def needsPositiveHypotheses : Formula Atom → Bool
+  | .imp _ _ => false
+  | _ => true
+
+@[simp] lemma needsPositiveHypotheses_atom (s : Atom) :
+    (Formula.atom s).needsPositiveHypotheses = true := rfl
+
+@[simp] lemma needsPositiveHypotheses_bot :
+    (Formula.bot : Formula Atom).needsPositiveHypotheses = true := rfl
+
+@[simp] lemma needsPositiveHypotheses_untl (p q : Formula Atom) :
+    (Formula.untl p q).needsPositiveHypotheses = true := rfl
+
+@[simp] lemma needsPositiveHypotheses_snce (p q : Formula Atom) :
+    (Formula.snce p q).needsPositiveHypotheses = true := rfl
+
+@[simp] lemma needsPositiveHypotheses_imp (p q : Formula Atom) :
+    (Formula.imp p q).needsPositiveHypotheses = false := rfl
+
+/-! ### Propositional Atoms -/
+
+section Atoms
+
+variable [DecidableEq Atom]
+
+/-- The set of propositional atoms appearing in a formula. -/
+def atoms : Formula Atom → Finset Atom
+  | .atom s => {s}
+  | .bot => ∅
+  | .imp φ ψ => atoms φ ∪ atoms ψ
+  | .untl φ ψ => atoms φ ∪ atoms ψ
+  | .snce φ ψ => atoms φ ∪ atoms ψ
+
+/-- swapTemporal preserves atoms: swapping past/future does not change which atoms appear. -/
+theorem atoms_swapTemporal (φ : Formula Atom) :
+    atoms (swapTemporal φ) = atoms φ := by
+  induction φ with
+  | atom _ => rfl
+  | bot => rfl
+  | imp _ _ ih1 ih2 => simp only [swapTemporal, atoms]; rw [ih1, ih2]
+  | untl _ _ ih1 ih2 => simp only [swapTemporal, atoms]; rw [ih1, ih2]
+  | snce _ _ ih1 ih2 => simp only [swapTemporal, atoms]; rw [ih1, ih2]
+
+end Atoms
+
+end Formula
+
+end Cslib.Logic.Temporal
+
+end
diff --git a/Cslib/Logics/Temporal/Syntax/Subformulas.lean b/Cslib/Logics/Temporal/Syntax/Subformulas.lean
new file mode 100644
index 000000000..bfd32f5bd
--- /dev/null
+++ b/Cslib/Logics/Temporal/Syntax/Subformulas.lean
@@ -0,0 +1,218 @@
+/-
+Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Benjamin Brast-McKie
+-/
+
+module
+
+public import Cslib.Logics.Temporal.Syntax.Formula
+import Mathlib.Data.List.Basic
+
+/-!
+# Subformula Definitions for Temporal Logic
+
+This module provides the subformula closure for temporal logic formulas.
+These definitions are used in the finite model property proof and
+decidability procedures.
+
+## Main Definitions
+
+- `Formula.subformulas`: Collect all subformulas of a formula (including itself)
+- `Formula.subformulaCount`: Count of distinct subformulas
+
+## Main Results
+
+- `Formula.self_mem_subformulas`: A formula is in its own subformula list
+- `Formula.subformulas_trans`: Subformula relation is transitive
+- Membership lemmas for each constructor
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Temporal
+
+namespace Formula
+
+variable {Atom : Type*}
+
+/--
+Collect all subformulas of a formula (including the formula itself).
+
+This is used to bound the size of finite models and tableaux.
+The subformula property ensures that expansion only produces
+formulas from the subformula closure.
+-/
+def subformulas : Formula Atom → List (Formula Atom)
+  | φ@(.atom _) => [φ]
+  | φ@.bot => [φ]
+  | φ@(.imp ψ χ) => φ :: (subformulas ψ ++ subformulas χ)
+  | φ@(.untl ψ χ) => φ :: (subformulas ψ ++ subformulas χ)
+  | φ@(.snce ψ χ) => φ :: (subformulas ψ ++ subformulas χ)
+
+/-- Count of distinct subformulas (used for termination). -/
+def subformulaCount [DecidableEq (Formula Atom)] (φ : Formula Atom) : Nat :=
+  (subformulas φ).eraseDups.length
+
+/-- Subformulas include the formula itself. -/
+theorem self_mem_subformulas (φ : Formula Atom) : φ ∈ subformulas φ := by
+  cases φ <;> simp [subformulas]
+
+/-- Subformulas of imp include the left component. -/
+theorem imp_left_mem_subformulas (ψ χ : Formula Atom) :
+    ψ ∈ subformulas (.imp ψ χ) := by
+  simp only [subformulas, List.mem_cons, List.mem_append]
+  right
+  left
+  exact self_mem_subformulas ψ
+
+/-- Subformulas of imp include the right component. -/
+theorem imp_right_mem_subformulas (ψ χ : Formula Atom) :
+    χ ∈ subformulas (.imp ψ χ) := by
+  simp only [subformulas, List.mem_cons, List.mem_append]
+  right
+  right
+  exact self_mem_subformulas χ
+
+/-- Subformulas of allPast include the inner formula. -/
+theorem allPast_inner_mem_subformulas (ψ : Formula Atom) :
+    ψ ∈ subformulas (𝐇ψ) := by
+  -- allPast ψ = imp (snce (imp ψ bot) (imp bot bot)) bot  [¬P(¬ψ) = ¬(¬ψ S ⊤) in Burgess]
+  simp only [subformulas, List.mem_cons, List.mem_append]
+  right; left; right; left; right; left
+  exact self_mem_subformulas ψ
+
+/-- Subformulas of allFuture include the inner formula. -/
+theorem allFuture_inner_mem_subformulas (ψ : Formula Atom) :
+    ψ ∈ subformulas (𝐆ψ) := by
+  -- allFuture ψ = imp (untl (imp ψ bot) (imp bot bot)) bot  [¬F(¬ψ) = ¬(¬ψ U ⊤) in Burgess]
+  simp only [subformulas, List.mem_cons, List.mem_append]
+  right; left; right; left; right; left
+  exact self_mem_subformulas ψ
+
+/--
+Transitivity of the subformula relation.
+
+If chi is a subformula of psi, and psi is a subformula of phi,
+then chi is a subformula of phi.
+-/
+theorem subformulas_trans {chi psi phi : Formula Atom}
+    (h1 : chi ∈ subformulas psi) (h2 : psi ∈ subformulas phi) :
+    chi ∈ subformulas phi := by
+  induction phi with
+  | atom p =>
+    simp only [subformulas, List.mem_singleton] at h2
+    subst h2
+    exact h1
+  | bot =>
+    simp only [subformulas, List.mem_singleton] at h2
+    subst h2
+    exact h1
+  | imp a b iha ihb =>
+    simp only [subformulas, List.mem_cons, List.mem_append] at h2
+    rcases h2 with rfl | ha | hb
+    · exact h1
+    · simp only [subformulas, List.mem_cons, List.mem_append]
+      right; left
+      exact iha ha
+    · simp only [subformulas, List.mem_cons, List.mem_append]
+      right; right
+      exact ihb hb
+  | untl a b iha ihb =>
+    simp only [subformulas, List.mem_cons, List.mem_append] at h2
+    rcases h2 with rfl | ha | hb
+    · exact h1
+    · simp only [subformulas, List.mem_cons, List.mem_append]
+      right; left
+      exact iha ha
+    · simp only [subformulas, List.mem_cons, List.mem_append]
+      right; right
+      exact ihb hb
+  | snce a b iha ihb =>
+    simp only [subformulas, List.mem_cons, List.mem_append] at h2
+    rcases h2 with rfl | ha | hb
+    · exact h1
+    · simp only [subformulas, List.mem_cons, List.mem_append]
+      right; left
+      exact iha ha
+    · simp only [subformulas, List.mem_cons, List.mem_append]
+      right; right
+      exact ihb hb
+
+/-- Left side of implication is in subformulas of the implication. -/
+theorem mem_subformulas_of_imp_left {ψ χ phi : Formula Atom}
+    (h : (ψ → χ) ∈ subformulas phi) : ψ ∈ subformulas phi := by
+  have h_left : ψ ∈ subformulas (ψ → χ) := imp_left_mem_subformulas ψ χ
+  exact subformulas_trans h_left h
+
+/-- Right side of implication is in subformulas of the implication. -/
+theorem mem_subformulas_of_imp_right {ψ χ phi : Formula Atom}
+    (h : (ψ → χ) ∈ subformulas phi) : χ ∈ subformulas phi := by
+  have h_right : χ ∈ subformulas (ψ → χ) := imp_right_mem_subformulas ψ χ
+  exact subformulas_trans h_right h
+
+/-- Inner formula of allPast is in subformulas. -/
+theorem mem_subformulas_of_allPast {ψ phi : Formula Atom}
+    (h : (𝐇ψ) ∈ subformulas phi) : ψ ∈ subformulas phi := by
+  have h_inner : ψ ∈ subformulas (𝐇ψ) :=
+    allPast_inner_mem_subformulas ψ
+  exact subformulas_trans h_inner h
+
+/-- Inner formula of allFuture is in subformulas. -/
+theorem mem_subformulas_of_allFuture {ψ phi : Formula Atom}
+    (h : (𝐆ψ) ∈ subformulas phi) : ψ ∈ subformulas phi := by
+  have h_inner : ψ ∈ subformulas (𝐆ψ) :=
+    allFuture_inner_mem_subformulas ψ
+  exact subformulas_trans h_inner h
+
+/-- Subformulas of untl include the left component. -/
+theorem untl_left_mem_subformulas (ψ χ : Formula Atom) :
+    ψ ∈ subformulas (.untl ψ χ) := by
+  simp only [subformulas, List.mem_cons, List.mem_append]
+  right; left
+  exact self_mem_subformulas ψ
+
+/-- Subformulas of untl include the right component. -/
+theorem untl_right_mem_subformulas (ψ χ : Formula Atom) :
+    χ ∈ subformulas (.untl ψ χ) := by
+  simp only [subformulas, List.mem_cons, List.mem_append]
+  right; right
+  exact self_mem_subformulas χ
+
+/-- Subformulas of snce include the left component. -/
+theorem snce_left_mem_subformulas (ψ χ : Formula Atom) :
+    ψ ∈ subformulas (.snce ψ χ) := by
+  simp only [subformulas, List.mem_cons, List.mem_append]
+  right; left
+  exact self_mem_subformulas ψ
+
+/-- Subformulas of snce include the right component. -/
+theorem snce_right_mem_subformulas (ψ χ : Formula Atom) :
+    χ ∈ subformulas (.snce ψ χ) := by
+  simp only [subformulas, List.mem_cons, List.mem_append]
+  right; right
+  exact self_mem_subformulas χ
+
+/-- Left of untl is in subformulas. -/
+theorem mem_subformulas_of_untl_left {ψ χ phi : Formula Atom}
+    (h : (ψ U χ) ∈ subformulas phi) : ψ ∈ subformulas phi := by
+  exact subformulas_trans (untl_left_mem_subformulas ψ χ) h
+
+/-- Right of untl is in subformulas. -/
+theorem mem_subformulas_of_untl_right {ψ χ phi : Formula Atom}
+    (h : (ψ U χ) ∈ subformulas phi) : χ ∈ subformulas phi := by
+  exact subformulas_trans (untl_right_mem_subformulas ψ χ) h
+
+/-- Left of snce is in subformulas. -/
+theorem mem_subformulas_of_snce_left {ψ χ phi : Formula Atom}
+    (h : (ψ S χ) ∈ subformulas phi) : ψ ∈ subformulas phi := by
+  exact subformulas_trans (snce_left_mem_subformulas ψ χ) h
+
+/-- Right of snce is in subformulas. -/
+theorem mem_subformulas_of_snce_right {ψ χ phi : Formula Atom}
+    (h : (ψ S χ) ∈ subformulas phi) : χ ∈ subformulas phi := by
+  exact subformulas_trans (snce_right_mem_subformulas ψ χ) h
+
+end Formula
+
+end Cslib.Logic.Temporal
diff --git a/references.bib b/references.bib
index 973371b65..a11948147 100644
--- a/references.bib
+++ b/references.bib
@@ -49,6 +49,17 @@ @book{Blackburn2001
   collection={Cambridge Tracts in Theoretical Computer Science}
 }
 
+@book{ChagrovZakharyaschev1997,
+  author       = {Chagrov, Alexander and Zakharyaschev, Michael},
+  title        = {Modal Logic},
+  series       = {Oxford Logic Guides},
+  volume       = {35},
+  publisher    = {Oxford University Press},
+  address      = {Oxford},
+  year         = {1997},
+  isbn         = {978-0-19-853779-3}
+}
+
 @misc{Burghardt2018,
 	title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}},
 	url = {https://arxiv.org/abs/1806.05036v2},
@@ -112,6 +123,16 @@ @misc{         WikipediaMyhillNerode2026
   note         = {[Online; accessed 9-April-2026]}
 }
 
+@book{Church1956,
+  author       = {Church, Alonzo},
+  title        = {Introduction to Mathematical Logic},
+  volume       = {1},
+  publisher    = {Princeton University Press},
+  address      = {Princeton},
+  year         = {1956},
+  isbn         = {978-0-691-02906-1}
+}
+
 @article{         Chargueraud2012,
 	title = {The {Locally} {Nameless} {Representation}},
 	volume = {49},
@@ -149,6 +170,26 @@ @article{ FLP1985
   numpages  = {9}
 }
 
+@article{Gentzen1935,
+  author       = {Gentzen, Gerhard},
+  title        = {Untersuchungen {\"u}ber das logische Schlie{\ss}en. {I}},
+  journal      = {Mathematische Zeitschrift},
+  volume       = {39},
+  number       = {1},
+  pages        = {176--210},
+  year         = {1935},
+  doi          = {10.1007/BF01201353}
+}
+
+@inproceedings{GabbayPnueliShelahStavi1980,
+  author    = {Dov Gabbay and Amir Pnueli and Saharon Shelah and Jonathan Stavi},
+  title     = {On the Temporal Analysis of Fairness},
+  booktitle = {Proceedings of the 7th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+  pages     = {163--173},
+  year      = {1980},
+  publisher = {ACM},
+}
+
 @article{        Girard1987,
   title={Linear logic},
   author={Girard, Jean-Yves},
@@ -204,6 +245,22 @@ @article{         Hennessy1985
   bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{Heyting1930,
+  author       = {Heyting, Arend},
+  title        = {Die formalen Regeln der intuitionistischen Logik},
+  journal      = {Sitzungsberichte der Preu{\ss}ischen Akademie der
+                  Wissenschaften, physikalisch-mathematische Klasse},
+  year         = {1930},
+  pages        = {42--56}
+}
+
+@phdthesis{Kamp1968,
+  author    = {Hans Kamp},
+  title     = {Tense Logic and the Theory of Linear Order},
+  school    = {University of California, Los Angeles},
+  year      = {1968},
+}
+
 @book{             KatzLindell2020,
   author       = {Jonathan Katz and
                   Yehuda Lindell},
@@ -296,6 +353,15 @@ @Book{            Montesi2023
   keywords      = {choreographic-programming,choreographic-language,choreography,concurrency-theory}
 }
 
+@book{Prawitz1965,
+  author       = {Prawitz, Dag},
+  title        = {Natural Deduction: A Proof-Theoretical Study},
+  publisher    = {Almqvist \& Wiksell},
+  address      = {Stockholm},
+  year         = {1965},
+  note         = {Reprinted by Dover Publications, 2006}
+}
+
 @article{         Nipkow2001,
   title        = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
   author       = {Nipkow, Tobias},
@@ -337,6 +403,18 @@ @Book{            Sangiorgi2011
   doi           = {10.1017/CBO9780511777110}
 }
 
+@book{TroelstraVanDalen1988,
+  author       = {Troelstra, A. S. and van Dalen, D.},
+  title        = {Constructivism in Mathematics: An Introduction},
+  volume       = {1},
+  series       = {Studies in Logic and the Foundations of Mathematics},
+  number       = {121},
+  publisher    = {North-Holland},
+  address      = {Amsterdam},
+  year         = {1988},
+  isbn         = {978-0-444-70506-8}
+}
+
 @incollection{ Thomas1990,
   author       = {Wolfgang Thomas},
   editor       = {Jan van Leeuwen},