Definitions and theorems about replaceFV and liftAt.

Main Definitions

• FirstOrder.Language.Term.replaceFV defines the function to replace all free variables fv' k with tsN k in a term t.
• FirstOrder.Language.BoundedFormula.replaceFV the function to replace all free variables fv' k with tsN k in a bounded formula ϕ.
• FirstOrder.Language.BoundedFormula.makeTsN defines the function on ℕ whose value at k is ts k if k < m + 1 and fv' k otherwise.
• FirstOrder.Language.BoundedFormula.replaceInitialValues replace the initial part of s : ℕ → V by xs : Fin (n + 1) → V.
• FirstOrder.Language.BoundedFormula.liftAndReplaceFV applies liftAt n' m and replace (makeTsN ts) in one call.

Main Statements

• Various "realize" theorems are proved.
• realize_liftAt' is the version of realize_liftAt in which we assume m ≤ n instead of m + n' ≤ n + 1.

Notations

• The symbols for Or and And, ∨' and ∧', are defined.

@[match_pattern]

def FirstOrder.Language.BoundedFormula.or {L : Language} {α : Type v} {n : ℕ} (ϕ1 ϕ2 : L.BoundedFormula α n) : L.BoundedFormula α n

Or operator in the formula.

Equations

• ϕ1∨'ϕ2 = ϕ1.not.imp ϕ2

def FirstOrder.Language.BoundedFormula.«term_∨'_» : Lean.TrailingParserDescr

Or operator in the formula.

Equations

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

@[match_pattern]

def FirstOrder.Language.BoundedFormula.and {L : Language} {α : Type v} {n : ℕ} (ϕ1 ϕ2 : L.BoundedFormula α n) : L.BoundedFormula α n

And operator in the formula.

Equations

• ϕ1∧'ϕ2 = (ϕ1.imp ϕ2.not).not

def FirstOrder.Language.BoundedFormula.«term_∧'_» : Lean.TrailingParserDescr

And operator in the formula.

Equations

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

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_or {V : Type u} {L : Language} [L.Structure V] {n : ℕ} {ϕ ψ : L.BoundedFormula ℕ n} {s : ℕ → V} {xs : Fin n → V} : (ϕ∨'ψ).Realize s xs ↔ ϕ.Realize s xs ∨ ψ.Realize s xs

@[simp]

theorem FirstOrder.Language.BoundedFormula.realize_and {V : Type u} {L : Language} [L.Structure V] {n : ℕ} {ϕ ψ : L.BoundedFormula ℕ n} {s : ℕ → V} {xs : Fin n → V} : (ϕ∧'ψ).Realize s xs ↔ ϕ.Realize s xs ∧ ψ.Realize s xs

def FirstOrder.Language.Term.replaceFV {L : Language} {n : ℕ} (t : L.Term (ℕ ⊕ Fin n)) (tsN : ℕ → L.Term (ℕ ⊕ Fin n)) : L.Term (ℕ ⊕ Fin n)

Replace all free variables fv' k with tsN k in a term t.

Equations

• (FirstOrder.Language.var (Sum.inl k)).replaceFV tsN = tsN k
• (FirstOrder.Language.var (Sum.inr val)).replaceFV tsN = FirstOrder.Language.var (Sum.inr val)
• (FirstOrder.Language.func _f _ts).replaceFV tsN = FirstOrder.Language.func _f fun (i : Fin l) => (_ts i).replaceFV tsN

def FirstOrder.Language.BoundedFormula.replaceFV {L : Language} {n : ℕ} (ϕ : L.BoundedFormula ℕ n) (tsN : ℕ → L.Term (ℕ ⊕ Fin n)) : L.BoundedFormula ℕ n

Replace all free variables fvN n k with tsN k in a formula ϕ.

Equations

• FirstOrder.Language.BoundedFormula.falsum.replaceFV tsN = FirstOrder.Language.BoundedFormula.falsum
• (FirstOrder.Language.BoundedFormula.equal t₁ t₂).replaceFV tsN = FirstOrder.Language.BoundedFormula.equal (t₁.replaceFV tsN) (t₂.replaceFV tsN)
• (FirstOrder.Language.BoundedFormula.rel R _ts).replaceFV tsN = FirstOrder.Language.BoundedFormula.rel R fun (i : Fin l) => (_ts i).replaceFV tsN
• (f₁.imp f₂).replaceFV tsN = (f₁.replaceFV tsN).imp (f₂.replaceFV tsN)
• f.all.replaceFV tsN = (f.replaceFV fun (k : ℕ) => FirstOrder.Language.Term.liftAt 1 n (tsN k)).all

def FirstOrder.Language.BoundedFormula.makeTsN {L : Language} {n m : ℕ} (ts : Fin (m + 1) → L.Term (ℕ ⊕ Fin n)) (k : ℕ) : L.Term (ℕ ⊕ Fin n)

Make a function on ℕ whose value at k is ts k if k < m + 1 and fv' k otherwise.

Equations

• FirstOrder.Language.BoundedFormula.makeTsN ts k = if k < m + 1 then ts (Fin.ofNat (m + 1) k) else FirstOrder.Language.var (Sum.inl k)

def FirstOrder.Language.BoundedFormula.replaceInitialValues {V : Type u} {n : ℕ} (s : ℕ → V) (xs : Fin (n + 1) → V) (k : ℕ) : V

Replace the initial part of s : ℕ → V by xs : Fin (n + 1) → V.

Equations

• FirstOrder.Language.BoundedFormula.replaceInitialValues s xs k = if k < n + 1 then xs (Fin.ofNat (n + 1) k) else s k

def FirstOrder.Language.BoundedFormula.liftAndReplaceFV {L : Language} {n l : ℕ} (ϕ : L.BoundedFormula ℕ n) (n' m : ℕ) (ts : Fin (l + 1) → L.Term (ℕ ⊕ Fin (n + n'))) : L.BoundedFormula ℕ (n + n')

Apply liftAt n' m and replace (makeTsN ts) in one call.

Equations

• ϕ.liftAndReplaceFV n' m ts = (FirstOrder.Language.BoundedFormula.liftAt n' m ϕ).replaceFV (FirstOrder.Language.BoundedFormula.makeTsN ts)

@[simp]

theorem FirstOrder.Language.ReplaceFV.Term.realize_replaceFV {L : Language} {V : Type u} [L.Structure V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {t : L.Term (ℕ ⊕ Fin n)} {tsN : ℕ → L.Term (ℕ ⊕ Fin n)} : Term.realize (Sum.elim s xs) (t.replaceFV tsN) = Term.realize (Sum.elim (fun (k : ℕ) => Term.realize (Sum.elim s xs) (tsN k)) xs) t

theorem FirstOrder.Language.ReplaceFV.Term.realize_liftAt'_one {L : Language} {V : Type u} [L.Structure V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {t : L.Term (ℕ ⊕ Fin n)} {a : V} : Term.realize (Sum.elim s (Fin.snoc xs a)) (Term.liftAt 1 n t) = Term.realize (Sum.elim s xs) t

theorem FirstOrder.Language.ReplaceFV.Term.realize_liftAt' {L : Language} {V : Type u} [L.Structure V] {n n' : ℕ} {s : ℕ → V} {xs : Fin n → V} {xs1 : Fin (n + n') → V} {t : L.Term (ℕ ⊕ Fin n)} : (∀ (k : Fin n), xs1 (Fin.castAdd n' k) = xs k) → Term.realize (Sum.elim s xs1) (Term.liftAt n' n t) = Term.realize (Sum.elim s xs) t

Realization of liftAt n' n t agrees with realization of t when the extra context values xs1 extend xs along castAdd. Lifts the hypothesis n + n' ≤ n + 1 from realize_liftAt to m ≤ n.

@[simp]

theorem FirstOrder.Language.ReplaceFV.BoundedFormula.realize_replaceFV {L : Language} {V : Type u} [L.Structure V] {n : ℕ} {s : ℕ → V} {xs : Fin n → V} {ϕ : L.BoundedFormula ℕ n} {tsN : ℕ → L.Term (ℕ ⊕ Fin n)} : (ϕ.replaceFV tsN).Realize s xs ↔ ϕ.Realize (fun (k : ℕ) => Term.realize (Sum.elim s xs) (tsN k)) xs

theorem FirstOrder.Language.ReplaceFV.realize_liftAt' {L : Language} {V : Type u} [L.Structure V] {n' m : ℕ} {h_n_prime_nezero : n' > 0} {s : ℕ → V} {n : ℕ} {φ : L.BoundedFormula ℕ n} (xs : Fin (n + n') → V) : m ≤ n → ((BoundedFormula.liftAt n' m φ).Realize s xs ↔ φ.Realize s (xs ∘ fun (i : Fin n) => if ↑i < m then Fin.castAdd n' i else i.addNat n'))

Lifted realization invariant: a formula's realization at lifted context matches its realization at the original context, under the hypothesis m ≤ n.

@[simp]

theorem FirstOrder.Language.ReplaceFV.replaceInitialValues_1_0 {V : Type u} {s : ℕ → V} {a : V} : BoundedFormula.replaceInitialValues s ![a] 0 = a

replaceInitialValues s ![a] 0 = a.

@[simp]

theorem FirstOrder.Language.ReplaceFV.replaceInitialValues_2_0 {V : Type u} {s : ℕ → V} {a b : V} : BoundedFormula.replaceInitialValues s ![a, b] 0 = a

replaceInitialValues s ![a, b] 0 = a.

@[simp]

theorem FirstOrder.Language.ReplaceFV.replaceInitialValues_2_1 {V : Type u} {s : ℕ → V} {a b : V} : BoundedFormula.replaceInitialValues s ![a, b] 1 = b

replaceInitialValues s ![a, b] 1 = b.

@[simp]

theorem FirstOrder.Language.ReplaceFV.realize_makeTsN {L : Language} {n m k : ℕ} {ts : Fin (m + 1) → L.Term (ℕ ⊕ Fin n)} {h : k < m + 1} : BoundedFormula.makeTsN ts k = ts (Fin.ofNat (m + 1) k)

makeTsN ts k = ts (Fin.ofNat (m+1) k) when k < m + 1.