Equations
Instances For
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 α}
:
@[simp]
theorem
LO.Propositional.Superintuitionistic.Tableau.equality_def
{α : Type u}
{t₁ : LO.Propositional.Superintuitionistic.Tableau α}
{t₂ : LO.Propositional.Superintuitionistic.Tableau α}
:
def
LO.Propositional.Superintuitionistic.Tableau.ParametricConsistent
{α : Type u}
(Λ : LO.Propositional.Superintuitionistic.DeductionParameter α)
(t : LO.Propositional.Superintuitionistic.Tableau α)
:
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 α}
:
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 α}
:
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 α}
:
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 α}
:
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 α)
:
Equations
- t.Saturated = ∀ (p : LO.Propositional.Superintuitionistic.Formula α), p ∈ t.1 ∨ p ∈ t.2
Instances For
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✝)
:
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✝)
:
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)
:
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 α)
:
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)
Instances For
def
LO.Propositional.Superintuitionistic.Tableau.lindenbaum_next_indexed
{α : Type u}
(Λ : LO.Propositional.Superintuitionistic.DeductionParameter α)
[Encodable α]
(t : 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
Instances For
def
LO.Propositional.Superintuitionistic.Tableau.lindenbaum_maximal
{α : Type u}
(Λ : LO.Propositional.Superintuitionistic.DeductionParameter α)
[Encodable α]
(t : LO.Propositional.Superintuitionistic.Tableau α)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 α)
:
@[simp]
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 : ℕ}
:
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 : ℕ)
:
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)
:
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)
:
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
Instances For
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
Instances For
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 Λ]
:
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.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]
@[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 Λ}
:
@[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 Λ}
:
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