Foundation.FirstOrder.Completeness.SearchTree

inductive LO.FirstOrder.Completeness.Redux {L : Language} (T : Theory L) :

System.Code L → Sequent L → Sequent L → Prop

axLRefl {L : Language} {T : Theory L} {Γ : Sequent L} {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ℕ 0) : Semiformula.rel r v ∉ Γ ∨ Semiformula.nrel r v ∉ Γ → Redux T (System.Code.axL r v) Γ Γ
verumRefl {L : Language} {T : Theory L} {Γ : Sequent L} : ⊤ ∉ Γ → Redux T System.Code.verum Γ Γ
and₁ {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋏ ψ ∈ Γ → Redux T (System.Code.and φ ψ) (φ :: Γ) Γ
and₂ {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋏ ψ ∈ Γ → Redux T (System.Code.and φ ψ) (ψ :: Γ) Γ
andRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋏ ψ ∉ Γ → Redux T (System.Code.and φ ψ) Γ Γ
or {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋎ ψ ∈ Γ → Redux T (System.Code.or φ ψ) (φ :: ψ :: Γ) Γ
orRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋎ ψ ∉ Γ → Redux T (System.Code.or φ ψ) Γ Γ
all {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} : ∀' φ ∈ Γ → Redux T (System.Code.all φ) (φ/[Semiterm.fvar (newVar Γ)] :: Γ) Γ
allRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} : ∀' φ ∉ Γ → Redux T (System.Code.all φ) Γ Γ
ex {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} {t : SyntacticTerm L} : ∃' φ ∈ Γ → Redux T (System.Code.ex φ t) (φ/[t] :: Γ) Γ
exRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} {t : SyntacticTerm L} : ∃' φ ∉ Γ → Redux T (System.Code.ex φ t) Γ Γ
id {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticFormula L} (hp : φ ∈ T) : Redux T (System.Code.id φ) (∼Semiformula.close φ :: Γ) Γ
idRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticFormula L} (hp : φ ∉ T) : Redux T (System.Code.id φ) Γ Γ

theorem LO.FirstOrder.Completeness.Redux.antimonotone {L : Language} {T : Theory L} {c : System.Code L} {Δ₂ Δ₁ : Sequent L} (h : Redux T c Δ₂ Δ₁) :

Δ₁ ⊆ Δ₂

source

inductive LO.FirstOrder.Completeness.ReduxNat {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (T : Theory L) (s : ℕ) :

Sequent L → Sequent L → Prop

redux {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : Theory L} {s : ℕ} {c : System.Code L} : Encodable.decode (Nat.unpair s).1 = some c → ∀ {Δ₂ Δ₁ : Sequent L}, Redux T c Δ₂ Δ₁ → ReduxNat T s Δ₂ Δ₁
refl {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : Theory L} {s : ℕ} : Encodable.decode (Nat.unpair s).1 = none → ∀ (Δ : Sequent L), ReduxNat T s Δ Δ

source

theorem LO.FirstOrder.Completeness.ReduxNat.antimonotone {L : Language} {T : Theory L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {s : ℕ} {Δ₂ Δ₁ : Sequent L} (h : ReduxNat T s Δ₂ Δ₁) :

Δ₁ ⊆ Δ₂

source

theorem LO.FirstOrder.Completeness.ReduxNat.toRedux {L : Language} {T : Theory L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {c : System.Code L} {i : ℕ} {Δ₂ Δ₁ : Sequent L} (h : ReduxNat T (Nat.pair (Encodable.encode c) i) Δ₂ Δ₁) :

Redux T c Δ₂ Δ₁

source

inductive LO.FirstOrder.Completeness.SearchTreeAux {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (T : Theory L) (Γ : Sequent L) :

ℕ → Sequent L → Type u

zero {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : Theory L} {Γ : Sequent L} : SearchTreeAux T Γ 0 Γ
succ {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : Theory L} {Γ : Sequent L} {s : ℕ} {Δ₁ Δ₂ : Sequent L} : SearchTreeAux T Γ s Δ₁ → ReduxNat T s Δ₂ Δ₁ → SearchTreeAux T Γ (s + 1) Δ₂

source

def LO.FirstOrder.Completeness.SearchTree {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (T : Theory L) (Γ : Sequent L) :

Type u

Equations

LO.FirstOrder.Completeness.SearchTree T Γ = ((s : ℕ) × (Δ : LO.FirstOrder.Sequent L) × LO.FirstOrder.Completeness.SearchTreeAux T Γ s Δ)

Instances For

LO.FirstOrder.Completeness.SearchTree.instTop

source

@[reducible, inline]

abbrev LO.FirstOrder.Completeness.SearchTree.rank {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (τ : SearchTree T Γ) :

ℕ

Equations

τ.rank = τ.fst

source

@[reducible, inline]

abbrev LO.FirstOrder.Completeness.SearchTree.seq {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (τ : SearchTree T Γ) :

Sequent L

Equations

τ.seq = τ.snd.fst

source

inductive LO.FirstOrder.Completeness.SearchTree.Lt {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (T : Theory L) (Γ : Sequent L) :

SearchTree T Γ → SearchTree T Γ → Prop

intro {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : Theory L} {Γ : Sequent L} {s : ℕ} {Δ₂ Δ₁ : Sequent L} (a : SearchTreeAux T Γ s Δ₁) (r : ReduxNat T s Δ₂ Δ₁) : Lt T Γ ⟨s + 1, ⟨Δ₂, a.succ r⟩⟩ ⟨s, ⟨Δ₁, a⟩⟩

source

theorem LO.FirstOrder.Completeness.SearchTree.rank_of_lt {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {τ₁ τ₂ : SearchTree T Γ} (h : Lt T Γ τ₂ τ₁) :

τ₂.rank = τ₁.rank + 1

source

theorem LO.FirstOrder.Completeness.SearchTree.seq_of_lt {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {τ₁ τ₂ : SearchTree T Γ} (h : Lt T Γ τ₂ τ₁) :

ReduxNat T τ₁.rank τ₂.seq τ₁.seq

source

instance LO.FirstOrder.Completeness.SearchTree.instTop {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] :

Top (SearchTree T Γ)

Equations

LO.FirstOrder.Completeness.SearchTree.instTop = { top := ⟨0, ⟨Γ, LO.FirstOrder.Completeness.SearchTreeAux.zero⟩⟩ }

source

@[simp]

theorem LO.FirstOrder.Completeness.SearchTree.rank_top {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] :

⊤.rank = 0

source

@[simp]

theorem LO.FirstOrder.Completeness.SearchTree.seq_top {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] :

⊤.seq = Γ

source

noncomputable def LO.FirstOrder.Completeness.SearchTree.recursion {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (wf : WellFounded (Lt T Γ)) {C : SearchTree T Γ → Sort v} (τ : SearchTree T Γ) (h : (τ₁ : SearchTree T Γ) → ((τ₂ : SearchTree T Γ) → Lt T Γ τ₂ τ₁ → C τ₂) → C τ₁) :

C τ

Equations

LO.FirstOrder.Completeness.SearchTree.recursion wf τ h = wf.fix h τ

source

noncomputable def LO.FirstOrder.Completeness.syntacticMainLemma {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (wf : WellFounded (SearchTree.Lt T Γ)) (φ : SearchTree T Γ) :

T ⟹ φ.seq

Equations

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

source

noncomputable def LO.FirstOrder.Completeness.syntacticMainLemmaTop {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (wf : WellFounded (SearchTree.Lt T Γ)) :

T ⟹ Γ

Equations

LO.FirstOrder.Completeness.syntacticMainLemmaTop wf = LO.FirstOrder.Completeness.syntacticMainLemma wf ⊤

source

noncomputable def LO.FirstOrder.Completeness.chainU {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (T : Theory L) (Γ : Sequent L) :

ℕ → SearchTree T Γ

Equations

LO.FirstOrder.Completeness.chainU T Γ = descendingChain (LO.FirstOrder.Completeness.SearchTree.Lt T Γ) ⊤

source

noncomputable def LO.FirstOrder.Completeness.chain {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (T : Theory L) (Γ : Sequent L) (s : ℕ) :

Sequent L

Equations

LO.FirstOrder.Completeness.chain T Γ s = (LO.FirstOrder.Completeness.chainU T Γ s).seq

source

def LO.FirstOrder.Completeness.chainSet {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (T : Theory L) (Γ : Sequent L) :

Set (SyntacticFormula L)

Equations

LO.FirstOrder.Completeness.chainSet T Γ = ⋃ (s : ℕ), {x : LO.FirstOrder.SyntacticFormula L | x ∈ LO.FirstOrder.Completeness.chain T Γ s}

source

theorem LO.FirstOrder.Completeness.top_inaccessible {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) :

¬Acc (SearchTree.Lt T Γ) ⊤

source

theorem LO.FirstOrder.Completeness.chainU_spec {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) :

IsInfiniteDescendingChain (SearchTree.Lt T Γ) (chainU T Γ)

source

theorem LO.FirstOrder.Completeness.chainU_val_fst_eq {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) (s : ℕ) :

(chainU T Γ s).rank = s

source

theorem LO.FirstOrder.Completeness.chain_spec {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) (s : ℕ) :

ReduxNat T s (chain T Γ (s + 1)) (chain T Γ s)

source

theorem LO.FirstOrder.Completeness.chain_monotone {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) {s u : ℕ} (h : s ≤ u) :

chain T Γ s ⊆ chain T Γ u

source

theorem LO.FirstOrder.Completeness.chain_spec' {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) (c : System.Code L) (i : ℕ) :

Redux T c (chain T Γ (Nat.pair (Encodable.encode c) i + 1)) (chain T Γ (Nat.pair (Encodable.encode c) i))

source

theorem LO.FirstOrder.Completeness.chainSet_verum {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) :

⊤ ∉ chainSet T Γ

source

theorem LO.FirstOrder.Completeness.chainSet_axL {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) {k : ℕ} (r : L.Rel k) (v : Fin k → SyntacticTerm L) :

Semiformula.rel r v ∉ chainSet T Γ ∨ Semiformula.nrel r v ∉ chainSet T Γ

source

theorem LO.FirstOrder.Completeness.chainSet_and {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) {φ ψ : SyntacticFormula L} (h : φ ⋏ ψ ∈ chainSet T Γ) :

φ ∈ chainSet T Γ ∨ ψ ∈ chainSet T Γ

source

theorem LO.FirstOrder.Completeness.chainSet_or {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) {φ ψ : SyntacticFormula L} (h : φ ⋎ ψ ∈ chainSet T Γ) :

φ ∈ chainSet T Γ ∧ ψ ∈ chainSet T Γ

source

theorem LO.FirstOrder.Completeness.chainSet_all {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) {φ : SyntacticSemiformula L 1} (h : ∀' φ ∈ chainSet T Γ) :

∃ (t : Semiterm L ℕ 0), φ/[t] ∈ chainSet T Γ

source

theorem LO.FirstOrder.Completeness.chainSet_ex {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) {φ : SyntacticSemiformula L 1} (h : ∃' φ ∈ chainSet T Γ) (t : Semiterm L ℕ 0) :

φ/[t] ∈ chainSet T Γ

source

theorem LO.FirstOrder.Completeness.chainSet_id {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) {φ : SyntacticFormula L} (h : φ ∈ T) :

∼Semiformula.close φ ∈ chainSet T Γ

source

@[reducible, inline]

abbrev LO.FirstOrder.Completeness.Model {L : Language} (T : Theory L) (Γ : Sequent L) :

Type u

Equations

LO.FirstOrder.Completeness.Model T Γ = LO.FirstOrder.SyntacticTerm L

Instances For

source

instance LO.FirstOrder.Completeness.instInhabitedModel {L : Language} {T : Theory L} {Γ : Sequent L} :

Inhabited (Model T Γ)

Equations

LO.FirstOrder.Completeness.instInhabitedModel = { default := default }

source

def LO.FirstOrder.Completeness.Model.equiv {L : Language} {T : Theory L} {Γ : Sequent L} :

Model T Γ ≃ SyntacticTerm L

Equations

LO.FirstOrder.Completeness.Model.equiv = Equiv.refl (LO.FirstOrder.Completeness.Model T Γ)

source

instance LO.FirstOrder.Completeness.Model.structure {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (T : Theory L) (Γ : Sequent L) :

Structure L (Model T Γ)

Equations

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

source

@[simp]

theorem LO.FirstOrder.Completeness.Model.val {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {n : ℕ} {e : Fin n → SyntacticTerm L} {ε : ℕ → Model T Γ} (t : SyntacticSemiterm L n) :

Semiterm.val («structure» T Γ) e ε t = (Rew.bind e ε) t

source

@[simp]

theorem LO.FirstOrder.Completeness.Model.rel {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {k : ℕ} (r : L.Rel k) (v : Fin k → SyntacticTerm L) :

Structure.rel r v ↔ Semiformula.nrel r v ∈ chainSet T Γ

source

@[irreducible]

theorem LO.FirstOrder.Completeness.semanticMainLemma_val {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) (φ : SyntacticFormula L) :

φ ∈ chainSet T Γ → ¬(Semiformula.Evalf (Model.structure T Γ) Semiterm.fvar) φ

source

theorem LO.FirstOrder.Completeness.Model.models {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) :

Model T Γ ⊧ₘ* T

source

theorem LO.FirstOrder.Completeness.semanticMainLemmaTop {L : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) {φ : SyntacticFormula L} (h : φ ∈ Γ) :

¬(Semiformula.Evalf (Model.structure T Γ) Semiterm.fvar) φ