inductive LO.FirstOrder.Completeness.Redux {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) : LO.FirstOrder.System.Code L → LO.FirstOrder.Sequent L → LO.FirstOrder.Sequent L → Prop

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

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

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

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

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

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

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

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

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

Equations

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

@[reducible, inline]

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

Equations

• τ.rank = τ.fst

@[reducible, inline]

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

Equations

• τ.seq = τ.snd.fst

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

• intro: ∀ {L : LO.FirstOrder.Language} [inst : (k : ℕ) → DecidableEq (L.Func k)] [inst_1 : (k : ℕ) → DecidableEq (L.Rel k)] [inst_2 : (k : ℕ) → Encodable (L.Func k)] [inst_3 : (k : ℕ) → Encodable (L.Rel k)] {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {s : ℕ} {Δ₂ Δ₁ : LO.FirstOrder.Sequent L} (a : LO.FirstOrder.Completeness.SearchTreeAux T Γ s Δ₁) (r : LO.FirstOrder.Completeness.ReduxNat T s Δ₂ Δ₁), LO.FirstOrder.Completeness.SearchTree.Lt T Γ ⟨s + 1, ⟨Δ₂, a.succ r⟩⟩ ⟨s, ⟨Δ₁, a⟩⟩

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

theorem LO.FirstOrder.Completeness.Model.val {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.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 → LO.FirstOrder.SyntacticTerm L} {ε : ℕ → LO.FirstOrder.Completeness.Model T Γ} (t : LO.FirstOrder.SyntacticSemiterm L n) : LO.FirstOrder.Semiterm.val (LO.FirstOrder.Completeness.Model.structure T Γ) e ε t = (LO.FirstOrder.Rew.bind e ε) t

@[simp]

theorem LO.FirstOrder.Completeness.Model.rel {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.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 → LO.FirstOrder.SyntacticTerm L) : LO.FirstOrder.Structure.rel r v ↔ LO.FirstOrder.Semiformula.nrel r v ∈ LO.FirstOrder.Completeness.chainSet T Γ

@[irreducible]

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

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

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