SearchTree

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

Imported declaration from the Incompleteness formalization.

• 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 (Entailment.Code.axL r v) Γ Γ
• verumRefl {L : Language} {T : Theory L} {Γ : Sequent L} : ⊤ ∉ Γ → Redux T Entailment.Code.verum Γ Γ
• and₁ {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋏ ψ ∈ Γ → Redux T (Entailment.Code.and φ ψ) (φ :: Γ) Γ
• and₂ {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋏ ψ ∈ Γ → Redux T (Entailment.Code.and φ ψ) (ψ :: Γ) Γ
• andRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋏ ψ ∉ Γ → Redux T (Entailment.Code.and φ ψ) Γ Γ
• or {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋎ ψ ∈ Γ → Redux T (Entailment.Code.or φ ψ) (φ :: ψ :: Γ) Γ
• orRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ ψ : SyntacticFormula L} : φ ⋎ ψ ∉ Γ → Redux T (Entailment.Code.or φ ψ) Γ Γ
• all {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} : ∀' φ ∈ Γ → Redux T (Entailment.Code.all φ) (φ/[Semiterm.fvar (newVar Γ)] :: Γ) Γ
• allRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} : ∀' φ ∉ Γ → Redux T (Entailment.Code.all φ) Γ Γ
• ex {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} {t : SyntacticTerm L} : ∃' φ ∈ Γ → Redux T (Entailment.Code.ex φ t) (φ/[t] :: Γ) Γ
• exRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} {t : SyntacticTerm L} : ∃' φ ∉ Γ → Redux T (Entailment.Code.ex φ t) Γ Γ
• id {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticFormula L} (hp : φ ∈ T) : Redux T (Entailment.Code.id φ) (∼Semiformula.close φ :: Γ) Γ
• idRefl {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticFormula L} (hp : φ ∉ T) : Redux T (Entailment.Code.id φ) Γ Γ

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

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

Imported declaration from the Incompleteness formalization.

• redux {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : Theory L} {s : ℕ} {c : Entailment.Code L} : Encodable.decode (Nat.unpair s).1 = some c → ∀ {Δ₂ Δ₁ : Sequent L}, Redux T c Δ₂ Δ₁ → ReduxNat T s Δ₂ Δ₁
• refl {L : Language} [(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 Δ Δ

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

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

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

Imported declaration from the Incompleteness formalization.

• zero {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {T : Theory L} {Γ : Sequent L} : SearchTreeAux T Γ 0 Γ
• succ {L : Language} [(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) Δ₂

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

Imported declaration from the Incompleteness formalization.

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 : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (τ : SearchTree T Γ) : ℕ

Imported declaration from the Incompleteness formalization.

Equations

• τ.rank = τ.fst

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• τ.seq = τ.snd.fst

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

Imported declaration from the Incompleteness formalization.

• intro {L : Language} [(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⟩⟩

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

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

@[instance_reducible]

instance LO.FirstOrder.Completeness.SearchTree.instTop {L : Language} {T : Theory L} {Γ : Sequent L} [(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⟩⟩ }

@[simp]

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

@[simp]

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

noncomputable def LO.FirstOrder.Completeness.SearchTree.recursion {L : Language} {T : Theory L} {Γ : Sequent L} [(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 τ

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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 ⟹ Γ

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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 : Language} {T : Theory L} {Γ : Sequent L} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] (nwf : ¬WellFounded (SearchTree.Lt T Γ)) : ¬Acc (SearchTree.Lt T Γ) ⊤

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

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

theorem LO.FirstOrder.Completeness.chain_spec {L : Language} {T : Theory L} {Γ : Sequent L} [(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)

theorem LO.FirstOrder.Completeness.chain_monotone {L : Language} {T : Theory L} {Γ : Sequent L} [(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

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

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

theorem LO.FirstOrder.Completeness.chainSet_axL {L : Language} {T : Theory L} {Γ : Sequent L} [(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 Γ

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

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

theorem LO.FirstOrder.Completeness.chainSet_all {L : Language} {T : Theory L} {Γ : Sequent L} [(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 Γ

theorem LO.FirstOrder.Completeness.chainSet_ex {L : Language} {T : Theory L} {Γ : Sequent L} [(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 Γ

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[instance_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[instance_reducible]

instance LO.FirstOrder.Completeness.Model.structure {L : Language} [(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.

@[simp]

theorem LO.FirstOrder.Completeness.Model.val {L : Language} {T : Theory L} {Γ : Sequent L} [(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

@[simp]

theorem LO.FirstOrder.Completeness.Model.rel {L : Language} {T : Theory L} {Γ : Sequent L} [(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 Γ

theorem LO.FirstOrder.Completeness.semanticMainLemma_val {L : Language} {T : Theory L} {Γ : Sequent L} [(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) φ

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

theorem LO.FirstOrder.Completeness.semanticMainLemmaTop {L : Language} {T : Theory L} {Γ : Sequent L} [(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) φ