Commit 2023-05-12 15:18 017781e6

View on Github →

feat: port ModelTheory.Semantics (#3196)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Semantics.lean

added def FirstOrder.Language.BoundedFormula.Realize

added theorem FirstOrder.Language.BoundedFormula.realize_all

added theorem FirstOrder.Language.BoundedFormula.realize_all_liftAt_one_self

added theorem FirstOrder.Language.BoundedFormula.realize_alls

added theorem FirstOrder.Language.BoundedFormula.realize_bdEqual

added theorem FirstOrder.Language.BoundedFormula.realize_bot

added theorem FirstOrder.Language.BoundedFormula.realize_castLe_of_eq

added theorem FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv

added theorem FirstOrder.Language.BoundedFormula.realize_ex

added theorem FirstOrder.Language.BoundedFormula.realize_exs

added theorem FirstOrder.Language.BoundedFormula.realize_foldr_inf

added theorem FirstOrder.Language.BoundedFormula.realize_foldr_sup

added theorem FirstOrder.Language.BoundedFormula.realize_iff

added theorem FirstOrder.Language.BoundedFormula.realize_imp

added theorem FirstOrder.Language.BoundedFormula.realize_inf

added theorem FirstOrder.Language.BoundedFormula.realize_liftAt

added theorem FirstOrder.Language.BoundedFormula.realize_liftAt_one

added theorem FirstOrder.Language.BoundedFormula.realize_liftAt_one_self

added theorem FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe

added theorem FirstOrder.Language.BoundedFormula.realize_mapTermRel_id

added theorem FirstOrder.Language.BoundedFormula.realize_not

added theorem FirstOrder.Language.BoundedFormula.realize_rel

added theorem FirstOrder.Language.BoundedFormula.realize_relabel

added theorem FirstOrder.Language.BoundedFormula.realize_relabelEquiv

added theorem FirstOrder.Language.BoundedFormula.realize_rel₁

added theorem FirstOrder.Language.BoundedFormula.realize_rel₂

added theorem FirstOrder.Language.BoundedFormula.realize_restrictFreeVar

added theorem FirstOrder.Language.BoundedFormula.realize_subst

added theorem FirstOrder.Language.BoundedFormula.realize_sup

added theorem FirstOrder.Language.BoundedFormula.realize_toFormula

added theorem FirstOrder.Language.BoundedFormula.realize_toPrenex

added theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImp

added theorem FirstOrder.Language.BoundedFormula.realize_toPrenexImpRight

added theorem FirstOrder.Language.BoundedFormula.realize_top

added theorem FirstOrder.Language.ElementarilyEquivalent.completeTheory_eq

added theorem FirstOrder.Language.ElementarilyEquivalent.infinite

added theorem FirstOrder.Language.ElementarilyEquivalent.infinite_iff

added theorem FirstOrder.Language.ElementarilyEquivalent.nonempty

added theorem FirstOrder.Language.ElementarilyEquivalent.nonempty_iff

added theorem FirstOrder.Language.ElementarilyEquivalent.realize_sentence

added theorem FirstOrder.Language.ElementarilyEquivalent.theory_model

added theorem FirstOrder.Language.ElementarilyEquivalent.theory_model_iff

added def FirstOrder.Language.ElementarilyEquivalent

added theorem FirstOrder.Language.Embedding.realize_term

added theorem FirstOrder.Language.Equiv.elementarilyEquivalent

added theorem FirstOrder.Language.Equiv.realize_boundedFormula

added theorem FirstOrder.Language.Equiv.realize_formula

added theorem FirstOrder.Language.Equiv.realize_sentence

added theorem FirstOrder.Language.Equiv.realize_term

added theorem FirstOrder.Language.Equiv.theory_model

added theorem FirstOrder.Language.Formula.realize_bot

added theorem FirstOrder.Language.Formula.realize_equal

added theorem FirstOrder.Language.Formula.realize_equivSentence

added theorem FirstOrder.Language.Formula.realize_equivSentence_symm

added theorem FirstOrder.Language.Formula.realize_equivSentence_symm_con

added theorem FirstOrder.Language.Formula.realize_graph

added theorem FirstOrder.Language.Formula.realize_iff

added theorem FirstOrder.Language.Formula.realize_imp

added theorem FirstOrder.Language.Formula.realize_inf

added theorem FirstOrder.Language.Formula.realize_not

added theorem FirstOrder.Language.Formula.realize_rel

added theorem FirstOrder.Language.Formula.realize_relabel

added theorem FirstOrder.Language.Formula.realize_relabel_sum_inr

added theorem FirstOrder.Language.Formula.realize_rel₁

added theorem FirstOrder.Language.Formula.realize_rel₂

added theorem FirstOrder.Language.Formula.realize_sup

added theorem FirstOrder.Language.Formula.realize_top

added theorem FirstOrder.Language.Hom.realize_term

added theorem FirstOrder.Language.LHom.onTheory_model

added theorem FirstOrder.Language.LHom.realize_onBoundedFormula

added theorem FirstOrder.Language.LHom.realize_onFormula

added theorem FirstOrder.Language.LHom.realize_onSentence

added theorem FirstOrder.Language.LHom.realize_onTerm

added theorem FirstOrder.Language.LHom.setOf_realize_onFormula

added theorem FirstOrder.Language.Relations.realize_antisymmetric

added theorem FirstOrder.Language.Relations.realize_irreflexive

added theorem FirstOrder.Language.Relations.realize_reflexive

added theorem FirstOrder.Language.Relations.realize_symmetric

added theorem FirstOrder.Language.Relations.realize_total

added theorem FirstOrder.Language.Relations.realize_transitive

added theorem FirstOrder.Language.Sentence.realize_cardGe

added theorem FirstOrder.Language.Sentence.realize_not

added def FirstOrder.Language.Term.realize

added theorem FirstOrder.Language.Term.realize_con

added theorem FirstOrder.Language.Term.realize_constants

added theorem FirstOrder.Language.Term.realize_constantsToVars

added theorem FirstOrder.Language.Term.realize_constantsVarsEquivLeft

added theorem FirstOrder.Language.Term.realize_func

added theorem FirstOrder.Language.Term.realize_functions_apply₁

added theorem FirstOrder.Language.Term.realize_functions_apply₂

added theorem FirstOrder.Language.Term.realize_liftAt

added theorem FirstOrder.Language.Term.realize_relabel

added theorem FirstOrder.Language.Term.realize_restrictVar

added theorem FirstOrder.Language.Term.realize_restrictVarLeft

added theorem FirstOrder.Language.Term.realize_subst

added theorem FirstOrder.Language.Term.realize_var

added theorem FirstOrder.Language.Term.realize_varsToConstants

added theorem FirstOrder.Language.Theory.CompleteTheory.subset

added theorem FirstOrder.Language.Theory.Model.mono

added theorem FirstOrder.Language.Theory.Model.union

added theorem FirstOrder.Language.Theory.model_iff

added theorem FirstOrder.Language.Theory.model_iff_subset_completeTheory

added theorem FirstOrder.Language.Theory.model_singleton_iff

added theorem FirstOrder.Language.Theory.model_union_iff

added theorem FirstOrder.Language.Theory.realize_sentence_of_mem

added theorem FirstOrder.Language.card_le_of_model_distinctConstantsTheory

added def FirstOrder.Language.completeTheory

added theorem FirstOrder.Language.elementarilyEquivalent_iff

added theorem FirstOrder.Language.mem_completeTheory

added theorem FirstOrder.Language.model_distinctConstantsTheory

added theorem FirstOrder.Language.model_infiniteTheory_iff

added theorem FirstOrder.Language.model_nonemptyTheory_iff

added theorem FirstOrder.Language.realize_iff_of_model_completeTheory