Theorems · Theorem · logic and foundations

FirstOrder.Language.BoundedFormula.realize_restrictFreeVar

∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : DecidableEq α]
  {n : ℕ} {φ : L.BoundedFormula α n} {f : ↥φ.freeVarFinset → β} {v : β → M} {xs : Fin n → M} (v' : α → M),
  (∀ (a : ↥φ.freeVarFinset), v (f a) = v' ↑a) → ((φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs)

Defined in

Mathlib.ModelTheory.Semantics

Cited by

4 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureDecidableEq