inductive
LO.FirstOrder.Completeness.Redux
{L : LO.FirstOrder.Language}
(T : LO.FirstOrder.Theory L)
:
- 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} {p q : LO.FirstOrder.SyntacticFormula L}, p ⋏ q ∈ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.and p q) (p :: Γ) Γ
- and₂: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p q : LO.FirstOrder.SyntacticFormula L}, p ⋏ q ∈ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.and p q) (q :: Γ) Γ
- andRefl: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p q : LO.FirstOrder.SyntacticFormula L}, p ⋏ q ∉ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.and p q) Γ Γ
- or: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p q : LO.FirstOrder.SyntacticFormula L}, p ⋎ q ∈ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.or p q) (p :: q :: Γ) Γ
- orRefl: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p q : LO.FirstOrder.SyntacticFormula L}, p ⋎ q ∉ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.or p q) Γ Γ
- all: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p : LO.FirstOrder.SyntacticSemiformula L 1}, ∀' p ∈ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.all p) ((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.fvar (LO.FirstOrder.newVar Γ)]).hom p :: Γ) Γ
- allRefl: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p : LO.FirstOrder.SyntacticSemiformula L 1}, ∀' p ∉ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.all p) Γ Γ
- ex: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p : LO.FirstOrder.SyntacticSemiformula L 1} {t : LO.FirstOrder.SyntacticTerm L}, ∃' p ∈ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.ex p t) ((LO.FirstOrder.Rew.substs ![t]).hom p :: Γ) Γ
- exRefl: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p : LO.FirstOrder.SyntacticSemiformula L 1} {t : LO.FirstOrder.SyntacticTerm L}, ∃' p ∉ Γ → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.ex p t) Γ Γ
- id: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p : LO.FirstOrder.SyntacticFormula L}, p ∈ T → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.id p) (∼LO.FirstOrder.Semiformula.close p :: Γ) Γ
- idRefl: ∀ {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {Γ : LO.FirstOrder.Sequent L} {p : LO.FirstOrder.SyntacticFormula L}, p ∉ T → LO.FirstOrder.Completeness.Redux T (LO.FirstOrder.System.Code.id p) Γ Γ
Instances For
inductive
LO.FirstOrder.Completeness.ReduxNat
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
(T : LO.FirstOrder.Theory L)
(s : ℕ)
:
- redux: ∀ {L : LO.FirstOrder.Language} [inst : (k : ℕ) → Encodable (L.Func k)] [inst_1 : (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 : ℕ) → Encodable (L.Func k)] [inst_1 : (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 Δ Δ
Instances For
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}
{Δ₁ : LO.FirstOrder.Sequent L}
(h : LO.FirstOrder.Completeness.Redux T c Δ₂ Δ₁)
:
Δ₁ ⊆ Δ₂
theorem
LO.FirstOrder.Completeness.ReduxNat.antimonotone
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{s : ℕ}
{Δ₂ : LO.FirstOrder.Sequent L}
{Δ₁ : LO.FirstOrder.Sequent L}
(h : LO.FirstOrder.Completeness.ReduxNat T s Δ₂ Δ₁)
:
Δ₁ ⊆ Δ₂
theorem
LO.FirstOrder.Completeness.ReduxNat.toRedux
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{c : LO.FirstOrder.System.Code L}
{i : ℕ}
{Δ₂ : LO.FirstOrder.Sequent L}
{Δ₁ : 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 : ℕ) → 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 : ℕ) → Encodable (L.Func k)] → [inst_1 : (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 : ℕ) → Encodable (L.Func k)] → [inst_1 : (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) Δ₂
Instances For
def
LO.FirstOrder.Completeness.SearchTree
{L : LO.FirstOrder.Language}
[(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 Δ)
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Completeness.SearchTree.rank
{L : LO.FirstOrder.Language}
[(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
- τ.rank = τ.fst
Instances For
@[reducible, inline]
abbrev
LO.FirstOrder.Completeness.SearchTree.seq
{L : LO.FirstOrder.Language}
[(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
- τ.seq = τ.snd.fst
Instances For
inductive
LO.FirstOrder.Completeness.SearchTree.Lt
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
(T : LO.FirstOrder.Theory L)
(Γ : LO.FirstOrder.Sequent L)
:
- intro: ∀ {L : LO.FirstOrder.Language} [inst : (k : ℕ) → Encodable (L.Func k)] [inst_1 : (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⟩⟩
Instances For
theorem
LO.FirstOrder.Completeness.SearchTree.rank_of_lt
{L : LO.FirstOrder.Language}
[(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 Γ}
(h : LO.FirstOrder.Completeness.SearchTree.Lt T Γ τ₂ τ₁)
:
theorem
LO.FirstOrder.Completeness.SearchTree.seq_of_lt
{L : LO.FirstOrder.Language}
[(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 Γ}
(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}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
:
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}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
:
@[simp]
theorem
LO.FirstOrder.Completeness.SearchTree.seq_top
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
:
noncomputable def
LO.FirstOrder.Completeness.SearchTree.recursion
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(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 τ
Instances For
noncomputable def
LO.FirstOrder.Completeness.syntacticMainLemma
{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}
(wf : WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
(p : LO.FirstOrder.Completeness.SearchTree T Γ)
:
T ⟹ p.seq
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
LO.FirstOrder.Completeness.syntacticMainLemmaTop
{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}
(wf : WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
:
T ⟹ Γ
Equations
Instances For
noncomputable def
LO.FirstOrder.Completeness.chainU
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
(T : LO.FirstOrder.Theory L)
(Γ : LO.FirstOrder.Sequent L)
:
Equations
Instances For
noncomputable def
LO.FirstOrder.Completeness.chain
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
(T : LO.FirstOrder.Theory L)
(Γ : LO.FirstOrder.Sequent L)
(s : ℕ)
:
Equations
- LO.FirstOrder.Completeness.chain T Γ s = (LO.FirstOrder.Completeness.chainU T Γ s).seq
Instances For
def
LO.FirstOrder.Completeness.chainSet
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
(T : LO.FirstOrder.Theory L)
(Γ : LO.FirstOrder.Sequent L)
:
Equations
- LO.FirstOrder.Completeness.chainSet T Γ = ⋃ (s : ℕ), {x : LO.FirstOrder.SyntacticFormula L | x ∈ LO.FirstOrder.Completeness.chain T Γ s}
Instances For
theorem
LO.FirstOrder.Completeness.top_inaccessible
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
:
theorem
LO.FirstOrder.Completeness.chainU_spec
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
:
theorem
LO.FirstOrder.Completeness.chainU_val_fst_eq
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(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}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(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}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
{s : ℕ}
{u : ℕ}
(h : s ≤ u)
:
theorem
LO.FirstOrder.Completeness.chain_spec'
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(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}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
:
theorem
LO.FirstOrder.Completeness.chainSet_axL
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
{k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.SyntacticTerm L)
:
theorem
LO.FirstOrder.Completeness.chainSet_and
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
{p : LO.FirstOrder.SyntacticFormula L}
{q : LO.FirstOrder.SyntacticFormula L}
(h : p ⋏ q ∈ LO.FirstOrder.Completeness.chainSet T Γ)
:
theorem
LO.FirstOrder.Completeness.chainSet_or
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
{p : LO.FirstOrder.SyntacticFormula L}
{q : LO.FirstOrder.SyntacticFormula L}
(h : p ⋎ q ∈ LO.FirstOrder.Completeness.chainSet T Γ)
:
theorem
LO.FirstOrder.Completeness.chainSet_all
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
{p : LO.FirstOrder.SyntacticSemiformula L 1}
(h : ∀' p ∈ LO.FirstOrder.Completeness.chainSet T Γ)
:
∃ (t : LO.FirstOrder.Semiterm L ℕ 0), (LO.FirstOrder.Rew.substs ![t]).hom p ∈ LO.FirstOrder.Completeness.chainSet T Γ
theorem
LO.FirstOrder.Completeness.chainSet_ex
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
{p : LO.FirstOrder.SyntacticSemiformula L 1}
(h : ∃' p ∈ LO.FirstOrder.Completeness.chainSet T Γ)
(t : LO.FirstOrder.Semiterm L ℕ 0)
:
(LO.FirstOrder.Rew.substs ![t]).hom p ∈ LO.FirstOrder.Completeness.chainSet T Γ
theorem
LO.FirstOrder.Completeness.chainSet_id
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
{p : LO.FirstOrder.SyntacticFormula L}
(h : p ∈ T)
:
@[reducible, inline]
abbrev
LO.FirstOrder.Completeness.Model
{L : LO.FirstOrder.Language}
(T : LO.FirstOrder.Theory L)
(Γ : LO.FirstOrder.Sequent L)
:
Type u
Equations
Instances For
instance
LO.FirstOrder.Completeness.instInhabitedModel
{L : LO.FirstOrder.Language}
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
:
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}
:
Equations
- LO.FirstOrder.Completeness.Model.equiv = Equiv.refl (LO.FirstOrder.Completeness.Model T Γ)
Instances For
instance
LO.FirstOrder.Completeness.Model.structure
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
(T : LO.FirstOrder.Theory L)
(Γ : LO.FirstOrder.Sequent L)
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LO.FirstOrder.Completeness.Model.val
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
{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}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
{k : ℕ}
(r : L.Rel k)
(v : Fin k → LO.FirstOrder.SyntacticTerm L)
:
@[irreducible]
theorem
LO.FirstOrder.Completeness.semanticMainLemma_val
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
(p : LO.FirstOrder.SyntacticFormula L)
:
p ∈ LO.FirstOrder.Completeness.chainSet T Γ →
¬(LO.FirstOrder.Semiformula.Evalf (LO.FirstOrder.Completeness.Model.structure T Γ) LO.FirstOrder.Semiterm.fvar) p
theorem
LO.FirstOrder.Completeness.Model.models
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
:
theorem
LO.FirstOrder.Completeness.semanticMainLemmaTop
{L : LO.FirstOrder.Language}
[(k : ℕ) → Encodable (L.Func k)]
[(k : ℕ) → Encodable (L.Rel k)]
{T : LO.FirstOrder.Theory L}
{Γ : LO.FirstOrder.Sequent L}
(nwf : ¬WellFounded (LO.FirstOrder.Completeness.SearchTree.Lt T Γ))
{p : LO.FirstOrder.SyntacticFormula L}
(h : p ∈ Γ)
:
¬(LO.FirstOrder.Semiformula.Evalf (LO.FirstOrder.Completeness.Model.structure T Γ) LO.FirstOrder.Semiterm.fvar) p