Foundation.IntProp.Hilbert.ConsistentTableau

source

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

Type u

Equations

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

Instances For

LO.IntProp.Tableau.instHasSubset

source

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

HasSubset (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₁ t₂ : Tableau α} :

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

source

@[simp]

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

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

source

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

Prop

Equations

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

source

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

Consistent H (insert φ T, U) ↔ ∀ {Γ Δ : List (Formula α)}, (∀ φ ∈ Γ, φ ∈ T) → (∀ φ ∈ Δ, φ ∈ U) → H ⊬ φ ⋏ ⋀Γ ➝ ⋁Δ

source

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

¬Consistent H (insert φ T, U) ↔ ∃ (Γ : List (Formula α)) (Δ : List (Formula α)), (∀ φ ∈ Γ, φ ∈ T) ∧ (∀ φ ∈ Δ, φ ∈ U) ∧ H ⊢! φ ⋏ ⋀Γ ➝ ⋁Δ

source

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

Consistent H (T, insert φ U) ↔ ∀ {Γ Δ : List (Formula α)}, (∀ φ ∈ Γ, φ ∈ T) → (∀ φ ∈ Δ, φ ∈ U) → H ⊬ ⋀Γ ➝ φ ⋎ ⋁Δ

source

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

¬Consistent H (T, insert φ U) ↔ ∃ (Γ : List (Formula α)) (Δ : List (Formula α)), (∀ φ ∈ Γ, φ ∈ T) ∧ (∀ φ ∈ Δ, φ ∈ U) ∧ H ⊢! ⋀Γ ➝ φ ⋎ ⋁Δ

source

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

Consistent H (insert φ t.1, t.2) ∨ Consistent H (t.1, insert φ t.2)

source

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

Disjoint t.1 t.2

source

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

ψ ∉ t.2

source

@[reducible, inline]

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

Prop

Equations

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

source

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

φ ∉ t.1 → φ ∈ t.2

source

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

φ ∉ t.2 → φ ∈ t.1

source

theorem LO.IntProp.Tableau.not_mem₁_iff_mem₂ {α : Type u} {H : Hilbert α} {φ : Formula α} {t : Tableau α} (hCon : Consistent H t) (hMat : t.Saturated) :

φ ∉ t.1 ↔ φ ∈ t.2

source

theorem LO.IntProp.Tableau.not_mem₂_iff_mem₁ {α : Type u} {H : Hilbert α} {φ : Formula α} {t : Tableau α} (hCon : Consistent H t) (hMat : t.Saturated) :

φ ∉ t.2 ↔ φ ∈ t.1

source

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

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

source

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

Consistent H (H.axioms, ∅)

source

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

Tableau α

Equations

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

source

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

ℕ → Tableau α

Equations

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

source

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

Tableau α

Equations

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

source

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

Consistent H (lindenbaum_next H φ t)

source

@[simp]

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

lindenbaum_next_indexed H t 0 = t

source

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

Consistent H (lindenbaum_next_indexed H t i) → Consistent H (lindenbaum_next_indexed H t (i + 1))

source

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

φ ∈ (lindenbaum_next_indexed H t (Encodable.encode φ + 1)).1 ∨ φ ∈ (lindenbaum_next_indexed H t (Encodable.encode φ + 1)).2

source

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

Consistent H (lindenbaum_next_indexed H t i)

source

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

(lindenbaum_next_indexed H t m).1 ⊆ (lindenbaum_next_indexed H t n).1

source

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

(lindenbaum_next_indexed H t m).2 ⊆ (lindenbaum_next_indexed H t n).2

source

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

∃ (u : Tableau α), t ⊆ u ∧ Consistent H u ∧ u.Saturated

source

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

∃ (u : Tableau α), t ⊆ u ∧ Consistent H u ∧ u.Saturated

Alias of LO.IntProp.Tableau.exists_parametricConsistent_saturated_tableau.

source

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

Type u

tableau : Tableau α
saturated : self.tableau.Saturated
consistent : Tableau.Consistent H self.tableau

source

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

Type u

Alias of LO.IntProp.SaturatedConsistentTableau.

Equations

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

Instances For

LO.IntProp.SaturatedConsistentTableau.instNonemptySCTOfConsistentOfIncludeEFQOfEncodable

source

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

∃ (t : SaturatedConsistentTableau H), t₀ ⊆ t.tableau

source

instance LO.IntProp.SaturatedConsistentTableau.instNonemptySCTOfConsistentOfIncludeEFQOfEncodable {α : Type u} {H : Hilbert α} [H.Consistent] [H.IncludeEFQ] [Encodable α] :

Nonempty (SCT H)

source

@[simp]

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

Disjoint t.tableau.1 t.tableau.2

source

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

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

source

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

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

source

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

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

source

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

t₁ = t₂

source

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

t₁ = t₂

source

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

ψ ∉ t.tableau.2

source

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

ψ ∈ t.tableau.1

source

@[simp]

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

⊤ ∈ t.tableau.1

source

@[simp]

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

⊥ ∉ t.tableau.1

source

@[simp]

theorem LO.IntProp.SaturatedConsistentTableau.iff_mem₁_and {α : Type u} {H : Hilbert α} {φ ψ : Formula α} {t : SCT H} :

φ ⋏ ψ ∈ t.tableau.1 ↔ φ ∈ t.tableau.1 ∧ ψ ∈ t.tableau.1

source

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

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

source

@[simp]

theorem LO.IntProp.SaturatedConsistentTableau.iff_mem₁_or {α : Type u} {H : Hilbert α} {φ ψ : Formula α} {t : SCT H} :

φ ⋎ ψ ∈ t.tableau.1 ↔ φ ∈ t.tableau.1 ∨ ψ ∈ t.tableau.1

source

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

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

source

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

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

source

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

H ⊢! φ → φ ∈ t.tableau.1

source

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

ψ ∈ t.tableau.1