Commit 2022-02-16 11:53 d24792c6

View on Github →

feat(model_theory/terms_and_formulas): Define satisfiability and semantic equivalence of formulas (#11928) Defines satisfiability of theories Provides a default model of a satisfiable theory Defines semantic (logical) equivalence of formulas

Estimated changes

Modified src/model_theory/basic.lean

deleted def first_order.language.empty

added theorem first_order.language.nonempty_of_nonempty_constants

Modified src/model_theory/definability.lean

Modified src/model_theory/terms_and_formulas.lean

added theorem first_order.language.Theory.imp_semantically_equivalent_not_sup

added theorem first_order.language.Theory.inf_semantically_equivalent_not_sup_not

added def first_order.language.Theory.is_finitely_satisfiable

added theorem first_order.language.Theory.is_satisfiable.is_finitely_satisfiable

added theorem first_order.language.Theory.is_satisfiable.mono

added def first_order.language.Theory.is_satisfiable.some_model

added theorem first_order.language.Theory.is_satisfiable.some_model_models

added def first_order.language.Theory.is_satisfiable

added theorem first_order.language.Theory.model.is_satisfiable

added theorem first_order.language.Theory.model.mono

added def first_order.language.Theory.model

added def first_order.language.Theory.models_bounded_formula

added theorem first_order.language.Theory.models_formula_iff

added theorem first_order.language.Theory.models_sentence_iff

added theorem first_order.language.Theory.semantically_equivalent.realize_eq

added theorem first_order.language.Theory.semantically_equivalent.some_model_realize_eq

added def first_order.language.Theory.semantically_equivalent

added theorem first_order.language.Theory.semantically_equivalent_not_not

added def first_order.language.Theory.semantically_equivalent_setoid

added theorem first_order.language.Theory.sup_semantically_equivalent_not_inf_not

added def first_order.language.Theory

modified def first_order.language.bd_not

added theorem first_order.language.realize_imp

added theorem first_order.language.realize_inf

deleted def first_order.language.theory