Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.realize_mapTermRel_id

∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'}
  [inst_1 : L'.Structure M] {ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)}
  {fr : (n : ℕ) → L.Relations n → L'.Relations n} {n : ℕ} {φ : L.BoundedFormula α n} {v : α → M} {v' : β → M}
  {xs : Fin n → M},
  (∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M),
      FirstOrder.Language.Term.realize (Sum.elim v' xs) (ft n t) = FirstOrder.Language.Term.realize (Sum.elim v xs) t) →
    (∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap (fr n R) x = FirstOrder.Language.Structure.RelMap R x) →
      ((FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun x => id) φ).Realize v' xs ↔ φ.Realize v xs)

Defined in

Mathlib.ModelTheory.Semantics

Cited by

4 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Structure