Documentation

Foundation.Propositional.Classical.Basic.Completeness

theorem LO.Propositional.Classical.Derivation.sound {α : Type u_1} {T : Theory α} {Δ : Sequent α} :

T ⟹ Δ → T ⊨[Valuation α] List.disj Δ

theorem LO.Propositional.Classical.soundness {α : Type u_1} {T : Theory α} {φ : Formula α} :

T ⊢! φ → T ⊨[Valuation α] φ

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

Sound T (Semantics.models (Valuation α) T)

def LO.Propositional.Classical.consistentTheory {α : Type u_1} :

Set (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 : Theory α} (consisT : System.Consistent T) :

∃ (Z : Theory α), System.Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), System.Consistent U → Z ⊆ U → U = Z

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

Equations

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

@[simp]

theorem LO.Propositional.Classical.maximalConsistentTheory_consistent {α✝ : Type u_2} {𝓢✝ : Theory α✝} {consisT : System.Consistent 𝓢✝} :

System.Consistent (maximalConsistentTheory consisT)

@[simp]

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

T ⊆ maximalConsistentTheory consisT

theorem LO.Propositional.Classical.maximalConsistentTheory_maximal {α✝ : Type u_2} {𝓢✝ : Theory α✝} {consisT : System.Consistent 𝓢✝} (U : Theory α✝) :

System.Consistent U → maximalConsistentTheory consisT ⊆ U → U = maximalConsistentTheory consisT

@[simp]

theorem LO.Propositional.Classical.theory_maximalConsistentTheory_eq {α✝ : Type u_2} {𝓢✝ : Theory α✝} {consisT : System.Consistent 𝓢✝} :

System.theory (maximalConsistentTheory consisT) = maximalConsistentTheory consisT

theorem LO.Propositional.Classical.mem_or_neg_mem_maximalConsistentTheory {α : Type u_1} {T : Theory α} {consisT : System.Consistent T} (φ : Formula α) :

φ ∈ maximalConsistentTheory consisT ∨ ∼φ ∈ maximalConsistentTheory consisT

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

φ ∈ maximalConsistentTheory consisT ↔ maximalConsistentTheory consisT ⊢! φ

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

φ ∈ maximalConsistentTheory consisT → ∼φ ∉ maximalConsistentTheory consisT

theorem LO.Propositional.Classical.not_mem_maximalConsistentTheory_iff {α✝ : Type u_2} {𝓢✝ : Theory α✝} {consisT : System.Consistent 𝓢✝} {φ : Formula α✝} :

φ ∉ maximalConsistentTheory consisT ↔ maximalConsistentTheory consisT ⊢! ∼φ

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

φ ∈ maximalConsistentTheory consisT ∧ ψ ∈ maximalConsistentTheory consisT

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

φ ∈ maximalConsistentTheory consisT ∨ ψ ∈ maximalConsistentTheory consisT

theorem LO.Propositional.Classical.maximalConsistentTheory_satisfiable {α✝ : Type u_2} {𝓢✝ : Theory α✝} {consisT : System.Consistent 𝓢✝} :

{ val := fun (x : α✝) => Formula.atom x ∈ maximalConsistentTheory consisT } ⊧* maximalConsistentTheory consisT

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

Semantics.Satisfiable (Valuation α) T

theorem LO.Propositional.Classical.completeness! {α : Type u_1} {T : Theory α} {φ : Formula α} :

T ⊨[Valuation α] φ → T ⊢! φ

noncomputable def LO.Propositional.Classical.completeness {α : Type u_1} {T : Theory α} {φ : Formula α} :

T ⊨[Valuation α] φ → T ⊢ φ

Equations

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

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

Complete T (Semantics.models (Valuation α) T)