MathematicalLogic.FirstOrder.Completeness.Henkin

source

theorem Set.decompose_subset_union {α : Type u_1} {s₁ s₂ s₃ : Set α} :

s₁ ⊆ s₂ ∪ s₃ → ∃ (s₄ : Set α) (s₅ : Set α), s₁ = s₄ ∪ s₅ ∧ s₄ ⊆ s₂ ∧ s₅ ⊆ s₃

source

def Fin.embedAt {n : ℕ} (k : ℕ) :

Fin (n + k + 1)

Equations

Fin.embedAt 0 = 0
Fin.embedAt k.succ = (Fin.embedAt k).succ

Instances For

source

def Fin.insertAt {n : ℕ} (k : ℕ) :

Fin (n + k) → Fin (n + k + 1)

Equations

Fin.insertAt 0 x_2 = x_2.succ
Fin.insertAt k.succ x_2 = Fin.cases 0 (fun (x : Fin (n.add k)) => (Fin.insertAt k x).succ) x_2

Instances For

source

theorem Fin.embedAt_or_insertAt {n k : ℕ} (x : Fin (n + k + 1)) :

x = embedAt k ∨ ∃ (y : Fin (n + k)), x = insertAt k y

source

def FirstOrder.Language.Term.consts {L : Language} {n : ℕ} :

L.Term n → Set L.Const

Equations

(#a).consts = ∅
(c ⬝ᶠ a).consts = {c}
(a ⬝ᶠ v).consts = ⋃ (i : Fin (n_1 + 1)), (v i).consts

Instances For

source

def FirstOrder.Language.Formula.consts {L : Language} {n : ℕ} :

L.Formula n → Set L.Const

Equations

(a ⬝ʳ v).consts = ⋃ (i : Fin m), (v i).consts
(t₁ ≐ t₂).consts = t₁.consts ∪ t₂.consts
FirstOrder.Language.Formula.false.consts = ∅
(p.imp q).consts = p.consts ∪ q.consts
(∀' p).consts = p.consts

Instances For

source

theorem FirstOrder.Language.Formula.consts_neg {L : Language} {n : ℕ} {p : L.Formula n} :

(~ p).consts = p.consts

source

theorem FirstOrder.Language.Formula.consts_ex {L✝ : Language} {a✝ : ℕ} {p : L✝.Formula (a✝ + 1)} :

(∃' p).consts = p.consts

source

theorem FirstOrder.Language.Term.consts_of_subst {L✝ : Language} {n✝ : ℕ} {t : L✝.Term n✝} {m✝ : ℕ} {σ : L✝.Subst n✝ m✝} :

t[σ]ₜ.consts = t.consts ∪ ⋃ x ∈ t.vars, (σ x).consts

source

theorem FirstOrder.Language.Formula.consts_of_subst {L : Language} {n m : ℕ} {p : L.Formula n} {σ : L.Subst n m} :

p[σ]ₚ.consts = p.consts ∪ ⋃ x ∈ p.free, (σ x).consts

source

def FirstOrder.Language.Subst.singleAt {L : Language} {n : ℕ} (k : ℕ) (t : L.Term n) :

L.Subst (n + k + 1) (n + k)

Equations

FirstOrder.Language.Subst.singleAt 0 x✝ = ↦ₛ x✝
FirstOrder.Language.Subst.singleAt k.succ x✝ = ⇑ₛ(FirstOrder.Language.Subst.singleAt k x✝)

Instances For

source

theorem FirstOrder.Language.Subst.singleAt_const_app_embedAt {L : Language} {k n : ℕ} {c : L.Const} :

singleAt k (c ⬝ᶠ []ᵥ) (Fin.embedAt k) = c ⬝ᶠ []ᵥ

source

theorem FirstOrder.Language.Subst.singleAt_app_insertAt {k : ℕ} {L✝ : Language} {n✝ : ℕ} {t : L✝.Term n✝} {x : Fin (n✝ + k)} :

singleAt k t (Fin.insertAt k x) = #x

source

def FirstOrder.Language.Subst.shiftAt {L : Language} {n : ℕ} (k : ℕ) :

L.Subst (n + k) (n + k + 1)

Equations

Instances For

source

theorem FirstOrder.Language.Subst.shiftAt_app {L : Language} {k a✝ : ℕ} {x : Fin (a✝ + k)} :

shiftAt k x = #(Fin.insertAt k x)

source

theorem FirstOrder.Language.Subst.shiftAt_comp_singleAt {k : ℕ} {L✝ : Language} {n✝ : ℕ} {t : L✝.Term n✝} :

shiftAt k ∘ₛ singleAt k t = idₛ

source

def FirstOrder.Language.Subst.insertAt {L : Language} {n m : ℕ} (k : ℕ) :

L.Subst (n + k) m → (t : L.Term m) → L.Subst (n + k + 1) m

Equations

FirstOrder.Language.Subst.insertAt 0 σ x✝ = x✝ ∷ᵥ σ
FirstOrder.Language.Subst.insertAt k.succ σ x✝ = Vec.head σ ∷ᵥ FirstOrder.Language.Subst.insertAt k (Vec.tail σ) x✝

Instances For

source

theorem FirstOrder.Language.Subst.insertAt_app_embedAt {k : ℕ} {L✝ : Language} {a✝ m✝ : ℕ} {σ : L✝.Subst (a✝ + k) m✝} {t : L✝.Term m✝} :

insertAt k σ t (Fin.embedAt k) = t

source

theorem FirstOrder.Language.Subst.insertAt_app_insertAt {k : ℕ} {L✝ : Language} {a✝ m✝ : ℕ} {σ : L✝.Subst (a✝ + k) m✝} {t : L✝.Term m✝} {x : Fin (a✝ + k)} :

insertAt k σ t (Fin.insertAt k x) = σ x

source

noncomputable def FirstOrder.Language.Term.invConst {L : Language} {n : ℕ} (k : ℕ) :

L.Term (n + k) → L.Const → L.Term (n + k + 1)

Equations

FirstOrder.Language.Term.invConst k (#x_2) x✝ = #(Fin.insertAt k x_2)
FirstOrder.Language.Term.invConst k (f ⬝ᶠ a) x✝ = if f = x✝ then #(Fin.embedAt k) else f ⬝ᶠ []ᵥ
FirstOrder.Language.Term.invConst k (f ⬝ᶠ v) x✝ = f ⬝ᶠ fun (i : Fin (n_1 + 1)) => FirstOrder.Language.Term.invConst k (v i) x✝

Instances For

source

theorem FirstOrder.Language.Term.subst_singleAt_invConst {L : Language} {n k : ℕ} {c : L.Const} {t : L.Term (n + k + 1)} (h : c ∉ t.consts) :

invConst k t[Subst.singleAt k (c ⬝ᶠ []ᵥ)]ₜ c = t

source

theorem FirstOrder.Language.Term.invConst_eq_shiftAt {L : Language} {n k : ℕ} {c : L.Const} {t : L.Term (n + k)} (h : c ∉ t.consts) :

invConst k t c = t[Subst.shiftAt k]ₜ

source

theorem FirstOrder.Language.Term.invConst_subst {L : Language} {n k n' k' : ℕ} {c : L.Const} {t : L.Term (n + k)} {σ : L.Subst (n + k) (n' + k')} :

invConst k' t[σ]ₜ c = (invConst k t c)[Subst.insertAt k ((fun (x : L.Term (n' + k')) => invConst k' x c) ∘ σ) #(Fin.embedAt k')]ₜ

source

theorem FirstOrder.Language.Term.invConst_shift {L : Language} {n k : ℕ} {c : L.Const} {t : L.Term (n + k)} :

invConst (k + 1) (↑ₜt) c = ↑ₜ(invConst k t c)

source

@[irreducible]

noncomputable def FirstOrder.Language.Formula.invConst {L : Language} {n : ℕ} (k : ℕ) :

L.Formula (n + k) → L.Const → L.Formula (n + k + 1)

Equations

FirstOrder.Language.Formula.invConst k (r ⬝ʳ v) x✝ = r ⬝ʳ fun (i : Fin m) => FirstOrder.Language.Term.invConst k (v i) x✝
FirstOrder.Language.Formula.invConst k (t₁ ≐ t₂) x✝ = FirstOrder.Language.Term.invConst k t₁ x✝ ≐ FirstOrder.Language.Term.invConst k t₂ x✝
FirstOrder.Language.Formula.invConst k FirstOrder.Language.Formula.false x✝ = ⊥
FirstOrder.Language.Formula.invConst k (p.imp q) x✝ = FirstOrder.Language.Formula.invConst k p x✝ ⇒ FirstOrder.Language.Formula.invConst k q x✝
FirstOrder.Language.Formula.invConst k (∀' p) x✝ = ∀' FirstOrder.Language.Formula.invConst (k + 1) p x✝

Instances For

source

@[simp]

theorem FirstOrder.Language.Formula.invConst_false {L : Language} {n k : ℕ} {c : L.Const} :

invConst k ⊥ c = ⊥

source

@[simp]

theorem FirstOrder.Language.Formula.invConst_imp {L : Language} {n k : ℕ} {p q : L.Formula (n + k)} {c : L.Const} :

invConst k (p ⇒ q) c = invConst k p c ⇒ invConst k q c

source

@[simp]

theorem FirstOrder.Language.Formula.invConst_neg {L : Language} {n k : ℕ} {p : L.Formula (n + k)} {c : L.Const} :

invConst k (~ p) c = ~ invConst k p c

source

theorem FirstOrder.Language.Formula.invConst_andN {L : Language} {n k m : ℕ} {c : L.Const} {v : Vec (L.Formula (n + k)) m} :

invConst k (⋀ (i : Fin m), v i) c = ⋀ (i : Fin m), invConst k (v i) c

source

@[irreducible]

theorem FirstOrder.Language.Formula.subst_singleAt_invConst {L : Language} {n k : ℕ} {c : L.Const} {p : L.Formula (n + k + 1)} (h : c ∉ p.consts) :

invConst k p[Subst.singleAt k (c ⬝ᶠ []ᵥ)]ₚ c = p

source

@[irreducible]

theorem FirstOrder.Language.Formula.invConst_eq_shiftAt {L : Language} {n k : ℕ} {c : L.Const} {p : L.Formula (n + k)} (h : c ∉ p.consts) :

invConst k p c = p[Subst.shiftAt k]ₚ

source

@[irreducible]

theorem FirstOrder.Language.Formula.invConst_subst {L : Language} {n k n' k' : ℕ} {c : L.Const} {p : L.Formula (n + k)} {σ : L.Subst (n + k) (n' + k')} :

invConst k' p[σ]ₚ c = (invConst k p c)[Subst.insertAt k ((fun (x : L.Term (n' + k')) => Term.invConst k' x c) ∘ σ) #(Fin.embedAt k')]ₚ

source

theorem FirstOrder.Language.Formula.invConst_shift {L : Language} {n k : ℕ} {c : L.Const} {p : L.Formula (n + k)} :

invConst (k + 1) (↑ₚp) c = ↑ₚ(invConst k p c)

source

theorem FirstOrder.Language.Formula.invConst_subst_single {L : Language} {n k : ℕ} {c : L.Const} {p : L.Formula (n + k + 1)} {t : L.Term (n + k)} :

invConst k p[↦ₛ t]ₚ c = (invConst (k + 1) p c)[↦ₛ Term.invConst k t c]ₚ

source

@[irreducible]

theorem FirstOrder.Language.Axiom.inv_const {L : Language} {n k : ℕ} {Γ : L.FormulaSet (n + k + 1)} {c : L.Const} {p : L.Formula (n + k)} :

p ∈ L.Axiom → Γ ⊢ Formula.invConst k p c

source

theorem FirstOrder.Language.Proof.inv_const {L : Language} {n k : ℕ} {Γ : L.FormulaSet (n + k)} {c : L.Const} {p : L.Formula (n + k)} (h₁ : ∀ p ∈ Γ, c ∉ p.consts) :

Γ ⊢ p → (fun (x : L.Formula (n + k)) => x[Subst.shiftAt k]ₚ) '' Γ ⊢ Formula.invConst k p c

source

theorem FirstOrder.Language.Proof.const_generalization {L : Language} {n : ℕ} {c : L.Const} {p : L.Formula (n + 1)} {Γ : L.FormulaSet n} (h₁ : ∀ p ∈ Γ, c ∉ p.consts) (h₂ : c ∉ p.consts) :

Γ ⊢ p[↦ₛ (c ⬝ᶠ []ᵥ)]ₚ → Γ ⊢ ∀' p

source

inductive FirstOrder.Language.henkinStep.Func (L : Language) (n : ℕ) :

ℕ → Type u

inj {L : Language} {n m : ℕ} : L.Func m → Func L n m
wit {L : Language} {n : ℕ} : L.Formula (n + 1) → Func L n 0

Instances For

source

def FirstOrder.Language.henkinStep (L : Language) (n : ℕ) :

Language

Equations

L.henkinStep n = { Func := FirstOrder.Language.henkinStep.Func L n, Rel := L.Rel }

Instances For

source

def FirstOrder.Language.henkinStep.wit {L : Language} {n : ℕ} (p : L.Formula (n + 1)) :

(L.henkinStep n).Const

Equations

FirstOrder.Language.henkinStep.wit p = FirstOrder.Language.henkinStep.Func.wit p

Instances For

source

def FirstOrder.Language.henkinStep.hom {L : Language} {n : ℕ} :

L →ᴸ L.henkinStep n

Equations

FirstOrder.Language.henkinStep.hom = { onFunc := fun {n_1 : ℕ} (f : L.Func n_1) => FirstOrder.Language.henkinStep.Func.inj f, onRel := fun {n : ℕ} (r : L.Rel n) => r }

Instances For

source

@[simp]

theorem FirstOrder.Language.henkinStep.hom_onFunc {L : Language} {n n✝ : ℕ} (f : L.Func n✝) :

hom.onFunc f = Func.inj f

source

@[simp]

theorem FirstOrder.Language.henkinStep.hom_onRel {L : Language} {n n✝ : ℕ} (r : L.Rel n✝) :

hom.onRel r = r

source

theorem FirstOrder.Language.henkinStep.wit_not_in_homTerm {L✝ : Language} {n✝ : ℕ} {t : L✝.Term n✝} {a✝ : ℕ} {p : L✝.Formula (a✝ + 1)} :

wit p ∉ (hom.onTerm t).consts

source

theorem FirstOrder.Language.henkinStep.wit_not_in_homFormula {L✝ : Language} {a✝ : ℕ} {q : L✝.Formula a✝} {a✝¹ : ℕ} {p : L✝.Formula (a✝¹ + 1)} :

wit p ∉ (hom.onFormula q).consts

source

@[irreducible]

def FirstOrder.Language.henkinStep.invTerm {L : Language} {n m : ℕ} (k : ℕ) :

(L.henkinStep n).Term (m + k) → L.Term (m + k + 1)

Equations

FirstOrder.Language.henkinStep.invTerm x✝ #x_2 = #(Fin.insertAt x✝ x_2)
FirstOrder.Language.henkinStep.invTerm x✝ (FirstOrder.Language.henkinStep.Func.inj f ⬝ᶠ v) = f ⬝ᶠ fun (i : Fin m_1) => FirstOrder.Language.henkinStep.invTerm x✝ (v i)
FirstOrder.Language.henkinStep.invTerm x✝ (FirstOrder.Language.henkinStep.Func.wit a ⬝ᶠ a_1) = #(Fin.embedAt x✝)

Instances For

source

theorem FirstOrder.Language.henkinStep.invTerm_homTerm {L : Language} {k n a✝ : ℕ} {t : L.Term (a✝ + k)} :

invTerm k (hom.onTerm t) = t[Subst.shiftAt k]ₜ

source

theorem FirstOrder.Language.henkinStep.invTerm_subst {L : Language} {n m k m' k' : ℕ} {t : (L.henkinStep n).Term (m + k)} {σ : (L.henkinStep n).Subst (m + k) (m' + k')} :

invTerm k' t[σ]ₜ = (invTerm k t)[Subst.insertAt k ((fun (x : (L.henkinStep n).Term (m' + k')) => invTerm k' x) ∘ σ) #(Fin.embedAt k')]ₜ

source

theorem FirstOrder.Language.henkinStep.invTerm_shift {k : ℕ} {L✝ : Language} {n✝ a✝ : ℕ} {t : (L✝.henkinStep n✝).Term (a✝.add k)} :

invTerm (k + 1) ↑ₜt = ↑ₜ(invTerm k t)

source

@[irreducible]

def FirstOrder.Language.henkinStep.invFormula {L : Language} {n m : ℕ} (k : ℕ) :

(L.henkinStep n).Formula (m + k) → L.Formula (m + k + 1)

Equations

FirstOrder.Language.henkinStep.invFormula x✝ (r ⬝ʳ v) = r ⬝ʳ fun (i : Fin m_1) => FirstOrder.Language.henkinStep.invTerm x✝ (v i)
FirstOrder.Language.henkinStep.invFormula x✝ (t₁ ≐ t₂) = FirstOrder.Language.henkinStep.invTerm x✝ t₁ ≐ FirstOrder.Language.henkinStep.invTerm x✝ t₂
FirstOrder.Language.henkinStep.invFormula x✝ FirstOrder.Language.Formula.false = ⊥
FirstOrder.Language.henkinStep.invFormula x✝ (p.imp q) = FirstOrder.Language.henkinStep.invFormula x✝ p ⇒ FirstOrder.Language.henkinStep.invFormula x✝ q
FirstOrder.Language.henkinStep.invFormula x✝ (∀' p) = ∀' FirstOrder.Language.henkinStep.invFormula (x✝ + 1) p

Instances For

source

@[simp]

theorem FirstOrder.Language.henkinStep.invFormula_false {L : Language} {k n m : ℕ} :

invFormula k ⊥ = ⊥

source

@[simp]

theorem FirstOrder.Language.henkinStep.invFormula_imp {L : Language} {n m k : ℕ} {p q : (L.henkinStep n).Formula (m + k)} :

invFormula k (p ⇒ q) = invFormula k p ⇒ invFormula k q

source

@[simp]

theorem FirstOrder.Language.henkinStep.invFormula_neg {k : ℕ} {L✝ : Language} {n✝ a✝ : ℕ} {p : (L✝.henkinStep n✝).Formula (a✝ + k)} :

invFormula k (~ p) = ~ invFormula k p

source

theorem FirstOrder.Language.henkinStep.invFormula_andN {L : Language} {n m k l : ℕ} {v : Vec ((L.henkinStep n).Formula (m + k)) l} :

invFormula k (⋀ (i : Fin l), v i) = ⋀ (i : Fin l), invFormula k (v i)

source

@[irreducible]

theorem FirstOrder.Language.henkinStep.invFormula_homFormula {L : Language} {k n a✝ : ℕ} {p : L.Formula (a✝ + k)} :

invFormula k (hom.onFormula p) = p[Subst.shiftAt k]ₚ

source

@[irreducible]

theorem FirstOrder.Language.henkinStep.invFormula_subst {L : Language} {n m k m' k' : ℕ} {p : (L.henkinStep n).Formula (m + k)} {σ : (L.henkinStep n).Subst (m + k) (m' + k')} :

invFormula k' p[σ]ₚ = (invFormula k p)[Subst.insertAt k ((fun (x : (L.henkinStep n).Term (m' + k')) => invTerm k' x) ∘ σ) #(Fin.embedAt k')]ₚ

source

theorem FirstOrder.Language.henkinStep.invFormula_shift {k : ℕ} {L✝ : Language} {n✝ a✝ : ℕ} {p : (L✝.henkinStep n✝).Formula (a✝.add k)} :

invFormula (k + 1) ↑ₚp = ↑ₚ(invFormula k p)

source

theorem FirstOrder.Language.henkinStep.invFormula_subst_single {k : ℕ} {L✝ : Language} {n✝ a✝ : ℕ} {p : (L✝.henkinStep n✝).Formula (a✝ + k + 1)} {t : (L✝.henkinStep n✝).Term (a✝ + k)} :

invFormula k p[↦ₛ t]ₚ = (invFormula (k + 1) p)[↦ₛ invTerm k t]ₚ

source

@[irreducible]

theorem FirstOrder.Language.henkinStep.inv_axiom {L : Language} {n m k : ℕ} {Γ : L.FormulaSet (m + k + 1)} {p : (L.henkinStep n).Formula (m + k)} :

p ∈ (L.henkinStep n).Axiom → Γ ⊢ invFormula k p

source

theorem FirstOrder.Language.henkinStep.inv_proof {L✝ : Language} {a✝ : ℕ} {Δ : Set (L✝.Formula a✝)} {n✝ : ℕ} {p : (L✝.henkinStep n✝).Formula a✝} :

hom.onFormula '' Δ ⊢ p → Δ ⊢ ∀' invFormula 0 p

source

theorem FirstOrder.Language.henkinStep.hom_consistent {L : Language} {m n : ℕ} {Γ : L.FormulaSet m} (h : Γ ⊢ ∃' ⊤) :

Consistent Γ → Consistent (hom.onFormula '' Γ)

source

inductive FirstOrder.Language.henkinStep.axioms {L : Language} {n : ℕ} :

(L.henkinStep n).FormulaSet n

henkin {L : Language} {n : ℕ} (p : L.Formula (n + 1)) : axioms (∃' hom.onFormula p ⇒ (hom.onFormula p)[↦ₛ (wit p ⬝ᶠ []ᵥ)]ₚ)

Instances For

source

def FirstOrder.Language.FormulaSet.henkinStep {L : Language} {n : ℕ} (Γ : L.FormulaSet n) :

(L.henkinStep n).FormulaSet n

Equations

Γ.henkinStep = FirstOrder.Language.henkinStep.hom.onFormula '' Γ ∪ FirstOrder.Language.henkinStep.axioms

Instances For

source

theorem FirstOrder.Language.FormulaSet.henkinStep.consistent {L✝ : Language} {n✝ : ℕ} {Γ : L✝.FormulaSet n✝} (h : Γ ⊢ ∃' ⊤) :

Consistent Γ → Consistent Γ.henkinStep

source

def FirstOrder.Language.henkinChain (L : Language) (n : ℕ) :

ℕ → Language

Equations

L.henkinChain n 0 = L
L.henkinChain n k.succ = (L.henkinChain n k).henkinStep n

Instances For

source

def FirstOrder.Language.henkinize (L : Language) (n : ℕ) :

Language

Equations

L.henkinize n = (FirstOrder.Language.DirectedSystem.ofChain (L.henkinChain n) fun (x : ℕ) => FirstOrder.Language.henkinStep.hom).directLimit

Instances For

source

def FirstOrder.Language.FormulaSet.henkinChain {L : Language} {n : ℕ} (Γ : L.FormulaSet n) (i : ℕ) :

(L.henkinChain n i).FormulaSet n

Equations

Γ.henkinChain 0 = Γ
Γ.henkinChain k.succ = (Γ.henkinChain k).henkinStep

Instances For

source

def FirstOrder.Language.FormulaSet.henkinize {L : Language} {n : ℕ} (Γ : L.FormulaSet n) :

(L.henkinize n).FormulaSet n

Equations

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

Instances For

source

theorem FirstOrder.Language.FormulaSet.henkinize.supset_henkin {n : ℕ} {L : Language} {Γ : L.FormulaSet n} {Δ : (L.henkinize n).FormulaSet n} :

Γ.henkinize ⊆ Δ → Henkin Δ

source

theorem FirstOrder.Language.FormulaSet.henkinChain.nontrivial {n : ℕ} {L : Language} {Γ : L.FormulaSet n} (h₁ : Γ ⊢ ∃' ⊤) {i : ℕ} :

Γ.henkinChain i ⊢ ∃' ⊤

source

theorem FirstOrder.Language.FormulaSet.henkinChain.consistent {n : ℕ} {L : Language} {Γ : L.FormulaSet n} (h₁ : Γ ⊢ ∃' ⊤) (h₂ : Consistent Γ) {i : ℕ} :

Consistent (Γ.henkinChain i)

source

theorem FirstOrder.Language.FormulaSet.henkinize.consistent {n : ℕ} {L : Language} {Γ : L.FormulaSet n} (h₁ : Γ ⊢ ∃' ⊤) (h₂ : Consistent Γ) :

Consistent Γ.henkinize