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 α} {φ : LO.Propositional.Classical.Formula α} : T ⊢! φ → T ⊨[LO.Propositional.Classical.Valuation α] φ

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_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} : 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_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} (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_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} : 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} (φ : LO.Propositional.Classical.Formula α) : φ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT ∨ ∼φ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.mem_maximalConsistentTheory_iff {α✝ : Type u_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} {φ : LO.Propositional.Classical.Formula α✝} : φ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT ↔ LO.Propositional.Classical.maximalConsistentTheory consisT ⊢! φ

theorem LO.Propositional.Classical.maximalConsistentTheory_consistent' {α✝ : Type u_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} {φ : LO.Propositional.Classical.Formula α✝} : φ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT → ∼φ ∉ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff {α✝ : Type u_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} {φ : LO.Propositional.Classical.Formula α✝} : φ ∉ LO.Propositional.Classical.maximalConsistentTheory consisT ↔ LO.Propositional.Classical.maximalConsistentTheory consisT ⊢! ∼φ

theorem LO.Propositional.Classical.mem_maximalConsistentTheory_and {α✝ : Type u_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} {φ ψ : LO.Propositional.Classical.Formula α✝} (h : φ ⋏ ψ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT) : φ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT ∧ ψ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.mem_maximalConsistentTheory_or {α✝ : Type u_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} {φ ψ : LO.Propositional.Classical.Formula α✝} (h : φ ⋎ ψ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT) : φ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT ∨ ψ ∈ LO.Propositional.Classical.maximalConsistentTheory consisT

theorem LO.Propositional.Classical.maximalConsistentTheory_satisfiable {α✝ : Type u_2} {𝓢✝ : LO.Propositional.Classical.Theory α✝} {consisT : LO.System.Consistent 𝓢✝} : { 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 α} {φ : LO.Propositional.Classical.Formula α} : T ⊨[LO.Propositional.Classical.Valuation α] φ → T ⊢! φ

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

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

• ⋯ = ⋯