theorem LO.Propositional.Classical.Derivation.sound {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {Δ : LO.Propositional.Classical.Sequent α} : T ⟹ Δ → T ⊨[LO.Propositional.Classical.Valuation α] List.disj Δ

theorem LO.Propositional.Classical.soundness {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {p : LO.Propositional.Classical.Formula α} : T ⊢! p → T ⊨[LO.Propositional.Classical.Valuation α] p

instance LO.Propositional.Classical.instSoundTheoryFormulaSetValuationModels {α : Type u_1} (T : LO.Propositional.Classical.Theory α) : LO.Sound T (LO.Semantics.models (LO.Propositional.Classical.Valuation α) T)

Equations

• ⋯ = ⋯

def LO.Propositional.Classical.consistentTheory {α : Type u_1} : Set (LO.Propositional.Classical.Theory α)

Equations

• LO.Propositional.Classical.consistentTheory = {U : LO.Propositional.Classical.Theory α | LO.System.Consistent U}

theorem LO.Propositional.Classical.exists_maximal_consistent_theory {α : Type u_1} {T : LO.Propositional.Classical.Theory α} (consisT : LO.System.Consistent T) : ∃ (Z : LO.Propositional.Classical.Theory α), LO.System.Consistent Z ∧ T ⊆ Z ∧ ∀ (U : LO.Propositional.Classical.Theory α), LO.System.Consistent U → Z ⊆ U → U = Z

noncomputable def LO.Propositional.Classical.maximalConsistentTheory {α : Type u_1} {T : LO.Propositional.Classical.Theory α} (consisT : LO.System.Consistent T) : LO.Propositional.Classical.Theory α

Equations

• LO.Propositional.Classical.maximalConsistentTheory consisT = Classical.choose ⋯

@[simp]

theorem LO.Propositional.Classical.maximalConsistentTheory_consistent {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} : LO.System.Consistent (LO.Propositional.Classical.maximalConsistentTheory consisT)

@[simp]

theorem LO.Propositional.Classical.subset_maximalConsistentTheory {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} : T ⊆ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.maximalConsistentTheory_maximal {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} (U : LO.Propositional.Classical.Theory α) : LO.System.Consistent U → LO.Propositional.Classical.maximalConsistentTheory consisT ⊆ U → U = LO.Propositional.Classical.maximalConsistentTheory consisT

@[simp]

theorem LO.Propositional.Classical.theory_maximalConsistentTheory_eq {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} : LO.System.theory (LO.Propositional.Classical.maximalConsistentTheory consisT) = LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} (p : LO.Propositional.Classical.Formula α) : p ∈ LO.Propositional.Classical.maximalConsistentTheory consisT ∨ ∼p ∈ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.mem_maximalConsistentTheory_iff {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} {p : LO.Propositional.Classical.Formula α} : p ∈ LO.Propositional.Classical.maximalConsistentTheory consisT ↔ LO.Propositional.Classical.maximalConsistentTheory consisT ⊢! p

theorem LO.Propositional.Classical.maximalConsistentTheory_consistent' {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} {p : LO.Propositional.Classical.Formula α} : p ∈ LO.Propositional.Classical.maximalConsistentTheory consisT → ∼p ∉ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} {p : LO.Propositional.Classical.Formula α} : p ∉ LO.Propositional.Classical.maximalConsistentTheory consisT ↔ LO.Propositional.Classical.maximalConsistentTheory consisT ⊢! ∼p

theorem LO.Propositional.Classical.mem_maximalConsistentTheory_and {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} {p : LO.Propositional.Classical.Formula α} {q : LO.Propositional.Classical.Formula α} (h : p ⋏ q ∈ LO.Propositional.Classical.maximalConsistentTheory consisT) : p ∈ LO.Propositional.Classical.maximalConsistentTheory consisT ∧ q ∈ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.mem_maximalConsistentTheory_or {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} {p : LO.Propositional.Classical.Formula α} {q : LO.Propositional.Classical.Formula α} (h : p ⋎ q ∈ LO.Propositional.Classical.maximalConsistentTheory consisT) : p ∈ LO.Propositional.Classical.maximalConsistentTheory consisT ∨ q ∈ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.maximalConsistentTheory_satisfiable {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {consisT : LO.System.Consistent T} : { val := fun (x : α) => LO.Propositional.Classical.Formula.atom x ∈ LO.Propositional.Classical.maximalConsistentTheory consisT } ⊧* LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.satisfiable_of_consistent {α : Type u_1} {T : LO.Propositional.Classical.Theory α} (consisT : LO.System.Consistent T) : LO.Semantics.Satisfiable (LO.Propositional.Classical.Valuation α) T

theorem LO.Propositional.Classical.completeness! {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {p : LO.Propositional.Classical.Formula α} : T ⊨[LO.Propositional.Classical.Valuation α] p → T ⊢! p

noncomputable def LO.Propositional.Classical.completeness {α : Type u_1} {T : LO.Propositional.Classical.Theory α} {p : LO.Propositional.Classical.Formula α} : T ⊨[LO.Propositional.Classical.Valuation α] p → T ⊢ p

Equations

• LO.Propositional.Classical.completeness h = ⋯.get

instance LO.Propositional.Classical.instCompleteTheoryFormulaSetValuationModels {α : Type u_1} (T : LO.Propositional.Classical.Theory α) : LO.Complete T (LO.Semantics.models (LO.Propositional.Classical.Valuation α) T)

Equations

• ⋯ = ⋯