Completeness theorem

Generic filters

@[implicit_reducible]

instance LO.FirstOrder.Derivation.Canonical.instEncodableSequentOfEncodableOfDecidableEq {K : Language} [K.Encodable] [K.DecidableEq] : Encodable (Sequent K)

Equations

• LO.FirstOrder.Derivation.Canonical.instEncodableSequentOfEncodableOfDecidableEq = List.encodable

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Derivation.Canonical.instEncodableConsistentSequentOfEncodable {K : Language} [K.Encodable] : Encodable (ConsistentSequent K)

Equations

• LO.FirstOrder.Derivation.Canonical.instEncodableConsistentSequentOfEncodable = Subtype.encodable

def LO.FirstOrder.Derivation.Canonical.decidablePoints {K : Language} (φ : Proposition K) : Order.DenseSet (ConsistentSequent K)

Equations

• LO.FirstOrder.Derivation.Canonical.decidablePoints φ = { set := {p : LO.FirstOrder.Derivation.Canonical.ConsistentSequent K | p ⊩ᶜ φ ∨ p ⊩ᶜ ∼φ}, is_dense := ⋯ }

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.mem_decidablePoints_def {K : Language} (p : ConsistentSequent K) (φ : Proposition K) : p ∈ decidablePoints φ ↔ p ⊩ᶜ φ ∨ p ⊩ᶜ ∼φ

def LO.FirstOrder.Derivation.Canonical.henkinPoints {K : Language} (φ : Semiproposition K 1) : Order.DenseSet (ConsistentSequent K)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.mem_henkinPoints_def {K : Language} (p : ConsistentSequent K) (φ : Semiproposition K 1) : p ∈ henkinPoints φ ↔ ∀ q ≤ p, q ⊩ᶜ ∃¹ φ → ∃ (t : Semiterm K ℕ 0), q ⊩ᶜ φ/[t]

@[reducible, inline]

abbrev LO.FirstOrder.Derivation.Canonical.denseSets {K : Language} : Set (Order.DenseSet (ConsistentSequent K))

Equations

• LO.FirstOrder.Derivation.Canonical.denseSets = Set.range LO.FirstOrder.Derivation.Canonical.decidablePoints ∪ Set.range LO.FirstOrder.Derivation.Canonical.henkinPoints

theorem LO.FirstOrder.Derivation.Canonical.exists_genericFilter {K : Language} [K.Encodable] (p : ConsistentSequent K) : ∃ (G : Order.PFilter (ConsistentSequent K)), G.IsGeneric denseSets ∧ p ∈ G

noncomputable def LO.FirstOrder.Derivation.Canonical.genericFilter {K : Language} [K.Encodable] (p : ConsistentSequent K) : Order.PFilter (ConsistentSequent K)

Equations

• LO.FirstOrder.Derivation.Canonical.genericFilter p = Classical.choose ⋯

instance LO.FirstOrder.Derivation.Canonical.genericFilter_isGeneric {K : Language} [K.Encodable] (p : ConsistentSequent K) : (genericFilter p).IsGeneric denseSets

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.mem_genericFilter {K : Language} [K.Encodable] (p : ConsistentSequent K) : p ∈ genericFilter p

def LO.FirstOrder.Derivation.Canonical.GenericForces {K : Language} [K.Encodable] (p : ConsistentSequent K) (φ : Proposition K) : Prop

Equations

• LO.FirstOrder.Derivation.Canonical.GenericForces p φ = ∃ q ∈ LO.FirstOrder.Derivation.Canonical.genericFilter p, q ⊩ᶜ φ

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.em {K : Language} [K.Encodable] (p : ConsistentSequent K) (φ : Proposition K) : GenericForces p φ ∨ GenericForces p (∼φ)

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.neg {K : Language} [K.Encodable] {p : ConsistentSequent K} {φ : Proposition K} : GenericForces p (∼φ) ↔ ¬GenericForces p φ

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.verum {K : Language} [K.Encodable] (p : ConsistentSequent K) : GenericForces p ⊤

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.not_falsum {K : Language} [K.Encodable] (p : ConsistentSequent K) : ¬GenericForces p ⊥

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.nrel {K : Language} [K.Encodable] {a✝ : ℕ} {R : K.Rel a✝} {v : Fin a✝ → Semiterm K ℕ 0} {p : ConsistentSequent K} : GenericForces p (Semiformula.nrel R v) ↔ ¬GenericForces p (Semiformula.rel R v)

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.henkin {K : Language} [K.Encodable] {p : ConsistentSequent K} {φ : Semiproposition K 1} : GenericForces p (∃¹ φ) → ∃ (t : Semiterm K ℕ 0), GenericForces p (φ/[t])

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.exs {K : Language} [K.Encodable] {φ : Semiproposition K (0 + 1)} {p : ConsistentSequent K} : GenericForces p (∃¹ φ) ↔ ∃ (t : Semiterm K ℕ 0), GenericForces p (φ/[t])

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.fal {K : Language} [K.Encodable] {φ : Semiproposition K (0 + 1)} {p : ConsistentSequent K} : GenericForces p (∀¹ φ) ↔ ∀ (t : Semiterm K ℕ 0), GenericForces p (φ/[t])

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.and {K : Language} [K.Encodable] {p : ConsistentSequent K} {φ ψ : Proposition K} : GenericForces p (φ ⋏ ψ) ↔ GenericForces p φ ∧ GenericForces p ψ

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.GenericForces.or {K : Language} [K.Encodable] {p : ConsistentSequent K} {φ ψ : Proposition K} : GenericForces p (φ ⋎ ψ) ↔ GenericForces p φ ∨ GenericForces p ψ

@[reducible, inline]

abbrev LO.FirstOrder.Derivation.Canonical.termModelOf {K : Language} [K.Encodable] (p : ConsistentSequent K) : Structure K (Term K ℕ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.termModel_func_def {K : Language} [K.Encodable] {k : ℕ} {p : ConsistentSequent K} (f : K.Func k) (v : Fin k → Term K ℕ) : Structure.func f v = Semiterm.func f v

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.termModel_rel_def {K : Language} [K.Encodable] {k : ℕ} {p : ConsistentSequent K} (R : K.Rel k) (v : Fin k → Term K ℕ) : Structure.rel R v ↔ GenericForces p (Semiformula.rel R v)

@[simp]

theorem LO.FirstOrder.Derivation.Canonical.termModel_val_eq {K : Language} [K.Encodable] {ξ : Type u_1} {n : ℕ} {p : ConsistentSequent K} (t : Semiterm K ξ n) (fv : ξ → Term K ℕ) (bv : Fin n → Term K ℕ) : Semiterm.val bv fv t = (Rew.bind bv fv) t

theorem LO.FirstOrder.Derivation.Canonical.forcing_lemma {K : Language} [K.Encodable] {ξ : Type u_1} {n : ℕ} {p : ConsistentSequent K} (φ : Semiformula K ξ n) {fv : ξ → Term K ℕ} {bv : Fin n → Term K ℕ} : (Semiformula.Eval bv fv) φ ↔ GenericForces p ((Rewriting.app (Rew.bind bv fv)) φ)

theorem LO.FirstOrder.Derivation.Canonical.refl {K : Language} [K.Encodable] (φ : Proposition K) (h : 𝐋𝐊¹ ⊬ ∼φ) : (Semiformula.Evalf fun (x : ℕ) => Semiterm.fvar x) φ

Completeness theorem

theorem LO.FirstOrder.LK.satisfiable_of_irrefutable {L : Language} (σ : Sentence L) (h : 𝐋𝐊¹ ⊬ ∼Rewriting.emb σ) : Satisfiable {σ}

theorem LO.FirstOrder.Theory.small_satisfiable_of_consistent {L : Language} {T : Theory L} : Entailment.Consistent T → Satisfiable T

Completeness theorem (I)

theorem LO.FirstOrder.Theory.satisfiable_iff_consistent {L : Language} {T : Theory L} : Semantics.Satisfiable (Struc L) T ↔ Entailment.Consistent T

theorem LO.FirstOrder.Theory.Proof.complete {L : Language} {T : Theory L} {φ : Sentence L} : T ⊨[Struc L] φ → T ⊢ φ

Completeness theorem (II)

theorem LO.FirstOrder.Theory.Proof.small_complete {L : Language} {T : Theory L} {φ : Sentence L} : Consequence T φ → T ⊢ φ

theorem LO.FirstOrder.Theory.Proof.complete_iff {L : Language} {T : Theory L} {φ : Sentence L} : Consequence T φ ↔ T ⊢ φ

instance LO.FirstOrder.Theory.Proof.isComplete {L : Language} (T : Theory L) : Complete T (Semantics.models (Struc L) T)

theorem LO.FirstOrder.Theory.satisfiable_iff_satisfiable {L : Language} {T : Theory L} : Semantics.Satisfiable (Struc L) T ↔ Satisfiable T

theorem LO.FirstOrder.Theory.consequence_iff_consequence {L : Language} {T : Theory L} {φ : Sentence L} : T ⊨[Struc L] φ ↔ Consequence T φ

Corollaries

theorem LO.FirstOrder.ModelsTheory.of_provably_subtheory {L : Language} (M : Type w) [Nonempty M] [Structure L M] (T U : Theory L) [le : T ⪯ U] (h : M↓[L] ⊧* U) : M↓[L] ⊧* T

theorem LO.FirstOrder.ModelsTheory.of_add_left {L : Language} (M : Type w) [Nonempty M] [Structure L M] (T U : Theory L) [M↓[L] ⊧* T ∪ U] : M↓[L] ⊧* T

theorem LO.FirstOrder.ModelsTheory.of_add_right {L : Language} (M : Type w) [Nonempty M] [Structure L M] (T U : Theory L) [M↓[L] ⊧* T ∪ U] : M↓[L] ⊧* U

theorem LO.FirstOrder.Theory.Proof.complete_on_eq_models {L : Language} [L.Eq] {T : Theory L} [𝗘𝗤 L ⪯ T] (φ : Sentence L) (H : ∀ (M : Type (max u v)) [inst : Nonempty M] [inst_1 : Structure L M] [Structure.Eq L M] [M↓[L] ⊧* T], M↓[L] ⊧ φ) : T ⊢ φ