Foundation.Modal.Tableau

source

def LO.Modal.Tableau (α : Type u) :

Type u

Equations

LO.Modal.Tableau α = (Set (LO.Modal.Formula α) × Set (LO.Modal.Formula α))

Instances For

source

def LO.Modal.Tableau.Consistent {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] (𝓢 : S) (t : Tableau α) :

Prop

Equations

LO.Modal.Tableau.Consistent 𝓢 t = ∀ {Γ Δ : Finset (LO.Modal.Formula α)}, ↑Γ ⊆ t.1 → ↑Δ ⊆ t.2 → 𝓢 ⊬ Γ.conj ➝ Δ.disj

Instances For

source

@[reducible, inline]

abbrev LO.Modal.Tableau.Inconsistent {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] (𝓢 : S) (t : Tableau α) :

Prop

Equations

LO.Modal.Tableau.Inconsistent 𝓢 t = ¬LO.Modal.Tableau.Consistent 𝓢 t

Instances For

source

structure LO.Modal.Tableau.Saturated {α : Type u_1} (t : Tableau α) :

Prop

implyK {φ ψ : Formula α} : φ ➝ ψ ∈ t.1 → φ ∈ t.2 ∨ ψ ∈ t.1
implyS {φ ψ : Formula α} : φ ➝ ψ ∈ t.2 → φ ∈ t.1 ∧ ψ ∈ t.2

Instances For

source

structure LO.Modal.Tableau.Disjoint {α : Type u_1} (t : Tableau α) :

Prop

union : Disjoint t.1 t.2
no_bot : ⊥ ∉ t.1

Instances For

source

def LO.Modal.Tableau.Maximal {α : Type u_1} (t : Tableau α) :

Prop

Equations

t.Maximal = ∀ {φ : LO.Modal.Formula α}, φ ∈ t.1 ∨ φ ∈ t.2

Instances For

source

instance LO.Modal.Tableau.instHasSubset {α : Type u_1} :

HasSubset (Tableau α)

Equations

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

source

@[simp]

theorem LO.Modal.Tableau.subset_def {α : Type u_1} {t₁ t₂ : Tableau α} :

t₁ ⊆ t₂ ↔ t₁.1 ⊆ t₂.1 ∧ t₁.2 ⊆ t₂.2

source

theorem LO.Modal.Tableau.equality_def {α : Type u_1} {t₁ t₂ : Tableau α} :

t₁ = t₂ ↔ t₁.1 = t₂.1 ∧ t₁.2 = t₂.2

source

theorem LO.Modal.Tableau.disjoint_of_consistent {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : Tableau α} [Entailment.Cl 𝓢] (hCon : Tableau.Consistent 𝓢 t) :

t.Disjoint

source

theorem LO.Modal.Tableau.mem₂_of_not_mem₁ {α : Type u_1} {t : Tableau α} {φ : Formula α} (hMax : t.Maximal) :

φ ∉ t.1 → φ ∈ t.2

source

theorem LO.Modal.Tableau.mem₁_of_not_mem₂ {α : Type u_1} {t : Tableau α} {φ : Formula α} (hMax : t.Maximal) :

φ ∉ t.2 → φ ∈ t.1

source

theorem LO.Modal.Tableau.iff_not_mem₁_mem₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : Tableau α} {φ : Formula α} [Entailment.Cl 𝓢] (hCon : Tableau.Consistent 𝓢 t) (hMax : t.Maximal) :

φ ∉ t.1 ↔ φ ∈ t.2

source

theorem LO.Modal.Tableau.iff_not_mem₂_mem₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : Tableau α} {φ : Formula α} [Entailment.Cl 𝓢] (hCon : Tableau.Consistent 𝓢 t) (hMax : t.Maximal) :

φ ∉ t.2 ↔ φ ∈ t.1

source

theorem LO.Modal.Tableau.maximal_duality {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} [Entailment.Cl 𝓢] {t₁ t₂ : Tableau α} (hCon₁ : Tableau.Consistent 𝓢 t₁) (hCon₂ : Tableau.Consistent 𝓢 t₂) (hMax₁ : t₁.Maximal) (hMax₂ : t₂.Maximal) :

t₁.1 = t₂.1 ↔ t₁.2 = t₂.2

source

theorem LO.Modal.Tableau.iff_consistent_insert₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} [Entailment.Cl 𝓢] [DecidableEq α] {T U : Set (Formula α)} :

Tableau.Consistent 𝓢 (insert φ T, U) ↔ ∀ {Γ Δ : Finset (Formula α)}, ↑Γ ⊆ T → ↑Δ ⊆ U → 𝓢 ⊬ φ ⋏ Γ.conj ➝ Δ.disj

source

theorem LO.Modal.Tableau.iff_inconsistent_insert₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} [Entailment.Cl 𝓢] [DecidableEq α] {T U : Set (Formula α)} :

Tableau.Inconsistent 𝓢 (insert φ T, U) ↔ ∃ (Γ : Finset (Formula α)) (Δ : Finset (Formula α)), ↑Γ ⊆ T ∧ ↑Δ ⊆ U ∧ 𝓢 ⊢ φ ⋏ Γ.conj ➝ Δ.disj

source

theorem LO.Modal.Tableau.iff_consistent_insert₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} [Entailment.Cl 𝓢] [DecidableEq α] {T U : Set (Formula α)} :

Tableau.Consistent 𝓢 (T, insert φ U) ↔ ∀ {Γ Δ : Finset (Formula α)}, ↑Γ ⊆ T → ↑Δ ⊆ U → 𝓢 ⊬ Γ.conj ➝ φ ⋎ Δ.disj

source

theorem LO.Modal.Tableau.iff_not_consistent_insert₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} [Entailment.Cl 𝓢] [DecidableEq α] {T U : Set (Formula α)} :

Tableau.Inconsistent 𝓢 (T, insert φ U) ↔ ∃ (Γ : Finset (Formula α)) (Δ : Finset (Formula α)), ↑Γ ⊆ T ∧ ↑Δ ⊆ U ∧ 𝓢 ⊢ Γ.conj ➝ φ ⋎ Δ.disj

source

theorem LO.Modal.Tableau.iff_consistent_empty_singleton₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} [Entailment.Cl 𝓢] [DecidableEq α] :

Tableau.Consistent 𝓢 (∅, {φ}) ↔ 𝓢 ⊬ φ

source

theorem LO.Modal.Tableau.iff_inconsistent_singleton₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} [Entailment.Cl 𝓢] [DecidableEq α] :

Tableau.Inconsistent 𝓢 (∅, {φ}) ↔ 𝓢 ⊢ φ

source

theorem LO.Modal.Tableau.either_expand_consistent_of_consistent {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : Tableau α} [Entailment.Cl 𝓢] [DecidableEq α] (hCon : Tableau.Consistent 𝓢 t) (φ : Formula α) :

Tableau.Consistent 𝓢 (insert φ t.1, t.2) ∨ Tableau.Consistent 𝓢 (t.1, insert φ t.2)

source

theorem LO.Modal.Tableau.consistent_empty {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} [Entailment.Cl 𝓢] [DecidableEq α] [H_consis : Entailment.Consistent 𝓢] :

Tableau.Consistent 𝓢 (∅, ∅)

source

noncomputable def LO.Modal.Tableau.lindenbaum_next {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] (𝓢 : S) (φ : Formula α) (t : Tableau α) :

Tableau α

Equations

LO.Modal.Tableau.lindenbaum_next 𝓢 φ t = if LO.Modal.Tableau.Consistent 𝓢 (insert φ t.1, t.2) then (insert φ t.1, t.2) else (t.1, insert φ t.2)

Instances For

source

noncomputable def LO.Modal.Tableau.lindenbaum_indexed {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] (𝓢 : S) [Encodable α] (t : Tableau α) :

ℕ → Tableau α

Equations

One or more equations did not get rendered due to their size.
LO.Modal.Tableau.lindenbaum_indexed 𝓢 t 0 = t

Instances For

source

def LO.Modal.Tableau.lindenbaum_max {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] (𝓢 : S) [Encodable α] (t : Tableau α) :

Tableau α

Equations

LO.Modal.Tableau.lindenbaum_max 𝓢 t = (⋃ (i : ℕ), (LO.Modal.Tableau.lindenbaum_indexed 𝓢 t i).1, ⋃ (i : ℕ), (LO.Modal.Tableau.lindenbaum_indexed 𝓢 t i).2)

Instances For

source

@[simp]

theorem LO.Modal.Tableau.eq_lindenbaum_indexed_zero {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} [Encodable α] {t : Tableau α} :

lindenbaum_indexed 𝓢 t 0 = t

source

theorem LO.Modal.Tableau.consistent_lindenbaum_next {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Entailment.Cl 𝓢] (consistent : Tableau.Consistent 𝓢 t) (φ : Formula α) :

Tableau.Consistent 𝓢 (lindenbaum_next 𝓢 φ t)

source

theorem LO.Modal.Tableau.consistent_lindenbaum_indexed_succ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] [Entailment.Cl 𝓢] {i : ℕ} :

Tableau.Consistent 𝓢 (lindenbaum_indexed 𝓢 t i) → Tableau.Consistent 𝓢 (lindenbaum_indexed 𝓢 t (i + 1))

source

theorem LO.Modal.Tableau.either_mem_lindenbaum_indexed {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} [Encodable α] (t : Tableau α) (φ : Formula α) :

φ ∈ (lindenbaum_indexed 𝓢 t (Encodable.encode φ + 1)).1 ∨ φ ∈ (lindenbaum_indexed 𝓢 t (Encodable.encode φ + 1)).2

source

theorem LO.Modal.Tableau.consistent_lindenbaum_indexed {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] [Entailment.Cl 𝓢] (consistent : Tableau.Consistent 𝓢 t) (i : ℕ) :

Tableau.Consistent 𝓢 (lindenbaum_indexed 𝓢 t i)

source

theorem LO.Modal.Tableau.subset₁_lindenbaum_indexed_of_lt {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] {m n : ℕ} (h : m ≤ n) :

(lindenbaum_indexed 𝓢 t m).1 ⊆ (lindenbaum_indexed 𝓢 t n).1

source

theorem LO.Modal.Tableau.subset₂_lindenbaum_indexed_of_lt {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] {m n : ℕ} (h : m ≤ n) :

(lindenbaum_indexed 𝓢 t m).2 ⊆ (lindenbaum_indexed 𝓢 t n).2

source

theorem LO.Modal.Tableau.exists_list_lindenbaum_index₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] {Γ : List (Formula α)} (hΓ : ↑Γ.toFinset ⊆ ⋃ (i : ℕ), (lindenbaum_indexed 𝓢 t i).1) :

∃ (m : ℕ), ∀ φ ∈ Γ, φ ∈ (lindenbaum_indexed 𝓢 t m).1

source

theorem LO.Modal.Tableau.exists_finset_lindenbaum_index₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] {Γ : Finset (Formula α)} (hΓ : ↑Γ ⊆ ⋃ (i : ℕ), (lindenbaum_indexed 𝓢 t i).1) :

∃ (m : ℕ), ∀ φ ∈ Γ, φ ∈ (lindenbaum_indexed 𝓢 t m).1

source

theorem LO.Modal.Tableau.exists_list_lindenbaum_index₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] {Δ : List (Formula α)} (hΔ : ↑Δ.toFinset ⊆ ⋃ (i : ℕ), (lindenbaum_indexed 𝓢 t i).2) :

∃ (n : ℕ), ∀ φ ∈ Δ, φ ∈ (lindenbaum_indexed 𝓢 t n).2

source

theorem LO.Modal.Tableau.exists_finset_lindenbaum_index₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] {Δ : Finset (Formula α)} (hΓ : ↑Δ ⊆ ⋃ (i : ℕ), (lindenbaum_indexed 𝓢 t i).2) :

∃ (n : ℕ), ∀ φ ∈ Δ, φ ∈ (lindenbaum_indexed 𝓢 t n).2

source

theorem LO.Modal.Tableau.exists_consistent_saturated_tableau {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] [Entailment.Cl 𝓢] (hCon : Tableau.Consistent 𝓢 t) :

∃ (u : Tableau α), t ⊆ u ∧ Tableau.Consistent 𝓢 u ∧ u.Maximal

source

theorem LO.Modal.Tableau.lindenbaum {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {t : Tableau α} {𝓢 : S} [Encodable α] [Entailment.Cl 𝓢] (hCon : Tableau.Consistent 𝓢 t) :

∃ (u : Tableau α), t ⊆ u ∧ Tableau.Consistent 𝓢 u ∧ u.Maximal

Alias of LO.Modal.Tableau.exists_consistent_saturated_tableau.

source

def LO.Modal.MaximalConsistentTableau {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] (𝓢 : S) :

Type u_1

Equations

LO.Modal.MaximalConsistentTableau 𝓢 = { t : LO.Modal.Tableau α // t.Maximal ∧ LO.Modal.Tableau.Consistent 𝓢 t }

Instances For

source

@[simp]

theorem LO.Modal.MaximalConsistentTableau.maximal {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} (t : MaximalConsistentTableau 𝓢) :

(↑t).Maximal

source

@[simp]

theorem LO.Modal.MaximalConsistentTableau.consistent {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} (t : MaximalConsistentTableau 𝓢) :

Tableau.Consistent 𝓢 ↑t

source

theorem LO.Modal.MaximalConsistentTableau.lindenbaum {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t₀ : Tableau α} [Entailment.Cl 𝓢] [Encodable α] (hCon : Tableau.Consistent 𝓢 t₀) :

∃ (t : MaximalConsistentTableau 𝓢), t₀ ⊆ ↑t

source

instance LO.Modal.MaximalConsistentTableau.instNonemptyOfConsistentOfClFormulaOfDecidableEqOfEncodable {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

Nonempty (MaximalConsistentTableau 𝓢)

source

theorem LO.Modal.MaximalConsistentTableau.disjoint {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

(↑t).Disjoint

source

theorem LO.Modal.MaximalConsistentTableau.iff_not_mem₁_mem₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

φ ∉ (↑t).1 ↔ φ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_not_mem₂_mem₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

φ ∉ (↑t).2 ↔ φ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.neither {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

¬(φ ∈ (↑t).1 ∧ φ ∈ (↑t).2)

source

theorem LO.Modal.MaximalConsistentTableau.maximal_duality {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t₁ t₂ : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

(↑t₁).1 = (↑t₂).1 ↔ (↑t₁).2 = (↑t₂).2

source

theorem LO.Modal.MaximalConsistentTableau.equality_of₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t₁ t₂ : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] (e₁ : (↑t₁).1 = (↑t₂).1) :

t₁ = t₂

source

theorem LO.Modal.MaximalConsistentTableau.equality_of₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t₁ t₂ : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] (e₂ : (↑t₁).2 = (↑t₂).2) :

t₁ = t₂

source

theorem LO.Modal.MaximalConsistentTableau.ne₁_of_ne {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t₁ t₂ : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

t₁ ≠ t₂ → (↑t₁).1 ≠ (↑t₂).1

source

theorem LO.Modal.MaximalConsistentTableau.ne₂_of_ne {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t₁ t₂ : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

t₁ ≠ t₂ → (↑t₁).2 ≠ (↑t₂).2

source

theorem LO.Modal.MaximalConsistentTableau.intro_equality {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t₁ t₂ : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] (h₁ : ∀ {φ : Formula α}, φ ∈ (↑t₁).1 → φ ∈ (↑t₂).1) (h₂ : ∀ {φ : Formula α}, φ ∈ (↑t₁).2 → φ ∈ (↑t₂).2) :

t₁ = t₂

source

theorem LO.Modal.MaximalConsistentTableau.iff_provable_include₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {T : Set (Formula α)} :

T *⊢[𝓢] φ ↔ ∀ (t : MaximalConsistentTableau 𝓢), T ⊆ (↑t).1 → φ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_provable_mem₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

𝓢 ⊢ φ ↔ ∀ (t : MaximalConsistentTableau 𝓢), φ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.mdp_mem₁ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] (hφψ : φ ➝ ψ ∈ (↑t).1) (hφ : φ ∈ (↑t).1) :

ψ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.mdp_mem₁_provable {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] (hφψ : 𝓢 ⊢ φ ➝ ψ) (hφ : φ ∈ (↑t).1) :

ψ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.mdp_mem₂_provable {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] (hφψ : 𝓢 ⊢ φ ➝ ψ) :

ψ ∈ (↑t).2 → φ ∈ (↑t).2

source

@[simp]

theorem LO.Modal.MaximalConsistentTableau.mem₁_verum {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

⊤ ∈ (↑t).1

source

@[simp]

theorem LO.Modal.MaximalConsistentTableau.not_mem₂_verum {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

⊤ ∉ (↑t).2

source

@[simp]

theorem LO.Modal.MaximalConsistentTableau.not_mem₁_falsum {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

⊥ ∉ (↑t).1

source

@[simp]

theorem LO.Modal.MaximalConsistentTableau.mem₂_falsum {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] :

⊥ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_and {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

φ ⋏ ψ ∈ (↑t).1 ↔ φ ∈ (↑t).1 ∧ ψ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_and {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

φ ⋏ ψ ∈ (↑t).2 ↔ φ ∈ (↑t).2 ∨ ψ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_conj₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {Γ : List (Formula α)} :

⋀Γ ∈ (↑t).1 ↔ ∀ φ ∈ Γ, φ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_fconj {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {Γ : Finset (Formula α)} :

Γ.conj ∈ (↑t).1 ↔ ↑Γ ⊆ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_conj₂ {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {Γ : List (Formula α)} :

⋀Γ ∈ (↑t).2 ↔ ∃ φ ∈ Γ, φ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_fconj {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {Γ : Finset (Formula α)} :

Γ.conj ∈ (↑t).2 ↔ ∃ φ ∈ Γ, φ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_or {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

φ ⋎ ψ ∈ (↑t).1 ↔ φ ∈ (↑t).1 ∨ ψ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_or {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

φ ⋎ ψ ∈ (↑t).2 ↔ φ ∈ (↑t).2 ∧ ψ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_disj {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {Γ : List (Formula α)} :

⋁Γ ∈ (↑t).1 ↔ ∃ φ ∈ Γ, φ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_disj {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {Γ : List (Formula α)} :

⋁Γ ∈ (↑t).2 ↔ ∀ φ ∈ Γ, φ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_fdisj {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {Γ : Finset (Formula α)} :

Γ.disj ∈ (↑t).2 ↔ ↑Γ ⊆ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_imp {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

φ ➝ ψ ∈ (↑t).1 ↔ φ ∈ (↑t).2 ∨ ψ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_imp' {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

φ ➝ ψ ∈ (↑t).1 ↔ φ ∈ (↑t).1 → ψ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_imp {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ ψ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

φ ➝ ψ ∈ (↑t).2 ↔ φ ∈ (↑t).1 ∧ ψ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_neg {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

∼φ ∈ (↑t).1 ↔ φ ∈ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_neg' {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

∼φ ∈ (↑t).1 ↔ φ ∉ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_neg {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

∼φ ∈ (↑t).2 ↔ φ ∈ (↑t).1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_neg' {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] :

∼φ ∈ (↑t).2 ↔ φ ∉ (↑t).2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_boxItr {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {n : ℕ} [Entailment.K 𝓢] :

□^[n]φ ∈ (↑t).1 ↔ ∀ {t' : MaximalConsistentTableau 𝓢}, (□⁻¹^[n]'(↑t).1) ⊆ (↑t').1 → φ ∈ (↑t').1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_box {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] [Entailment.K 𝓢] :

□φ ∈ (↑t).1 ↔ ∀ {t' : MaximalConsistentTableau 𝓢}, □⁻¹'(↑t).1 ⊆ (↑t').1 → φ ∈ (↑t').1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_boxItr {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {n : ℕ} [Entailment.K 𝓢] :

□^[n]φ ∈ (↑t).2 ↔ ∃ (t' : MaximalConsistentTableau 𝓢), (□⁻¹^[n]'(↑t).1) ⊆ (↑t').1 ∧ φ ∈ (↑t').2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_box {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] [Entailment.K 𝓢] :

□φ ∈ (↑t).2 ↔ ∃ (t' : MaximalConsistentTableau 𝓢), □⁻¹'(↑t).1 ⊆ (↑t').1 ∧ φ ∈ (↑t').2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_diaItr {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {n : ℕ} [Entailment.K 𝓢] :

◇^[n]φ ∈ (↑t).1 ↔ ∃ (t' : MaximalConsistentTableau 𝓢), (□⁻¹^[n]'(↑t).1) ⊆ (↑t').1 ∧ φ ∈ (↑t').1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₁_dia {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] [Entailment.K 𝓢] :

◇φ ∈ (↑t).1 ↔ ∃ (t' : MaximalConsistentTableau 𝓢), □⁻¹'(↑t).1 ⊆ (↑t').1 ∧ φ ∈ (↑t').1

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_diaItr {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {n : ℕ} [Entailment.K 𝓢] :

◇^[n]φ ∈ (↑t).2 ↔ ∀ (t' : MaximalConsistentTableau 𝓢), (□⁻¹^[n]'(↑t).1) ⊆ (↑t').1 → φ ∈ (↑t').2

source

theorem LO.Modal.MaximalConsistentTableau.iff_mem₂_dia {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} {φ : Formula α} {t : MaximalConsistentTableau 𝓢} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] [Entailment.K 𝓢] :

◇φ ∈ (↑t).2 ↔ ∀ (t' : MaximalConsistentTableau 𝓢), □⁻¹'(↑t).1 ⊆ (↑t').1 → φ ∈ (↑t').2

source

theorem Set.exists_of_ne {α : Type u_1} {s t : Set α} (h : s ≠ t) :

∃ (x : α), x ∈ s ∧ x ∉ t ∨ x ∉ s ∧ x ∈ t

source

theorem LO.Modal.MaximalConsistentTableau.exists₁₂_of_ne {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {y z : MaximalConsistentTableau 𝓢} (eyz : y ≠ z) :

∃ φ₂ ∈ (↑y).1, φ₂ ∈ (↑z).2

source

theorem LO.Modal.MaximalConsistentTableau.exists₂₁_of_ne {α : Type u_1} {S : Type u_2} [Entailment S (Formula α)] {𝓢 : S} [Entailment.Cl 𝓢] [DecidableEq α] [Encodable α] {y z : MaximalConsistentTableau 𝓢} (eyz : y ≠ z) :

∃ φ₁ ∈ (↑y).2, φ₁ ∈ (↑z).1