English
φ Realizes in T under a theory extension iff the encodings via an expanded language realize equivalently.
Русский
Реализация ограниченной формулы через расширение языка эквивалентна реализации через эквивалентные кодировки.
LaTeX
$$$T \\models^b φ \\iff (L_{\\text{with constants}}^\\alpha \\text{ on } T) \\models^b \\mathrm{FormulaEquiv}(φ)$$$
Lean4
theorem models_formula_iff_onTheory_models_equivSentence {φ : L.Formula α} :
T ⊨ᵇ φ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ :=
by
refine ⟨fun h => models_sentence_iff.2 (fun M => ?_), fun h => models_formula_iff.2 (fun M v => ?_)⟩
· letI := (L.lhomWithConstants α).reduct M
have : (L.lhomWithConstants α).IsExpansionOn M :=
LHom.isExpansionOn_reduct _
_
-- why doesn't that instance just work?
rw [Formula.realize_equivSentence]
have : M ⊨ T := (LHom.onTheory_model _ _).1 M.is_model
let M' := Theory.ModelType.of T M
exact h M' (fun a => (L.con a : M)) _
· letI : (constantsOn α).Structure M := constantsOn.structure v
have : M ⊨ (L.lhomWithConstants α).onTheory T := (LHom.onTheory_model _ _).2 inferInstance
exact (Formula.realize_equivSentence _ _).1 (h.realize_sentence M)
