def LO.Propositional.Superintuitionistic.Tableau (α : Type u) : Type u

Equations

• LO.Propositional.Superintuitionistic.Tableau α = (LO.Propositional.Superintuitionistic.Theory α × LO.Propositional.Superintuitionistic.Theory α)

instance LO.Propositional.Superintuitionistic.Tableau.instHasSubset {α : Type u} : HasSubset (LO.Propositional.Superintuitionistic.Tableau α)

Equations

• LO.Propositional.Superintuitionistic.Tableau.instHasSubset = { Subset := fun (t₁ t₂ : LO.Propositional.Superintuitionistic.Tableau α) => t₁.1 ⊆ t₂.1 ∧ t₁.2 ⊆ t₂.2 }

@[simp]

theorem LO.Propositional.Superintuitionistic.Tableau.subset_def {α : Type u} {t₁ : LO.Propositional.Superintuitionistic.Tableau α} {t₂ : LO.Propositional.Superintuitionistic.Tableau α} : t₁ ⊆ t₂ ↔ t₁.1 ⊆ t₂.1 ∧ t₁.2 ⊆ t₂.2

@[simp]

theorem LO.Propositional.Superintuitionistic.Tableau.equality_def {α : Type u} {t₁ : LO.Propositional.Superintuitionistic.Tableau α} {t₂ : LO.Propositional.Superintuitionistic.Tableau α} : t₁ = t₂ ↔ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2

def LO.Propositional.Superintuitionistic.Tableau.ParametricConsistent {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) (t : LO.Propositional.Superintuitionistic.Tableau α) : Prop

Equations

• (Λ)-Consistent t = ∀ {Γ Δ : List (LO.Propositional.Superintuitionistic.Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → Λ ⊬! ⋀Γ ⟶ ⋁Δ

def LO.Propositional.Superintuitionistic.Tableau.«term(_)-Consistent» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₁ {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {T : LO.Propositional.Superintuitionistic.Theory α} {U : LO.Propositional.Superintuitionistic.Theory α} : (Λ)-Consistent (insert p T, U) ↔ ∀ {Γ Δ : List (LO.Propositional.Superintuitionistic.Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → Λ ⊬! p ⋏ ⋀Γ ⟶ ⋁Δ

theorem LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₁ {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {T : LO.Propositional.Superintuitionistic.Theory α} {U : LO.Propositional.Superintuitionistic.Theory α} : ¬(Λ)-Consistent (insert p T, U) ↔ ∃ (Γ : List (LO.Propositional.Superintuitionistic.Formula α)) (Δ : List (LO.Propositional.Superintuitionistic.Formula α)), (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ Λ ⊢! p ⋏ ⋀Γ ⟶ ⋁Δ

theorem LO.Propositional.Superintuitionistic.Tableau.iff_ParametricConsistent_insert₂ {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] {p : LO.Propositional.Superintuitionistic.Formula α} {T : LO.Propositional.Superintuitionistic.Theory α} {U : LO.Propositional.Superintuitionistic.Theory α} : (Λ)-Consistent (T, insert p U) ↔ ∀ {Γ Δ : List (LO.Propositional.Superintuitionistic.Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → Λ ⊬! ⋀Γ ⟶ p ⋎ ⋁Δ

theorem LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂ {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] {p : LO.Propositional.Superintuitionistic.Formula α} {T : LO.Propositional.Superintuitionistic.Theory α} {U : LO.Propositional.Superintuitionistic.Theory α} : ¬(Λ)-Consistent (T, insert p U) ↔ ∃ (Γ : List (LO.Propositional.Superintuitionistic.Formula α)) (Δ : List (LO.Propositional.Superintuitionistic.Formula α)), (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ Λ ⊢! ⋀Γ ⟶ p ⋎ ⋁Δ

theorem LO.Propositional.Superintuitionistic.Tableau.consistent_either {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] {t : LO.Propositional.Superintuitionistic.Tableau α} (hCon : (Λ)-Consistent t) (p : LO.Propositional.Superintuitionistic.Formula α) : (Λ)-Consistent (insert p t.1, t.2) ∨ (Λ)-Consistent (t.1, insert p t.2)

theorem LO.Propositional.Superintuitionistic.Tableau.disjoint_of_consistent {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t : LO.Propositional.Superintuitionistic.Tableau α} (hCon : (Λ)-Consistent t) : Disjoint t.1 t.2

theorem LO.Propositional.Superintuitionistic.Tableau.not_mem₂ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {q : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.Tableau α} (hCon : (Λ)-Consistent t) {Γ : List (LO.Propositional.Superintuitionistic.Formula α)} (hΓ : ∀ p ∈ Γ, p ∈ t.1) (h : Λ ⊢! ⋀Γ ⟶ q) : q ∉ t.2

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.Tableau.Saturated {α : Type u} (t : LO.Propositional.Superintuitionistic.Tableau α) : Prop

Equations

• t.Saturated = ∀ (p : LO.Propositional.Superintuitionistic.Formula α), p ∈ t.1 ∨ p ∈ t.2

theorem LO.Propositional.Superintuitionistic.Tableau.mem₂_of_not_mem₁ {α : Type u} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.Tableau α} (hMat : autoParam t.Saturated _auto✝) : p ∉ t.1 → p ∈ t.2

theorem LO.Propositional.Superintuitionistic.Tableau.mem₁_of_not_mem₂ {α : Type u} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.Tableau α} (hMat : autoParam t.Saturated _auto✝) : p ∉ t.2 → p ∈ t.1

theorem LO.Propositional.Superintuitionistic.Tableau.not_mem₁_iff_mem₂ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.Tableau α} (hCon : autoParam ((Λ)-Consistent t) _auto✝) (hMat : autoParam t.Saturated _auto✝) : p ∉ t.1 ↔ p ∈ t.2

theorem LO.Propositional.Superintuitionistic.Tableau.not_mem₂_iff_mem₁ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.Tableau α} (hCon : autoParam ((Λ)-Consistent t) _auto✝) (hMat : autoParam t.Saturated _auto✝) : p ∉ t.2 ↔ p ∈ t.1

theorem LO.Propositional.Superintuitionistic.Tableau.saturated_duality {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t₁ : LO.Propositional.Superintuitionistic.Tableau α} {t₂ : LO.Propositional.Superintuitionistic.Tableau α} (ct₁ : (Λ)-Consistent t₁) (ct₂ : (Λ)-Consistent t₂) (st₁ : t₁.Saturated) (st₂ : t₂.Saturated) : t₁.1 = t₂.1 ↔ t₁.2 = t₂.2

theorem LO.Propositional.Superintuitionistic.Tableau.self_ParametricConsistent {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [h : LO.System.Consistent Λ] : (Λ)-Consistent (Ax(Λ), ∅)

def LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) (p : LO.Propositional.Superintuitionistic.Formula α) (t : LO.Propositional.Superintuitionistic.Tableau α) : LO.Propositional.Superintuitionistic.Tableau α

Equations

• LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next Λ p t = if (Λ)-Consistent (insert p t.1, t.2) then (insert p t.1, t.2) else (t.1, insert p t.2)

def LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) [Encodable α] (t : LO.Propositional.Superintuitionistic.Tableau α) : ℕ → LO.Propositional.Superintuitionistic.Tableau α

Equations

• One or more equations did not get rendered due to their size.
• LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t 0 = t

def LO.Propositional.Superintuitionistic.Tableau.lindenbaum_maximal {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) [Encodable α] (t : LO.Propositional.Superintuitionistic.Tableau α) : LO.Propositional.Superintuitionistic.Tableau α

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Propositional.Superintuitionistic.Tableau.next_parametericConsistent {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] {t : LO.Propositional.Superintuitionistic.Tableau α} (consistent : (Λ)-Consistent t) (p : LO.Propositional.Superintuitionistic.Formula α) : (Λ)-Consistent (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next Λ p t)

@[simp]

theorem LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_zero {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Encodable α] {t : LO.Propositional.Superintuitionistic.Tableau α} : LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t 0 = t

theorem LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent_succ {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] {t : LO.Propositional.Superintuitionistic.Tableau α} {i : ℕ} : (Λ)-Consistent (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t i) → (Λ)-Consistent (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t (i + 1))

theorem LO.Propositional.Superintuitionistic.Tableau.mem_lindenbaum_next_indexed {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Encodable α] (t : LO.Propositional.Superintuitionistic.Tableau α) (p : LO.Propositional.Superintuitionistic.Formula α) : p ∈ (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t (Encodable.encode p + 1)).1 ∨ p ∈ (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t (Encodable.encode p + 1)).2

theorem LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_parametricConsistent {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] {t : LO.Propositional.Superintuitionistic.Tableau α} (consistent : (Λ)-Consistent t) (i : ℕ) : (Λ)-Consistent (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t i)

theorem LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₁_of_lt {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Encodable α] {t : LO.Propositional.Superintuitionistic.Tableau α} {m : ℕ} {n : ℕ} (h : m ≤ n) : (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t m).1 ⊆ (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t n).1

theorem LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed_subset₂_of_lt {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Encodable α] {t : LO.Propositional.Superintuitionistic.Tableau α} {m : ℕ} {n : ℕ} (h : m ≤ n) : (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t m).2 ⊆ (LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed Λ t n).2

theorem LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] {t : LO.Propositional.Superintuitionistic.Tableau α} (hCon : (Λ)-Consistent t) : ∃ (u : LO.Propositional.Superintuitionistic.Tableau α), t ⊆ u ∧ (Λ)-Consistent u ∧ u.Saturated

theorem LO.Propositional.Superintuitionistic.Tableau.lindenbaum {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] {t : LO.Propositional.Superintuitionistic.Tableau α} (hCon : (Λ)-Consistent t) : ∃ (u : LO.Propositional.Superintuitionistic.Tableau α), t ⊆ u ∧ (Λ)-Consistent u ∧ u.Saturated

Alias of LO.Propositional.Superintuitionistic.Tableau.exists_parametricConsistent_saturated_tableau.

structure LO.Propositional.Superintuitionistic.SaturatedConsistentTableau {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) : Type u

• tableau : LO.Propositional.Superintuitionistic.Tableau α
• saturated : self.tableau.Saturated
• consistent : (Λ)-Consistent self.tableau

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.saturated {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} (self : LO.Propositional.Superintuitionistic.SaturatedConsistentTableau Λ) : self.tableau.Saturated

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.consistent {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} (self : LO.Propositional.Superintuitionistic.SaturatedConsistentTableau Λ) : (Λ)-Consistent self.tableau

def LO.Propositional.Superintuitionistic.SCT {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) : Type u

Alias of LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.

Equations

• @LO.Propositional.Superintuitionistic.SCT = @LO.Propositional.Superintuitionistic.SaturatedConsistentTableau

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.lindenbaum {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] {t₀ : LO.Propositional.Superintuitionistic.Tableau α} (hCon : (Λ)-Consistent t₀) : ∃ (t : LO.Propositional.Superintuitionistic.SaturatedConsistentTableau Λ), t₀ ⊆ t.tableau

instance LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.instNonemptySCTOfConsistentFormulaDeductionParameter {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] [LO.System.Consistent Λ] : Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.disjoint {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : Disjoint t.tableau.1 t.tableau.2

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_iff_mem₂ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : p ∉ t.tableau.1 ↔ p ∈ t.tableau.2

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₂_iff_mem₁ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : p ∉ t.tableau.2 ↔ p ∈ t.tableau.1

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.saturated_duality {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t₁ : LO.Propositional.Superintuitionistic.SCT Λ} {t₂ : LO.Propositional.Superintuitionistic.SCT Λ} : t₁.tableau.1 = t₂.tableau.1 ↔ t₁.tableau.2 = t₂.tableau.2

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.equality_of₁ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t₁ : LO.Propositional.Superintuitionistic.SCT Λ} {t₂ : LO.Propositional.Superintuitionistic.SCT Λ} (e₁ : t₁.tableau.1 = t₂.tableau.1) : t₁ = t₂

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.equality_of₂ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t₁ : LO.Propositional.Superintuitionistic.SCT Λ} {t₂ : LO.Propositional.Superintuitionistic.SCT Λ} (e₂ : t₁.tableau.2 = t₂.tableau.2) : t₁ = t₂

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₂ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {q : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} {Γ : List (LO.Propositional.Superintuitionistic.Formula α)} (hΓ : ∀ p ∈ Γ, p ∈ t.tableau.1) (h : Λ ⊢! ⋀Γ ⟶ q) : q ∉ t.tableau.2

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mdp₁ {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} (hp₁ : p ∈ t.tableau.1) (h : Λ ⊢! p ⟶ q) : q ∈ t.tableau.1

@[simp]

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_verum {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : ⊤ ∈ t.tableau.1

@[simp]

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_falsum {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : ⊥ ∉ t.tableau.1

@[simp]

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : p ⋏ q ∈ t.tableau.1 ↔ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_conj {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {t : LO.Propositional.Superintuitionistic.SCT Λ} {Γ : List (LO.Propositional.Superintuitionistic.Formula α)} : ⋀Γ ∈ t.tableau.1 ↔ ∀ p ∈ Γ, p ∈ t.tableau.1

@[simp]

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : p ⋎ q ∈ t.tableau.1 ↔ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.not_mem₁_neg_of_mem₁ {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : p ∈ t.tableau.1 → ~p ∉ t.tableau.1

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₂_neg_of_mem₁ {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : p ∈ t.tableau.1 → ~p ∈ t.tableau.2

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_of_provable {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} : Λ ⊢! p → p ∈ t.tableau.1

theorem LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mdp₁_mem {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} {t : LO.Propositional.Superintuitionistic.SCT Λ} (hp : p ∈ t.tableau.1) (h : p ⟶ q ∈ t.tableau.1) : q ∈ t.tableau.1

def LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] : LO.Kripke.Frame.Dep α

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.reflexive {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] : Reflexive (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel

theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.antisymmetric {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] : Antisymmetric (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel

theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.transitive {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] : Transitive (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel

theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.confluent {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] [LO.System.HasAxiomWeakLEM Λ] : Confluent (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel

theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.connected {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] [LO.System.HasAxiomDummett Λ] : Connected (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel

def LO.Propositional.Superintuitionistic.Kripke.CanonicalModel {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] : LO.Kripke.Model α

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.hereditary {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] : (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).Valuation.atomic_hereditary

@[reducible]

instance LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.instSemanticsFormulaWorld {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] : LO.Semantics (LO.Propositional.Superintuitionistic.Formula α) (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).World

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.frame_def {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] {t₁ : LO.Propositional.Superintuitionistic.SCT Λ} {t₂ : LO.Propositional.Superintuitionistic.SCT Λ} : (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).Frame.Rel t₁ t₂ ↔ t₁.tableau.1 ⊆ t₂.tableau.1

@[simp]

theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.valuation_def {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] {t : LO.Propositional.Superintuitionistic.SCT Λ} {a : α} : (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).Valuation t a ↔ LO.Propositional.Superintuitionistic.Formula.atom a ∈ t.tableau.1

theorem LO.Propositional.Superintuitionistic.Kripke.truthlemma {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] {p : LO.Propositional.Superintuitionistic.Formula α} {t : (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).World} : t ⊧ p ↔ p ∈ t.tableau.1

theorem LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Encodable α] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] {p : LO.Propositional.Superintuitionistic.Formula α} : LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ ⊧ p ↔ Λ ⊢! p

theorem LO.Propositional.Superintuitionistic.Kripke.complete {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] [DecidableEq α] [Encodable α] {𝔽 : LO.Kripke.FrameClass} (H : LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ ∈ 𝔽) {p : LO.Propositional.Superintuitionistic.Formula α} : 𝔽#α ⊧ p → Λ ⊢! p

instance LO.Propositional.Superintuitionistic.Kripke.instComplete {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] [DecidableEq α] [Encodable α] {𝔽 : LO.Kripke.FrameClass} (H : LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ ∈ 𝔽) : LO.Complete Λ (𝔽#α)

Equations

• ⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.Int_complete {α : Type u} [DecidableEq α] [Encodable α] : LO.Complete 𝐈𝐧𝐭 (LO.Kripke.ReflexiveTransitiveFrameClass#α)

Equations

• ⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.instCompleteDeductionParameterFormulaDepIntuitionisticFrameClassOfSystem {α : Type u} [DecidableEq α] [Encodable α] : LO.Complete 𝐈𝐧𝐭 𝔽(𝐈𝐧𝐭 of α)

Equations

• ⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.LC_complete {α : Type u} [DecidableEq α] [Encodable α] : LO.Complete 𝐋𝐂 (LO.Kripke.ReflexiveTransitiveConnectedFrameClass#α)

Equations

• ⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.KC_complete {α : Type u} [DecidableEq α] [Encodable α] : LO.Complete 𝐊𝐂 (LO.Kripke.ReflexiveTransitiveConfluentFrameClass#α)

Equations

• ⋯ = ⋯