diff --git a/Foundation.lean b/Foundation.lean
index eeba1bc7f..f026cea73 100644
--- a/Foundation.lean
+++ b/Foundation.lean
@@ -19,6 +19,7 @@ import Foundation.Propositional.Heyting.Semantics
 import Foundation.Propositional.Logic.Disjunctive
 import Foundation.Propositional.Logic.WellKnown
 import Foundation.Propositional.Logic.Sublogic
+import Foundation.Propositional.Logic.Sublogic.BD
 import Foundation.Propositional.Logic.Letterless_Int_Cl
 
 -- FirstOrder
diff --git a/Foundation/Propositional/BoundDepth.lean b/Foundation/Propositional/BoundDepth.lean
new file mode 100644
index 000000000..027d338f2
--- /dev/null
+++ b/Foundation/Propositional/BoundDepth.lean
@@ -0,0 +1,16 @@
+import Foundation.Propositional.Formula
+
+namespace LO.Propositional
+
+namespace Axioms
+
+protected abbrev BoundDepth' : ℕ → Formula ℕ
+  | 0     => (.atom 0) ⋎ ∼(.atom 0)
+  | n + 1 => (.atom (n + 1)) ⋎ ((.atom (n + 1)) ➝ Axioms.BoundDepth' n)
+
+
+protected abbrev BoundDepth (n : ℕ+) : Formula ℕ := Axioms.BoundDepth' n.natPred
+
+end Axioms
+
+end LO.Propositional
diff --git a/Foundation/Propositional/Hilbert/BD.lean b/Foundation/Propositional/Hilbert/BD.lean
new file mode 100644
index 000000000..3fda6191d
--- /dev/null
+++ b/Foundation/Propositional/Hilbert/BD.lean
@@ -0,0 +1,17 @@
+import Foundation.Propositional.Hilbert.Int
+import Foundation.Propositional.BoundDepth
+
+
+namespace LO.Propositional
+
+namespace Hilbert
+
+variable {n : ℕ+}
+
+protected abbrev BD (n : ℕ+) : Hilbert ℕ := ⟨{Axioms.EFQ (.atom 0), Axioms.BoundDepth n}⟩
+instance : (Hilbert.BD n).FiniteAxiomatizable where
+instance : (Hilbert.BD n).HasEFQ where p := 0;
+
+end Hilbert
+
+end LO.Propositional
diff --git a/Foundation/Propositional/Kripke/AxiomBoundDepth.lean b/Foundation/Propositional/Kripke/AxiomBoundDepth.lean
new file mode 100644
index 000000000..8bae6e6b2
--- /dev/null
+++ b/Foundation/Propositional/Kripke/AxiomBoundDepth.lean
@@ -0,0 +1,266 @@
+import Foundation.Propositional.Kripke.Completeness
+import Foundation.Vorspiel.List.Chain
+import Mathlib.Data.PNat.Basic
+import Foundation.Propositional.BoundDepth
+
+namespace LO.Propositional
+
+namespace Kripke
+
+open Kripke
+open Formula.Kripke
+
+section definability
+
+variable {F : Kripke.Frame}
+
+open Formula (atom)
+open Classical
+
+/-- Frame has at most `n`-chain. -/
+def Frame.IsDepthLt (F : Frame) (n : ℕ) := ∀ l : List F.World, l.length = n + 1 ∧ l.Chain' F → ¬l.Nodup
+
+private lemma not_isDepthLt'_of_not_validate_BoundDepth' {M : Model} {x : M.World} {n : ℕ} (h : ¬x ⊧ Axioms.BoundDepth' n)
+  : ∃ l : List M.World, l.length = n + 2 ∧ l.Chain' (· ≺ ·) ∧ (l.head? = some x) ∧ ∀ i j : Fin l.length, i ≠ j → l.get i ≠ l.get j := by
+  induction n generalizing x with
+  | zero =>
+    have ⟨h₁, h₂⟩ := Satisfies.not_or_def.mp h;
+    replace ⟨y, Rxy, h₂⟩ := Satisfies.not_neg_def.mp h₂;
+    use [x, y];
+    refine ⟨?_, ?_, ?_, ?_⟩;
+    . simp;
+    . simpa;
+    . simp;
+    . simp only [List.length_cons, List.length_nil, Nat.reduceAdd, ne_eq, List.get_eq_getElem];
+      intro i j hij;
+      by_contra hC;
+      match i, j with
+      | 0, 0 => contradiction;
+      | 1, 1 => contradiction;
+      | 0, 1 =>
+        simp only [Fin.isValue, Fin.val_zero, List.getElem_cons_zero, Fin.val_one, List.getElem_cons_succ] at hC;
+        subst hC;
+        contradiction;
+      | 1, 0 =>
+        simp only [Fin.isValue, Fin.val_zero, List.getElem_cons_zero, Fin.val_one, List.getElem_cons_succ] at hC;
+        subst hC;
+        contradiction;
+  | succ n ih =>
+    have ⟨h₁, h₂⟩ := Satisfies.not_or_def.mp h;
+    replace ⟨y, Rxy, h₂, h₃⟩ := Satisfies.not_imp_def.mp h₂;
+    obtain ⟨l, hl₁, hl₂, hl₃, hl₄⟩ := @ih y h₃;
+    use (x :: l);
+    refine ⟨?_, ?_, ?_, ?_⟩;
+    . simpa;
+    . apply List.Chain'.cons';
+      . exact hl₂;
+      . simpa [hl₃];
+    . simp;
+    . apply List.ne_get_con_get_con_of_ne;
+      . exact hl₄;
+      . by_contra hC;
+        have : l ≠ [] :=  List.length_pos_iff_ne_nil.mp (by omega);
+        have Rhx : (l.head _) ≺ x := List.rel_head_of_chain'_preorder hl₂ (by assumption) x hC;
+        have ehy : (l.head _) = y := List.head_eq_iff_head?_eq_some (by assumption) |>.mpr hl₃;
+        subst ehy;
+        have exy := _root_.antisymm Rxy Rhx;
+        subst exy;
+        contradiction;
+
+private lemma not_isDepthLt_of_not_validate_BoundDepth' {n : ℕ} (h : ¬F ⊧ Axioms.BoundDepth' n)
+  : ¬F.IsDepthLt (n + 1) := by
+  obtain ⟨M, x, rfl, h₂⟩ := ValidOnFrame.exists_model_world_of_not h;
+  obtain ⟨l, hl₁, hl₂, _, hl₃⟩ := not_isDepthLt'_of_not_validate_BoundDepth' h₂;
+  dsimp [Frame.IsDepthLt];
+  push_neg;
+  use l;
+  refine ⟨⟨?_, ?_⟩, ?_⟩;
+  . simpa using hl₁;
+  . assumption;
+  . apply List.nodup_iff_get_ne_get.mpr hl₃;
+
+private lemma validate_BoundDepth'_of_isDepthLt {n : ℕ} : F.IsDepthLt (n + 1) → F ⊧ Axioms.BoundDepth' n := by
+  contrapose!;
+  intro h;
+  exact not_isDepthLt_of_not_validate_BoundDepth' h;
+
+lemma validate_BoundDepth_of_isDepthLt {n : ℕ+} : F.IsDepthLt n → F ⊧ Axioms.BoundDepth n := by
+  simpa using validate_BoundDepth'_of_isDepthLt (n := n.natPred);
+
+
+abbrev cascadeVal (l : List F.World) (n) (hl : l.length = n + 1 := by omega) : Valuation F := ⟨
+  λ w a =>
+    letI i : Fin l.length := ⟨(l.length - 1) - a, by omega⟩;
+    letI x : F.World := l[i]
+    x ≺ w
+  ,
+  by
+    simp only [Fin.getElem_fin];
+    intro x y Rxy a Rlx;
+    exact _root_.trans Rlx Rxy;
+⟩
+
+/-
+lemma cascadeVal_sat {l : List F.World} {hl : 0 < l.length} (a : Fin l.length) :
+  letI i : Fin l.length := ⟨l.length - (a + 1), by omega⟩;
+  Satisfies ⟨F, cascadeVal l hl⟩ (l[i]) (.atom a) := by
+  apply _root_.refl;
+
+lemma wowwow
+  (hl₁ : 1 < l.length) (hl₂ : l.Chain' (· ≺ ·)) :
+  letI x : F.World := l.tail.head (List.ne_nil_of_length_pos (by simpa));
+  Satisfies ⟨F, cascadeVal l (by omega)⟩ x (Axioms.BoundDepth' n) →
+  Satisfies ⟨F, cascadeVal l.tail (by simpa)⟩ x (Axioms.BoundDepth' n) := by
+  induction n with
+  | zero =>
+    simp [Axioms.BoundDepth', Satisfies];
+    have e : l[l.length - 1 - 1 + 1] = l[l.length - 1] := by
+
+      sorry;
+    rintro (h | h);
+    . left;
+      rw [e];
+      apply _root_.trans ?_ h;
+      apply _root_.refl;
+    . right;
+      intro x Rhx;
+      have := h Rhx;
+      revert this;
+      contrapose!;
+      rw [e];
+      tauto;
+  | succ n ih =>
+    simp_all [Satisfies]
+    rintro (h | h);
+    . left;
+      sorry;
+    . right;
+      intro x Rhx h₂;
+      apply Satisfies.formula_hereditary Rhx $ ih ?_
+      apply h;
+      . apply _root_.refl;
+      . sorry;
+-/
+
+lemma isDepthLt_of_validate_BoundDepth'_aux {n : ℕ}
+  {l : List F.World}
+  (hl₁ : l.length = n + 2) (hl₂ : l.Chain' (· ≺ ·)) :
+  letI M : Model := ⟨F, (cascadeVal l (n + 1))⟩;
+  letI x₀ : M.World := l.head (List.ne_nil_of_length_pos (by omega));
+  Satisfies M x₀ (Axioms.BoundDepth' n) → ¬l.Nodup := by
+  intro h;
+  induction n generalizing l with
+  | zero =>
+    apply List.nodup_iff_get_ne_get.not.mpr;
+    push_neg;
+    let i₀ : Fin l.length := ⟨0, by omega⟩;
+    let i₁ : Fin l.length := ⟨1, by omega⟩;
+    use i₀, i₁;
+    constructor;
+    . simp [i₀, i₁];
+    . replace h := Satisfies.or_def.mp h;
+      rcases h with h | h;
+      . replace h : l[1] ≺ l[0] := by
+          simpa [Semantics.Realize, Satisfies, hl₁, List.head_eq_getElem_zero] using h;
+        apply _root_.antisymm ?_ h;
+        apply List.Chain'.of_lt hl₂;
+        simp;
+      . exfalso;
+        apply Satisfies.neg_def.mp h (w' := l[i₁]) $ by
+          apply List.rel_head_of_chain'_preorder hl₂;
+          simp;
+        simp [Semantics.Realize, Satisfies, i₁, hl₁];
+  | succ n ih =>
+    replace h := Satisfies.or_def.mp h;
+    rcases h with h | h;
+    . apply List.nodup_iff_get_ne_get.not.mpr;
+      push_neg;
+      use ⟨0, by omega⟩, ⟨1, by omega⟩;
+      constructor
+      . simp;
+      . simp only [Fin.getElem_fin];
+        apply _root_.antisymm (r := F.Rel');
+        . apply List.Chain'.of_lt hl₂;
+          simp;
+        . simpa [Semantics.Realize, Satisfies, hl₁, List.head_eq_getElem_zero] using h;
+    . suffices ¬l.tail.Nodup by exact List.not_noDup_of_not_tail_noDup this;
+      apply ih (l := l.tail);
+      . exact List.Chain'.tail hl₂;
+      . have := h (w' := l.tail.head ?_) ?_ ?_;
+        . sorry;
+        . apply List.ne_nil_of_length_pos
+          simp [hl₁];
+        . suffices l[0] ≺ l[1] by simpa [List.head_eq_getElem_zero];
+          apply List.Chain'.of_lt hl₂;
+          simp;
+        . simp [Satisfies, hl₁]
+      . simpa;
+
+lemma isDepthLt_of_validate_BoundDepth' {n : ℕ} (h : F ⊧ Axioms.BoundDepth' n) : F.IsDepthLt (n + 1) := by
+  rintro l ⟨l₁, l₂⟩;
+  apply isDepthLt_of_validate_BoundDepth'_aux (n := n) l₁ l₂;
+  apply h;
+
+lemma isDepthLt_of_validate_BoundDepth {n : ℕ+} : F ⊧ Axioms.BoundDepth n → F.IsDepthLt n := by
+  convert isDepthLt_of_validate_BoundDepth' (n := n.natPred);
+  simp;
+
+end definability
+
+
+
+section canonical
+
+variable {S} [Entailment (Formula ℕ) S]
+variable {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢]
+
+open Formula.Kripke
+open Entailment
+     Entailment.FiniteContext
+open canonicalModel
+open SaturatedConsistentTableau
+open Classical
+
+namespace Canonical
+
+open Formula
+
+lemma isDepthLt' (h : 𝓢 ⊢! (Axioms.BoundDepth' n)) :
+  ∀ l : List (canonicalFrame 𝓢).World, l.length = n + 2 ∧ (l.head? = some (canonicalFrame 𝓢).default) ∧ l.Chain' (· ≺ ·) → ∃ i j : Fin l.length, i ≠ j ∧ l.get i = l.get j := by
+  rintro l ⟨hl₁, hl₂, hl₃⟩;
+  induction n with
+  | zero =>
+    simp at hl₁;
+    let i₀ : Fin l.length := ⟨0, by omega⟩;
+    let i₁ : Fin l.length := ⟨1, by omega⟩;
+    use i₀, i₁;
+    constructor;
+    . simp [i₀, i₁];
+    . generalize ex₀ : l.get i₀ = x₀;
+      generalize ex₁ : l.get i₁ = x₁;
+      sorry;
+      /-
+      have Rx₀₁ : x₀ ≺ x₁ := by
+        sorry;
+      by_contra hC;
+      have := (iff_valid_on_canonicalModel_deducible.mpr h) x₀;
+      simp [Axioms.BoundDepth', Axioms.BoundDepth] at this;
+      rcases this with (h | h);
+      . simp [Semantics.Realize, Satisfies, canonicalModel] at h;
+        simp [Semantics.Realize] at h;
+      . have := Satisfies.neg_def.mp h Rx₀₁
+
+        sorry;
+      -/
+  | succ n ih =>
+    sorry;
+
+end Canonical
+
+end canonical
+
+
+
+end Kripke
+
+end LO.Propositional
diff --git a/Foundation/Propositional/Kripke/Basic.lean b/Foundation/Propositional/Kripke/Basic.lean
index a25db77b1..30d18d5b4 100644
--- a/Foundation/Propositional/Kripke/Basic.lean
+++ b/Foundation/Propositional/Kripke/Basic.lean
@@ -35,6 +35,8 @@ instance [Finite F.World] : F.IsFinite := ⟨⟩
 @[trans] lemma trans (F : Frame) {x y z : F.World} : x ≺ y → y ≺ z → x ≺ z := F.rel_partial_order.trans x y z
 lemma antisymm (F : Frame) {x y : F.World} : x ≺ y → y ≺ x → x = y := F.rel_partial_order.antisymm x y
 
+noncomputable abbrev default (F : Frame) : F.World := F.world_nonempty.some
+
 end Frame
 
 section
@@ -95,12 +97,20 @@ variable {M : Kripke.Model} {w w' : M.World} {a : ℕ} {φ ψ χ : Formula ℕ}
 
 @[simp] lemma and_def  : w ⊧ φ ⋏ ψ ↔ w ⊧ φ ∧ w ⊧ ψ := by simp [Satisfies];
 
+lemma not_and_def : ¬w ⊧ φ ⋏ ψ ↔ ¬w ⊧ φ ∨ ¬w ⊧ ψ := Iff.trans (Iff.not and_def) (by tauto)
+
 @[simp] lemma or_def   : w ⊧ φ ⋎ ψ ↔ w ⊧ φ ∨ w ⊧ ψ := by simp [Satisfies];
 
-@[simp] lemma imp_def  : w ⊧ φ ➝ ψ ↔ ∀ {w' : M.World}, (w ≺ w') → (w' ⊧ φ → w' ⊧ ψ) := by simp [Satisfies, imp_iff_not_or];
+lemma not_or_def : ¬w ⊧ φ ⋎ ψ ↔ ¬w ⊧ φ ∧ ¬w ⊧ ψ := Iff.trans (Iff.not or_def) (by simp_all)
+
+@[simp] lemma imp_def  : w ⊧ φ ➝ ψ ↔ ∀ {w'}, (w ≺ w') → (w' ⊧ φ → w' ⊧ ψ) := by simp [Satisfies, imp_iff_not_or];
+
+lemma not_imp_def : ¬w ⊧ φ ➝ ψ ↔ ∃ w', (w ≺ w') ∧ (w' ⊧ φ) ∧ ¬(w' ⊧ ψ) := Iff.trans (Iff.not imp_def) (by simp_all)
 
 @[simp] lemma neg_def  : w ⊧ ∼φ ↔ ∀ {w' : M.World}, (w ≺ w') → ¬(w' ⊧ φ) := by simp [Satisfies];
 
+lemma not_neg_def : ¬w ⊧ ∼φ ↔ ∃ w', (w ≺ w') ∧ (w' ⊧ φ) := Iff.trans (Iff.not neg_def) (by simp_all)
+
 lemma not_of_neg : w ⊧ ∼φ → ¬w ⊧ φ := fun h hC ↦ h (refl w) hC
 
 instance : Semantics.Top M.World where
diff --git a/Foundation/Propositional/Kripke/Hilbert/BD.lean b/Foundation/Propositional/Kripke/Hilbert/BD.lean
new file mode 100644
index 000000000..ee17f095e
--- /dev/null
+++ b/Foundation/Propositional/Kripke/Hilbert/BD.lean
@@ -0,0 +1,48 @@
+import Foundation.Propositional.Hilbert.BD
+import Foundation.Propositional.Kripke.AxiomBoundDepth
+import Foundation.Propositional.Kripke.Hilbert.Soundness
+
+namespace LO.Propositional
+
+open Kripke
+open Hilbert.Kripke
+open Formula.Kripke
+
+namespace Kripke.FrameClass
+
+protected abbrev isDepthLt (n : ℕ+) : FrameClass := { F | F.IsDepthLt n }
+
+end Kripke.FrameClass
+
+
+namespace Hilbert.BD.Kripke
+
+variable {n : ℕ+}
+
+instance sound : Sound (Hilbert.BD n) (FrameClass.isDepthLt n) := instSound_of_validates_axioms $ by
+    apply FrameClass.Validates.withAxiomEFQ;
+    rintro F hF _ rfl;
+    replace hF := Set.mem_setOf_eq.mp hF;
+    apply validate_BoundDepth_of_isDepthLt hF;
+
+instance consistent : Entailment.Consistent (Hilbert.BD n) := consistent_of_sound_frameclass (FrameClass.isDepthLt n) $ by
+  use whitepoint;
+  apply Set.mem_setOf_eq.mpr;
+  simp only [Frame.IsDepthLt, whitepoint, ne_eq, List.get_eq_getElem, and_true, and_imp];
+  intro l hl₁ hl₂;
+  apply List.nodup_iff_get_ne_get.not.mpr;
+  push_neg;
+  use ⟨0, by omega⟩, ⟨n, by omega⟩;
+  simp only [ne_eq, Fin.mk.injEq, Fin.getElem_fin, and_true];
+  apply PNat.ne_zero n |>.symm;
+
+instance canonical : Canonical (Hilbert.BD n) (FrameClass.isDepthLt n) := ⟨by
+  apply Set.mem_setOf_eq.mpr;
+  sorry;
+⟩
+
+instance complete : Complete (Hilbert.BD n) (FrameClass.isDepthLt n) := inferInstance
+
+end Hilbert.BD.Kripke
+
+end LO.Propositional
diff --git a/Foundation/Propositional/Logic/Basic.lean b/Foundation/Propositional/Logic/Basic.lean
index 4516d24ef..87932ea71 100644
--- a/Foundation/Propositional/Logic/Basic.lean
+++ b/Foundation/Propositional/Logic/Basic.lean
@@ -14,11 +14,15 @@ protected abbrev Logic.Int : Logic := Hilbert.Int.logic
 
 namespace Logic
 
-class Superintuitionistic (L : Logic) where
+class IsSuperintuitionistic (L : Logic) where
   subset_Int : Logic.Int ⊆ L
   mdp_closed {φ ψ} : φ ➝ ψ ∈ L → φ ∈ L → ψ ∈ L
   subst_closed {φ} : φ ∈ L → ∀ s, φ⟦s⟧ ∈ L
 
+class Consistent (L : Logic) : Prop where
+  consis : L ≠ Set.univ
+attribute [simp] Consistent.consis
+
 end Logic
 
 
@@ -28,7 +32,7 @@ open Entailment
 
 variable {H : Hilbert ℕ}
 
-protected instance superintuitionistic [H.HasEFQ] : (H.logic).Superintuitionistic where
+protected instance superintuitionistic [H.HasEFQ] : (H.logic).IsSuperintuitionistic where
   subset_Int := by
     intro φ hφ;
     induction hφ using Hilbert.Deduction.rec! with
@@ -45,9 +49,16 @@ protected instance superintuitionistic [H.HasEFQ] : (H.logic).Superintuitionisti
 
 end Hilbert
 
-instance : (Logic.Int).Superintuitionistic := Hilbert.superintuitionistic
 
+instance : (Logic.Int).IsSuperintuitionistic := Hilbert.superintuitionistic
 
+instance Logic.consistent_of_consistent_hilbert {H : Hilbert ℕ} [Entailment.Consistent H] : Consistent (H.logic) := ⟨by
+  apply Set.eq_univ_iff_forall.not.mpr;
+  push_neg;
+  obtain ⟨φ, hφ⟩ : ∃ φ, H ⊬ φ := Entailment.Consistent.exists_unprovable inferInstance;
+  use φ;
+  simpa;
+⟩
 
 section
 
@@ -67,6 +78,8 @@ lemma Logic.Int.Kripke.eq_all : Logic.Int = FrameClass.all.logic := eq_Hilbert_L
 
 lemma Logic.Int.Kripke.eq_all_finite : Logic.Int = FrameClass.finite_all.logic := eq_Hilbert_Logic_KripkeFrameClass_Logic
 
+
+
 end
 
 
diff --git a/Foundation/Propositional/Logic/Sublogic/BD.lean b/Foundation/Propositional/Logic/Sublogic/BD.lean
new file mode 100644
index 000000000..8cfc5861f
--- /dev/null
+++ b/Foundation/Propositional/Logic/Sublogic/BD.lean
@@ -0,0 +1,79 @@
+import Foundation.Propositional.Logic.WellKnown
+
+namespace LO.Propositional.Logic
+
+open Entailment
+open Kripke
+open Formula.Kripke
+
+namespace BD
+
+variable {n m : ℕ+}
+
+theorem subset_succ : Logic.BD (n + 1) ⊂ Logic.BD n := by
+  constructor;
+  . simp only [Kripke.eq_isDepthLt, Set.setOf_subset_setOf];
+    intro φ hφ F hF;
+    apply hφ;
+    simp only [Set.mem_setOf_eq, Frame.IsDepthLt, and_imp, PNat.add_coe, PNat.val_ofNat] at hF ⊢;
+    intro l hl₁ hl₂;
+    apply List.not_noDup_of_not_tail_noDup $ hF l.tail ?_ ?_;
+    . simpa;
+    . apply List.Chain'.tail hl₂;
+  . suffices ∃ φ, (Hilbert.BD n) ⊢! φ ∧ ¬(FrameClass.isDepthLt (n + 1)) ⊧ φ by
+      obtain ⟨φ, hφ₁, hφ₂⟩ := this;
+      simp only [Kripke.eq_isDepthLt, Set.setOf_subset_setOf];
+      push_neg;
+      use φ;
+      constructor;
+      . exact BD.Kripke.eq_isDepthLt.subset hφ₁;
+      . assumption;
+    use Axioms.BoundDepth n;
+    constructor;
+    . apply Hilbert.Deduction.maxm!;
+      simp only [Set.mem_setOf_eq, Set.mem_insert_iff, Set.mem_singleton_iff, exists_eq_or_imp, exists_eq_left];
+      right;
+      use Substitution.id;
+      simp;
+    . apply not_validOnFrameClass_of_exists_frame;
+      use ⟨Fin (n + 1), (· ≤ ·)⟩;
+      constructor;
+      . simp only [Set.mem_setOf_eq, Frame.IsDepthLt, PNat.add_coe, PNat.val_ofNat, and_imp];
+        rintro l hl _;
+        apply List.not_nodup_of_lt_length;
+        omega;
+      . apply not_imp_not.mpr $ Kripke.isDepthLt_of_validate_BoundDepth;
+        dsimp [Frame.IsDepthLt];
+        push_neg;
+        use List.finRange (n + 1);
+        exact ⟨⟨List.length_finRange _, List.finRange.chain'_lt⟩, List.finRange.noDup⟩;
+
+lemma subset_add : Logic.BD (n + m) ⊂ Logic.BD n := by
+  induction m with
+  | one => exact subset_succ;
+  | succ m ih =>
+    trans Logic.BD (n + m);
+    . rw [(show n + (m + 1) = n + m + 1 by rfl)];
+      apply subset_succ;
+    . apply ih;
+
+lemma subset_of_lt (hnm : n < m) : Logic.BD m ⊂ Logic.BD n := by
+  convert subset_add (n := n) (m := m - n);
+  exact PNat.add_sub_of_lt hnm |>.symm;
+
+lemma neq_of_neq (hnm : n ≠ m) : Logic.BD n ≠ Logic.BD m := by
+  rcases lt_trichotomy n m with h | rfl | h;
+  . apply subset_of_lt h |>.ne.symm;
+  . contradiction;
+  . apply subset_of_lt h |>.ne;
+
+/-- There are countable infinite superintuitionistic logics. -/
+instance : Infinite { L : Logic // L.IsSuperintuitionistic ∧ L.Consistent } := Infinite.of_injective (λ n => ⟨Logic.BD n, ⟨inferInstance, inferInstance⟩⟩) $ by
+  intro i j;
+  simp only [Subtype.mk.injEq];
+  contrapose!;
+  apply BD.neq_of_neq;
+
+end BD
+
+end LO.Propositional.Logic
diff --git a/Foundation/Propositional/Logic/WellKnown.lean b/Foundation/Propositional/Logic/WellKnown.lean
index 27b6e194c..19c280504 100644
--- a/Foundation/Propositional/Logic/WellKnown.lean
+++ b/Foundation/Propositional/Logic/WellKnown.lean
@@ -4,6 +4,7 @@ import Foundation.Propositional.Kripke.Hilbert.Cl
 import Foundation.Propositional.Kripke.Hilbert.KC
 import Foundation.Propositional.Kripke.Hilbert.LC
 import Foundation.Propositional.Kripke.Hilbert.KP
+import Foundation.Propositional.Kripke.Hilbert.BD
 
 namespace LO.Propositional
 
@@ -34,6 +35,11 @@ protected abbrev KP : Logic := Hilbert.KP.logic
 lemma KP.Kripke.eq_krieselputnam : Logic.KP = Kripke.FrameClass.krieselputnam.logic
   := eq_Hilbert_Logic_KripkeFrameClass_Logic
 
+
+protected abbrev BD (n : ℕ+) : Logic := (Hilbert.BD n).logic
+lemma BD.Kripke.eq_isDepthLt : (Logic.BD n) = (Kripke.FrameClass.isDepthLt n).logic
+  := eq_Hilbert_Logic_KripkeFrameClass_Logic
+
 end Logic
 
 end LO.Propositional
diff --git a/Foundation/Vorspiel/Fin/Supplemental.lean b/Foundation/Vorspiel/Fin/Supplemental.lean
index 262d7744b..3ddc12bf1 100644
--- a/Foundation/Vorspiel/Fin/Supplemental.lean
+++ b/Foundation/Vorspiel/Fin/Supplemental.lean
@@ -12,6 +12,11 @@ lemma isEmpty_embedding_lt (hn : n > m) : IsEmpty (Fin n ↪ Fin m) := by
   apply Function.Embedding.isEmpty_of_card_lt;
   simpa;
 
+lemma le_of_nonempty_embedding : Nonempty (Fin n ↪ Fin m) → n ≤ m := by
+  contrapose!;
+  rw [not_nonempty_iff];
+  apply isEmpty_embedding_lt;
+
 variable {n : ℕ} [NeZero n] {i : Fin n}
 
 def last' : Fin n := ⟨n - 1, Nat.sub_one_lt'⟩
diff --git a/Foundation/Vorspiel/List/Chain.lean b/Foundation/Vorspiel/List/Chain.lean
index d3fa9a18a..5af0479e7 100644
--- a/Foundation/Vorspiel/List/Chain.lean
+++ b/Foundation/Vorspiel/List/Chain.lean
@@ -1,6 +1,7 @@
 import Mathlib.Data.List.Nodup
 import Mathlib.Data.List.Range
 import Foundation.Vorspiel.Fin.Supplemental
+import Foundation.Vorspiel.List.Supplemental
 
 lemma Nat.zero_lt_of_not_zero {n : ℕ} (hn : n ≠ 0) : 0 < n := by omega;
 
@@ -39,29 +40,6 @@ lemma range.le_chain' : List.Chain' (· < ·) (List.range n) := by
   | 0 => simp [List.range_zero]
   | n + 1 => apply le_chain'_succ;
 
-lemma finRange.le_chain'_succ : List.Chain' (· < ·) (List.finRange (n + 1)) := by
-  rw [finRange_succ];
-  induction n with
-  | zero => simp [finRange]
-  | succ n ih =>
-    rw [List.finRange_succ, List.map]
-    apply List.chain'_append_cons_cons (α := Fin (n + 2)) (l₁ := []) |>.mpr;
-    refine ⟨?_, ?_, ?_⟩;
-    . tauto;
-    . tauto;
-    . have := @List.chain'_map_of_chain'
-        (α := Fin (n + 1)) (β := Fin (n + 2)) (R := (· < ·)) (S := (· < ·))
-        (f := Fin.succ)
-        (by simp)
-        (l := 0 :: (map Fin.succ (finRange n)))
-      apply this;
-      exact ih;
-
-@[simp]
-lemma finRange.le_chain' : List.Chain' (· < ·) (List.finRange n) := by
-  match n with
-  | 0 => simp [List.finRange_zero]
-  | n + 1 => apply finRange.le_chain'_succ;
 
 end
 
@@ -73,6 +51,11 @@ variable {R} [IsTrans α R] {l : List α} {i j : Fin l.length}
 lemma of_lt (h : List.Chain' R l) (hij : i < j) : R (l.get i) (l.get j) :=
   List.pairwise_iff_get.mp (List.chain'_iff_pairwise.mp h) _ _ hij
 
+lemma of_le [IsRefl α R] (h : List.Chain' R l) (hij : i ≤ j) : R (l.get i) (l.get j) := by
+  rcases (lt_or_eq_of_le hij) with hij | rfl;
+  . apply of_lt h hij;
+  . apply IsRefl.refl;
+
 lemma connected_of_trans' (h : List.Chain' R l) (eij : i ≠ j) : R (l.get i) (l.get j) ∨ R (l.get j) (l.get i) := by
   rcases Nat.lt_trichotomy i j with (_ | _ | _);
   . left; exact of_lt h $ by omega;
@@ -126,6 +109,23 @@ lemma chain'_concat :  List.Chain' R (l.concat a) ↔ List.Chain' R l ∧ ∀ x
       have : R x a := h₂ x hx;
       simpa;
 
+lemma chain'_of_trans_of_lt {l : List α} {R} [IsTrans _ R] (h : ∀ i j : Fin l.length, i < j → R l[i] l[j]) : l.Chain' R := by
+  induction l with
+  | nil => simp;
+  | cons x xs ih =>
+    apply List.chain'_cons'.mpr;
+    constructor;
+    . intro y hy;
+      replace hy := List.mem_head?_eq_head hy;
+      obtain ⟨hxs, rfl⟩ := hy;
+      have := h ⟨0, by simp⟩ ⟨1, ?_⟩ ?_;
+      . simpa [←(List.head_eq_getElem_zero hxs)] using this;
+      . simp [length_cons, lt_add_iff_pos_left, List.ne_nil_iff_length_pos.mp hxs];
+      . apply Fin.mk_lt_mk.mpr;
+        omega;
+    . apply ih;
+      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij;
+      simpa using h ⟨i + 1, by simpa⟩ ⟨j + 1, by simpa⟩ (by simpa);
 
 section
 
@@ -180,9 +180,41 @@ lemma rel_getLast_of_chain'_preorder [IsPreorder _ R] (h : List.Chain' R l) (lh
 
 end
 
+
 def embedding_of_exists_noDup {l : List α} (hl₁ : l.Nodup) (hl₂ : l.length = n) : Fin n ↪ α := by
   refine ⟨λ ⟨i, hi⟩ => l.get ⟨i, by omega⟩, ?_⟩;
   . rintro ⟨i, hi⟩ ⟨j, hj⟩ hij;
     simpa using (List.nodup_iff_injective_get (l := l) |>.mp hl₁) hij;
 
+lemma not_nodup_of_lt_length {l : List (Fin n)} : l.length > n → ¬l.Nodup := by
+  contrapose!;
+  intro h;
+  apply Fin.le_of_nonempty_embedding;
+  exact ⟨List.embedding_of_exists_noDup h (n := l.length) (by simp)⟩;
+
+
+namespace finRange
+
+variable {n : ℕ}
+
+@[simp]
+lemma chain'_le : List.finRange n |>.Chain' (· < ·) := by
+  apply chain'_of_trans_of_lt;
+  intro i j hij;
+  simpa;
+
+@[simp]
+lemma chain'_lt : List.finRange n |>.Chain' (· ≤ ·) := by
+  apply chain'_of_trans_of_lt;
+  intro i j hij;
+  apply le_of_lt;
+  simpa;
+
+@[simp]
+lemma noDup : List.finRange n |>.Nodup := by
+  apply List.nodup_iff_get_ne_get.mpr;
+  simp;
+
+end finRange
+
 end List
diff --git a/Foundation/Vorspiel/List/Supplemental.lean b/Foundation/Vorspiel/List/Supplemental.lean
index 5759ef00e..641bb84f2 100644
--- a/Foundation/Vorspiel/List/Supplemental.lean
+++ b/Foundation/Vorspiel/List/Supplemental.lean
@@ -2,7 +2,7 @@ import Foundation.Vorspiel.Vorspiel
 
 namespace List
 
-variable {l : List α}
+variable {α} {l : List α}
 
 lemma exists_of_not_nil (hl : l ≠ []) : ∃ a, a ∈ l := by
   match l with
@@ -20,4 +20,59 @@ lemma iff_nil_forall : (l = []) ↔ (∀ a ∈ l, a ∈ []) := by
     use a;
     tauto;
 
+lemma ne_get_con_get_con_of_ne
+  (h : ∀ i j : Fin l.length, i ≠ j → (l.get i) ≠ (l.get j))
+  (hx : x ∉ l)
+  : ∀ i j, i ≠ j → (x :: l).get i ≠ (x :: l).get j := by
+  rintro ⟨i, hi⟩ ⟨j, hj⟩ hij;
+  match i, j with
+  | 0, 0 => contradiction;
+  | 0, j + 1 =>
+    revert hx;
+    contrapose!;
+    intro h;
+    apply List.mem_of_getElem;
+    exact h.symm;
+  | i + 1, 0 =>
+    revert hx;
+    contrapose!;
+    intro h;
+    apply List.mem_of_getElem;
+    exact h;
+  | i + 1,j + 1 =>
+    apply h;
+    simpa using hij;
+
+lemma iff_eq_getElem_eq_getElem? {i j : Fin l.length} : l[i] = l[j] ↔ l[i]? = l[j]? := by
+  simp_all only [Fin.getElem_fin, Fin.getElem?_fin, Fin.is_lt, getElem?_eq_getElem, Option.some.injEq];
+
+lemma nodup_iff_get_ne_get : l.Nodup ↔ ∀ i j : Fin l.length, i ≠ j → l[i] ≠ l[j] := by
+  apply Iff.trans List.nodup_iff_getElem?_ne_getElem?
+  constructor
+  · rintro h ⟨i, hi⟩ ⟨j, hj⟩ eij;
+    wlog hij : i < j;
+    . apply this h j hj i hi eij.symm ?_ |>.symm;
+      apply lt_of_le_of_ne';
+      . exact le_of_not_lt hij;
+      . by_contra eij;
+        subst eij;
+        simp at eij;
+    have := h i j hij hj;
+    revert this;
+    contrapose!;
+    apply List.iff_eq_getElem_eq_getElem?.mp;
+  · intro h i j hij hjl;
+    apply l.iff_eq_getElem_eq_getElem? (i := ⟨i, by omega⟩) (j := ⟨j, by omega⟩) |>.not.mp;
+    apply h;
+    simp only [ne_eq, Fin.mk.injEq];
+    by_contra eij;
+    subst eij;
+    simp at hij;
+
+protected lemma Nodup.tail {l : List α} (h : l.Nodup) : l.tail.Nodup := Nodup.sublist (tail_sublist l) h
+
+lemma not_noDup_of_not_tail_noDup {l : List α} : ¬l.tail.Nodup → ¬l.Nodup := by
+  contrapose!;
+  apply Nodup.tail
+
 end List