Foundation.IntProp.ConsistentTableau

source

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

Type u

Equations

LO.IntProp.Tableau α = (LO.IntProp.Theory α × LO.IntProp.Theory α)

Instances For

source

instance LO.IntProp.Tableau.instHasSubset {α : Type u} :

HasSubset (LO.IntProp.Tableau α)

Equations

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

source

@[simp]

theorem LO.IntProp.Tableau.subset_def {α : Type u} {t₁ : LO.IntProp.Tableau α} {t₂ : LO.IntProp.Tableau α} :

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

source

@[simp]

theorem LO.IntProp.Tableau.equality_def {α : Type u} {t₁ : LO.IntProp.Tableau α} {t₂ : LO.IntProp.Tableau α} :

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

source

def LO.IntProp.Tableau.Consistent {α : Type u} (Λ : LO.IntProp.Hilbert α) (t : LO.IntProp.Tableau α) :

Prop

Equations

LO.IntProp.Tableau.Consistent Λ t = ∀ {Γ Δ : List (LO.IntProp.Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → Λ ⊬ ⋀Γ ➝ ⋁Δ

Instances For

source

theorem LO.IntProp.Tableau.iff_consistent_insert₁ {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {T : LO.IntProp.Theory α} {U : LO.IntProp.Theory α} :

LO.IntProp.Tableau.Consistent Λ (insert p T, U) ↔ ∀ {Γ Δ : List (LO.IntProp.Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → Λ ⊬ p ⋏ ⋀Γ ➝ ⋁Δ

source

theorem LO.IntProp.Tableau.iff_not_consistent_insert₁ {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {T : LO.IntProp.Theory α} {U : LO.IntProp.Theory α} :

¬LO.IntProp.Tableau.Consistent Λ (insert p T, U) ↔ ∃ (Γ : List (LO.IntProp.Formula α)) (Δ : List (LO.IntProp.Formula α)), (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ Λ ⊢! p ⋏ ⋀Γ ➝ ⋁Δ

source

theorem LO.IntProp.Tableau.iff_consistent_insert₂ {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] {p : LO.IntProp.Formula α} {T : LO.IntProp.Theory α} {U : LO.IntProp.Theory α} :

LO.IntProp.Tableau.Consistent Λ (T, insert p U) ↔ ∀ {Γ Δ : List (LO.IntProp.Formula α)}, (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → Λ ⊬ ⋀Γ ➝ p ⋎ ⋁Δ

source

theorem LO.IntProp.Tableau.iff_not_consistent_insert₂ {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] {p : LO.IntProp.Formula α} {T : LO.IntProp.Theory α} {U : LO.IntProp.Theory α} :

¬LO.IntProp.Tableau.Consistent Λ (T, insert p U) ↔ ∃ (Γ : List (LO.IntProp.Formula α)) (Δ : List (LO.IntProp.Formula α)), (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ Λ ⊢! ⋀Γ ➝ p ⋎ ⋁Δ

source

theorem LO.IntProp.Tableau.consistent_either {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] {t : LO.IntProp.Tableau α} (hCon : LO.IntProp.Tableau.Consistent Λ t) (p : LO.IntProp.Formula α) :

LO.IntProp.Tableau.Consistent Λ (insert p t.1, t.2) ∨ LO.IntProp.Tableau.Consistent Λ (t.1, insert p t.2)

source

theorem LO.IntProp.Tableau.disjoint_of_consistent {α : Type u} {Λ : LO.IntProp.Hilbert α} {t : LO.IntProp.Tableau α} (hCon : LO.IntProp.Tableau.Consistent Λ t) :

Disjoint t.1 t.2

source

theorem LO.IntProp.Tableau.not_mem₂ {α : Type u} {Λ : LO.IntProp.Hilbert α} {q : LO.IntProp.Formula α} {t : LO.IntProp.Tableau α} (hCon : LO.IntProp.Tableau.Consistent Λ t) {Γ : List (LO.IntProp.Formula α)} (hΓ : ∀ p ∈ Γ, p ∈ t.1) (h : Λ ⊢! ⋀Γ ➝ q) :

q ∉ t.2

source

@[reducible, inline]

abbrev LO.IntProp.Tableau.Saturated {α : Type u} (t : LO.IntProp.Tableau α) :

Prop

Equations

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

Instances For

source

theorem LO.IntProp.Tableau.mem₂_of_not_mem₁ {α : Type u} {p : LO.IntProp.Formula α} {t : LO.IntProp.Tableau α} (hMat : autoParam t.Saturated _auto✝) :

p ∉ t.1 → p ∈ t.2

source

theorem LO.IntProp.Tableau.mem₁_of_not_mem₂ {α : Type u} {p : LO.IntProp.Formula α} {t : LO.IntProp.Tableau α} (hMat : autoParam t.Saturated _auto✝) :

p ∉ t.2 → p ∈ t.1

source

theorem LO.IntProp.Tableau.not_mem₁_iff_mem₂ {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {t : LO.IntProp.Tableau α} (hCon : autoParam (LO.IntProp.Tableau.Consistent Λ t) _auto✝) (hMat : autoParam t.Saturated _auto✝) :

p ∉ t.1 ↔ p ∈ t.2

source

theorem LO.IntProp.Tableau.not_mem₂_iff_mem₁ {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {t : LO.IntProp.Tableau α} (hCon : autoParam (LO.IntProp.Tableau.Consistent Λ t) _auto✝) (hMat : autoParam t.Saturated _auto✝) :

p ∉ t.2 ↔ p ∈ t.1

source

theorem LO.IntProp.Tableau.saturated_duality {α : Type u} {Λ : LO.IntProp.Hilbert α} {t₁ : LO.IntProp.Tableau α} {t₂ : LO.IntProp.Tableau α} (ct₁ : LO.IntProp.Tableau.Consistent Λ t₁) (ct₂ : LO.IntProp.Tableau.Consistent Λ t₂) (st₁ : t₁.Saturated) (st₂ : t₂.Saturated) :

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

source

theorem LO.IntProp.Tableau.self_consistent {α : Type u} {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [h : LO.System.Consistent Λ] :

LO.IntProp.Tableau.Consistent Λ (Ax(Λ), ∅)

source

def LO.IntProp.Tableau.lindenbaum_next {α : Type u} (Λ : LO.IntProp.Hilbert α) (p : LO.IntProp.Formula α) (t : LO.IntProp.Tableau α) :

LO.IntProp.Tableau α

Equations

LO.IntProp.Tableau.lindenbaum_next Λ p t = if LO.IntProp.Tableau.Consistent Λ (insert p t.1, t.2) then (insert p t.1, t.2) else (t.1, insert p t.2)

Instances For

source

def LO.IntProp.Tableau.lindenbaum_next_indexed {α : Type u} (Λ : LO.IntProp.Hilbert α) [Encodable α] (t : LO.IntProp.Tableau α) :

ℕ → LO.IntProp.Tableau α

Equations

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

Instances For

source

def LO.IntProp.Tableau.lindenbaum_maximal {α : Type u} (Λ : LO.IntProp.Hilbert α) [Encodable α] (t : LO.IntProp.Tableau α) :

LO.IntProp.Tableau α

Equations

LO.IntProp.Tableau.lindenbaum_maximal Λ t = (⋃ (i : ℕ), (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t i).1, ⋃ (i : ℕ), (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t i).2)

Instances For

source

theorem LO.IntProp.Tableau.next_parametericConsistent {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] {t : LO.IntProp.Tableau α} (consistent : LO.IntProp.Tableau.Consistent Λ t) (p : LO.IntProp.Formula α) :

LO.IntProp.Tableau.Consistent Λ (LO.IntProp.Tableau.lindenbaum_next Λ p t)

source

@[simp]

theorem LO.IntProp.Tableau.lindenbaum_next_indexed_zero {α : Type u} {Λ : LO.IntProp.Hilbert α} [Encodable α] {t : LO.IntProp.Tableau α} :

LO.IntProp.Tableau.lindenbaum_next_indexed Λ t 0 = t

source

theorem LO.IntProp.Tableau.lindenbaum_next_indexed_parametricConsistent_succ {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Encodable α] {t : LO.IntProp.Tableau α} {i : ℕ} :

LO.IntProp.Tableau.Consistent Λ (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t i) → LO.IntProp.Tableau.Consistent Λ (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t (i + 1))

source

theorem LO.IntProp.Tableau.mem_lindenbaum_next_indexed {α : Type u} {Λ : LO.IntProp.Hilbert α} [Encodable α] (t : LO.IntProp.Tableau α) (p : LO.IntProp.Formula α) :

p ∈ (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t (Encodable.encode p + 1)).1 ∨ p ∈ (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t (Encodable.encode p + 1)).2

source

theorem LO.IntProp.Tableau.lindenbaum_next_indexed_parametricConsistent {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Encodable α] {t : LO.IntProp.Tableau α} (consistent : LO.IntProp.Tableau.Consistent Λ t) (i : ℕ) :

LO.IntProp.Tableau.Consistent Λ (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t i)

source

theorem LO.IntProp.Tableau.lindenbaum_next_indexed_subset₁_of_lt {α : Type u} {Λ : LO.IntProp.Hilbert α} [Encodable α] {t : LO.IntProp.Tableau α} {m : ℕ} {n : ℕ} (h : m ≤ n) :

(LO.IntProp.Tableau.lindenbaum_next_indexed Λ t m).1 ⊆ (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t n).1

source

theorem LO.IntProp.Tableau.lindenbaum_next_indexed_subset₂_of_lt {α : Type u} {Λ : LO.IntProp.Hilbert α} [Encodable α] {t : LO.IntProp.Tableau α} {m : ℕ} {n : ℕ} (h : m ≤ n) :

(LO.IntProp.Tableau.lindenbaum_next_indexed Λ t m).2 ⊆ (LO.IntProp.Tableau.lindenbaum_next_indexed Λ t n).2

source

theorem LO.IntProp.Tableau.exists_parametricConsistent_saturated_tableau {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Encodable α] {t : LO.IntProp.Tableau α} (hCon : LO.IntProp.Tableau.Consistent Λ t) :

∃ (u : LO.IntProp.Tableau α), t ⊆ u ∧ LO.IntProp.Tableau.Consistent Λ u ∧ u.Saturated

source

theorem LO.IntProp.Tableau.lindenbaum {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Encodable α] {t : LO.IntProp.Tableau α} (hCon : LO.IntProp.Tableau.Consistent Λ t) :

∃ (u : LO.IntProp.Tableau α), t ⊆ u ∧ LO.IntProp.Tableau.Consistent Λ u ∧ u.Saturated

Alias of LO.IntProp.Tableau.exists_parametricConsistent_saturated_tableau.

source

structure LO.IntProp.SaturatedConsistentTableau {α : Type u} (Λ : LO.IntProp.Hilbert α) :

Type u

tableau : LO.IntProp.Tableau α
saturated : self.tableau.Saturated
consistent : LO.IntProp.Tableau.Consistent Λ self.tableau

Instances For

source

theorem LO.IntProp.SaturatedConsistentTableau.saturated {α : Type u} {Λ : LO.IntProp.Hilbert α} (self : LO.IntProp.SaturatedConsistentTableau Λ) :

self.tableau.Saturated

source

theorem LO.IntProp.SaturatedConsistentTableau.consistent {α : Type u} {Λ : LO.IntProp.Hilbert α} (self : LO.IntProp.SaturatedConsistentTableau Λ) :

LO.IntProp.Tableau.Consistent Λ self.tableau

source

def LO.IntProp.SCT {α : Type u} (Λ : LO.IntProp.Hilbert α) :

Type u

Alias of LO.IntProp.SaturatedConsistentTableau.

Equations

@LO.IntProp.SCT = @LO.IntProp.SaturatedConsistentTableau

Instances For

source

theorem LO.IntProp.SaturatedConsistentTableau.lindenbaum {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Encodable α] {t₀ : LO.IntProp.Tableau α} (hCon : LO.IntProp.Tableau.Consistent Λ t₀) :

∃ (t : LO.IntProp.SaturatedConsistentTableau Λ), t₀ ⊆ t.tableau

source

instance LO.IntProp.SaturatedConsistentTableau.instNonemptySCTOfConsistentFormulaHilbert {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Encodable α] [LO.System.Consistent Λ] :

Nonempty (LO.IntProp.SCT Λ)

Equations

⋯ = ⋯

source

@[simp]

theorem LO.IntProp.SaturatedConsistentTableau.disjoint {α : Type u} {Λ : LO.IntProp.Hilbert α} {t : LO.IntProp.SCT Λ} :

Disjoint t.tableau.1 t.tableau.2

source

theorem LO.IntProp.SaturatedConsistentTableau.not_mem₁_iff_mem₂ {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} :

p ∉ t.tableau.1 ↔ p ∈ t.tableau.2

source

theorem LO.IntProp.SaturatedConsistentTableau.not_mem₂_iff_mem₁ {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} :

p ∉ t.tableau.2 ↔ p ∈ t.tableau.1

source

theorem LO.IntProp.SaturatedConsistentTableau.saturated_duality {α : Type u} {Λ : LO.IntProp.Hilbert α} {t₁ : LO.IntProp.SCT Λ} {t₂ : LO.IntProp.SCT Λ} :

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

source

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

t₁ = t₂

source

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

t₁ = t₂

source

theorem LO.IntProp.SaturatedConsistentTableau.not_mem₂ {α : Type u} {Λ : LO.IntProp.Hilbert α} {q : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} {Γ : List (LO.IntProp.Formula α)} (hΓ : ∀ p ∈ Γ, p ∈ t.tableau.1) (h : Λ ⊢! ⋀Γ ➝ q) :

q ∉ t.tableau.2

source

theorem LO.IntProp.SaturatedConsistentTableau.mdp₁ {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} (hp₁ : p ∈ t.tableau.1) (h : Λ ⊢! p ➝ q) :

q ∈ t.tableau.1

source

@[simp]

theorem LO.IntProp.SaturatedConsistentTableau.mem₁_verum {α : Type u} {Λ : LO.IntProp.Hilbert α} {t : LO.IntProp.SCT Λ} :

⊤ ∈ t.tableau.1

source

@[simp]

theorem LO.IntProp.SaturatedConsistentTableau.not_mem₁_falsum {α : Type u} {Λ : LO.IntProp.Hilbert α} {t : LO.IntProp.SCT Λ} :

⊥ ∉ t.tableau.1

source

@[simp]

theorem LO.IntProp.SaturatedConsistentTableau.iff_mem₁_and {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} :

p ⋏ q ∈ t.tableau.1 ↔ p ∈ t.tableau.1 ∧ q ∈ t.tableau.1

source

theorem LO.IntProp.SaturatedConsistentTableau.iff_mem₁_conj {α : Type u} {Λ : LO.IntProp.Hilbert α} {t : LO.IntProp.SCT Λ} {Γ : List (LO.IntProp.Formula α)} :

⋀Γ ∈ t.tableau.1 ↔ ∀ p ∈ Γ, p ∈ t.tableau.1

source

@[simp]

theorem LO.IntProp.SaturatedConsistentTableau.iff_mem₁_or {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} :

p ⋎ q ∈ t.tableau.1 ↔ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1

source

theorem LO.IntProp.SaturatedConsistentTableau.not_mem₁_neg_of_mem₁ {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} :

p ∈ t.tableau.1 → ∼p ∉ t.tableau.1

source

theorem LO.IntProp.SaturatedConsistentTableau.mem₂_neg_of_mem₁ {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} :

p ∈ t.tableau.1 → ∼p ∈ t.tableau.2

source

theorem LO.IntProp.SaturatedConsistentTableau.mem₁_of_provable {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {t : LO.IntProp.SCT Λ} :

Λ ⊢! p → p ∈ t.tableau.1

source

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

q ∈ t.tableau.1