Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-27 04:09 2c6df07f

View on Github →

chore(model_theory/*): Split up big model theory files (#12918) Splits up model_theory/basic into model_theory/basic, model_theory/language_maps, and model_theory/bundled. Splits up model_theory/terms_and_formulas into model_theory/syntax, model_theory/semantics, and model_theory/satisfiability. Adds to the module docs of these files.

Estimated changes

Modified src/model_theory/basic.lean

deleted def first_order.language.Lequiv.add_empty_constants

deleted structure first_order.language.Lequiv

deleted def first_order.language.Lhom.add_constants

deleted def first_order.language.Lhom.comp

deleted theorem first_order.language.Lhom.comp_assoc

deleted theorem first_order.language.Lhom.comp_id

deleted theorem first_order.language.Lhom.comp_sum_elim

deleted def first_order.language.Lhom.constants_on_map

deleted theorem first_order.language.Lhom.id_comp

deleted theorem first_order.language.Lhom.map_constants_comp_sum_inl

deleted theorem first_order.language.Lhom.sum_elim_comp_inl

deleted theorem first_order.language.Lhom.sum_elim_comp_inr

deleted theorem first_order.language.Lhom.sum_elim_inl_inr

deleted def first_order.language.Lhom.sum_map

deleted theorem first_order.language.Lhom.sum_map_comp_inl

deleted theorem first_order.language.Lhom.sum_map_comp_inr

deleted structure first_order.language.Lhom

deleted def first_order.language.Lhom_with_constants

deleted def first_order.language.Lhom_with_constants_map

deleted theorem first_order.language.coe_con

deleted def first_order.language.constants_on.Structure

deleted def first_order.language.constants_on

deleted theorem first_order.language.constants_on_constants

deleted def first_order.language.constants_on_functions

deleted theorem first_order.language.constants_on_map_is_expansion_on

deleted def first_order.language.with_constants

Created src/model_theory/bundled.lean

Modified src/model_theory/definability.lean

Modified src/model_theory/elementary_maps.lean

Modified src/model_theory/fraisse.lean

Created src/model_theory/language_map.lean

added def first_order.language.Lequiv.add_empty_constants

added structure first_order.language.Lequiv

added def first_order.language.Lhom.add_constants

added def first_order.language.Lhom.comp

added theorem first_order.language.Lhom.comp_assoc

added theorem first_order.language.Lhom.comp_id

added theorem first_order.language.Lhom.comp_sum_elim

added def first_order.language.Lhom.constants_on_map

added theorem first_order.language.Lhom.id_comp

added theorem first_order.language.Lhom.map_constants_comp_sum_inl

added theorem first_order.language.Lhom.sum_elim_comp_inl

added theorem first_order.language.Lhom.sum_elim_comp_inr

added theorem first_order.language.Lhom.sum_elim_inl_inr

added def first_order.language.Lhom.sum_map

added theorem first_order.language.Lhom.sum_map_comp_inl

added theorem first_order.language.Lhom.sum_map_comp_inr

added structure first_order.language.Lhom

added def first_order.language.Lhom_with_constants

added def first_order.language.Lhom_with_constants_map

added theorem first_order.language.coe_con

added def first_order.language.constants_on.Structure

added def first_order.language.constants_on

added theorem first_order.language.constants_on_constants

added def first_order.language.constants_on_functions

added theorem first_order.language.constants_on_map_is_expansion_on

added def first_order.language.with_constants

Modified src/model_theory/quotients.lean

Created src/model_theory/satisfiability.lean

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 def first_order.language.Theory.is_satisfiable

added theorem first_order.language.Theory.is_satisfiable_iff_is_finitely_satisfiable

added theorem first_order.language.Theory.model.is_satisfiable

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_bd_iff

added theorem first_order.language.Theory.semantically_equivalent.realize_iff

added theorem first_order.language.Theory.semantically_equivalent.refl

added theorem first_order.language.Theory.semantically_equivalent.some_model_realize_bd_iff

added theorem first_order.language.Theory.semantically_equivalent.some_model_realize_iff

added theorem first_order.language.Theory.semantically_equivalent.symm

added theorem first_order.language.Theory.semantically_equivalent.trans

added def first_order.language.Theory.semantically_equivalent

added def first_order.language.Theory.semantically_equivalent_setoid

added theorem first_order.language.bounded_formula.all_semantically_equivalent_not_ex_not

added theorem first_order.language.bounded_formula.ex_semantically_equivalent_not_all_not

added theorem first_order.language.bounded_formula.imp_semantically_equivalent_not_sup

added theorem first_order.language.bounded_formula.induction_on_all_ex

added theorem first_order.language.bounded_formula.induction_on_exists_not

added theorem first_order.language.bounded_formula.inf_semantically_equivalent_not_sup_not

added theorem first_order.language.bounded_formula.is_qf.induction_on_inf_not

added theorem first_order.language.bounded_formula.is_qf.induction_on_sup_not

added theorem first_order.language.bounded_formula.semantically_equivalent_all_lift_at

added theorem first_order.language.bounded_formula.semantically_equivalent_not_not

added theorem first_order.language.bounded_formula.semantically_equivalent_to_prenex

added theorem first_order.language.bounded_formula.sup_semantically_equivalent_not_inf_not

added theorem first_order.language.formula.imp_semantically_equivalent_not_sup

added theorem first_order.language.formula.inf_semantically_equivalent_not_sup_not

added theorem first_order.language.formula.semantically_equivalent_not_not

added theorem first_order.language.formula.sup_semantically_equivalent_not_inf_not

Created src/model_theory/semantics.lean

added theorem first_order.language.Lhom.on_Theory_model

added theorem first_order.language.Lhom.realize_on_bounded_formula

added theorem first_order.language.Lhom.realize_on_formula

added theorem first_order.language.Lhom.realize_on_sentence

added theorem first_order.language.Lhom.realize_on_term

added theorem first_order.language.Lhom.set_of_realize_on_formula

added theorem first_order.language.Theory.model.mono

added theorem first_order.language.Theory.realize_sentence_of_mem

added def first_order.language.bounded_formula.realize

added theorem first_order.language.bounded_formula.realize_all

added theorem first_order.language.bounded_formula.realize_all_lift_at_one_self

added theorem first_order.language.bounded_formula.realize_alls

added theorem first_order.language.bounded_formula.realize_bd_equal

added theorem first_order.language.bounded_formula.realize_bot

added theorem first_order.language.bounded_formula.realize_cast_le_of_eq

added theorem first_order.language.bounded_formula.realize_ex

added theorem first_order.language.bounded_formula.realize_exs

added theorem first_order.language.bounded_formula.realize_iff

added theorem first_order.language.bounded_formula.realize_imp

added theorem first_order.language.bounded_formula.realize_inf

added theorem first_order.language.bounded_formula.realize_lift_at

added theorem first_order.language.bounded_formula.realize_lift_at_one

added theorem first_order.language.bounded_formula.realize_lift_at_one_self

added theorem first_order.language.bounded_formula.realize_not

added theorem first_order.language.bounded_formula.realize_rel

added theorem first_order.language.bounded_formula.realize_relabel

added theorem first_order.language.bounded_formula.realize_sup

added theorem first_order.language.bounded_formula.realize_to_prenex

added theorem first_order.language.bounded_formula.realize_to_prenex_imp

added theorem first_order.language.bounded_formula.realize_to_prenex_imp_right

added theorem first_order.language.bounded_formula.realize_top

added theorem first_order.language.embedding.realize_term

added theorem first_order.language.equiv.realize_bounded_formula

added theorem first_order.language.equiv.realize_formula

added theorem first_order.language.equiv.realize_term

added def first_order.language.formula.realize

added theorem first_order.language.formula.realize_bot

added theorem first_order.language.formula.realize_equal

added theorem first_order.language.formula.realize_graph

added theorem first_order.language.formula.realize_iff

added theorem first_order.language.formula.realize_imp

added theorem first_order.language.formula.realize_inf

added theorem first_order.language.formula.realize_not

added theorem first_order.language.formula.realize_rel

added theorem first_order.language.formula.realize_relabel

added theorem first_order.language.formula.realize_sup

added theorem first_order.language.formula.realize_top

added theorem first_order.language.hom.realize_term

added def first_order.language.sentence.realize

added def first_order.language.term.realize

added theorem first_order.language.term.realize_con

added theorem first_order.language.term.realize_constants

added theorem first_order.language.term.realize_lift_at

added theorem first_order.language.term.realize_relabel

Modified src/model_theory/substructures.lean

Created src/model_theory/syntax.lean

added def first_order.language.Lequiv.on_bounded_formula

added theorem first_order.language.Lequiv.on_bounded_formula_symm

added def first_order.language.Lequiv.on_formula

added theorem first_order.language.Lequiv.on_formula_apply

added theorem first_order.language.Lequiv.on_formula_symm

added def first_order.language.Lequiv.on_sentence

added def first_order.language.Lequiv.on_term

added theorem first_order.language.Lhom.comp_on_bounded_formula

added theorem first_order.language.Lhom.comp_on_term

added theorem first_order.language.Lhom.id_on_bounded_formula

added theorem first_order.language.Lhom.id_on_term

added theorem first_order.language.Lhom.mem_on_Theory

added def first_order.language.Lhom.on_Theory

added def first_order.language.Lhom.on_bounded_formula

added def first_order.language.Lhom.on_formula

added def first_order.language.Lhom.on_sentence

added def first_order.language.Lhom.on_term

added def first_order.language.Theory

added def first_order.language.bounded_formula.alls

added def first_order.language.bounded_formula.cast_le

added def first_order.language.bounded_formula.exs

added theorem first_order.language.bounded_formula.is_atomic.cast_le

added theorem first_order.language.bounded_formula.is_atomic.is_prenex

added theorem first_order.language.bounded_formula.is_atomic.is_qf

added theorem first_order.language.bounded_formula.is_atomic.lift_at

added theorem first_order.language.bounded_formula.is_atomic.relabel

added inductive first_order.language.bounded_formula.is_atomic

added theorem first_order.language.bounded_formula.is_prenex.cast_le

added theorem first_order.language.bounded_formula.is_prenex.induction_on_all_not

added theorem first_order.language.bounded_formula.is_prenex.lift_at

added theorem first_order.language.bounded_formula.is_prenex.relabel

added inductive first_order.language.bounded_formula.is_prenex

added theorem first_order.language.bounded_formula.is_prenex_to_prenex_imp

added theorem first_order.language.bounded_formula.is_prenex_to_prenex_imp_right

added theorem first_order.language.bounded_formula.is_qf.cast_le

added theorem first_order.language.bounded_formula.is_qf.is_prenex

added theorem first_order.language.bounded_formula.is_qf.lift_at

added theorem first_order.language.bounded_formula.is_qf.not

added theorem first_order.language.bounded_formula.is_qf.relabel

added theorem first_order.language.bounded_formula.is_qf.to_prenex_imp

added theorem first_order.language.bounded_formula.is_qf.to_prenex_imp_right

added inductive first_order.language.bounded_formula.is_qf

added theorem first_order.language.bounded_formula.is_qf_bot

added def first_order.language.bounded_formula.lift_at

added theorem first_order.language.bounded_formula.not_all_is_atomic

added theorem first_order.language.bounded_formula.not_all_is_qf

added theorem first_order.language.bounded_formula.not_ex_is_atomic

added theorem first_order.language.bounded_formula.not_ex_is_qf

added def first_order.language.bounded_formula.relabel

added def first_order.language.bounded_formula.relabel_aux

added theorem first_order.language.bounded_formula.sum_elim_comp_relabel_aux

added def first_order.language.bounded_formula.to_prenex

added def first_order.language.bounded_formula.to_prenex_imp

added def first_order.language.bounded_formula.to_prenex_imp_right

added theorem first_order.language.bounded_formula.to_prenex_is_prenex

added inductive first_order.language.bounded_formula

added def first_order.language.constants.term

added def first_order.language.formula.graph

added theorem first_order.language.formula.is_atomic_graph

added def first_order.language.formula.relabel

added def first_order.language.formula

added def first_order.language.relations.bounded_formula

added def first_order.language.relations.formula

added def first_order.language.sentence

added def first_order.language.term.bd_equal

added theorem first_order.language.term.card_le

added theorem first_order.language.term.card_le_omega

added def first_order.language.term.equal

added def first_order.language.term.lift_at

added def first_order.language.term.list_decode

added theorem first_order.language.term.list_decode_encode_list

added def first_order.language.term.list_encode

added theorem first_order.language.term.list_encode_injective

added def first_order.language.term.relabel

added inductive first_order.language.term

Deleted src/model_theory/terms_and_formulas.lean

deleted def first_order.language.Lequiv.on_bounded_formula

deleted theorem first_order.language.Lequiv.on_bounded_formula_symm

deleted def first_order.language.Lequiv.on_formula

deleted theorem first_order.language.Lequiv.on_formula_apply

deleted theorem first_order.language.Lequiv.on_formula_symm

deleted def first_order.language.Lequiv.on_sentence

deleted def first_order.language.Lequiv.on_term

deleted theorem first_order.language.Lhom.comp_on_bounded_formula

deleted theorem first_order.language.Lhom.comp_on_term

deleted theorem first_order.language.Lhom.id_on_bounded_formula

deleted theorem first_order.language.Lhom.id_on_term

deleted theorem first_order.language.Lhom.mem_on_Theory

deleted def first_order.language.Lhom.on_Theory

deleted theorem first_order.language.Lhom.on_Theory_model

deleted def first_order.language.Lhom.on_bounded_formula

deleted def first_order.language.Lhom.on_formula

deleted def first_order.language.Lhom.on_sentence

deleted def first_order.language.Lhom.on_term

deleted theorem first_order.language.Lhom.realize_on_bounded_formula

deleted theorem first_order.language.Lhom.realize_on_formula

deleted theorem first_order.language.Lhom.realize_on_sentence

deleted theorem first_order.language.Lhom.realize_on_term

deleted theorem first_order.language.Lhom.set_of_realize_on_formula

deleted def first_order.language.Theory.is_finitely_satisfiable

deleted theorem first_order.language.Theory.is_satisfiable.is_finitely_satisfiable

deleted theorem first_order.language.Theory.is_satisfiable.mono

deleted def first_order.language.Theory.is_satisfiable.some_model

deleted def first_order.language.Theory.is_satisfiable

deleted theorem first_order.language.Theory.model.is_satisfiable

deleted theorem first_order.language.Theory.model.mono

deleted def first_order.language.Theory.models_bounded_formula

deleted theorem first_order.language.Theory.models_formula_iff

deleted theorem first_order.language.Theory.models_sentence_iff

deleted theorem first_order.language.Theory.realize_sentence_of_mem

deleted theorem first_order.language.Theory.semantically_equivalent.realize_bd_iff

deleted theorem first_order.language.Theory.semantically_equivalent.realize_iff

deleted theorem first_order.language.Theory.semantically_equivalent.refl

deleted theorem first_order.language.Theory.semantically_equivalent.some_model_realize_bd_iff

deleted theorem first_order.language.Theory.semantically_equivalent.some_model_realize_iff

deleted theorem first_order.language.Theory.semantically_equivalent.symm

deleted theorem first_order.language.Theory.semantically_equivalent.trans

deleted def first_order.language.Theory.semantically_equivalent

deleted def first_order.language.Theory.semantically_equivalent_setoid

deleted def first_order.language.Theory

deleted theorem first_order.language.bounded_formula.all_semantically_equivalent_not_ex_not

deleted def first_order.language.bounded_formula.alls

deleted def first_order.language.bounded_formula.cast_le

deleted theorem first_order.language.bounded_formula.ex_semantically_equivalent_not_all_not

deleted def first_order.language.bounded_formula.exs

deleted theorem first_order.language.bounded_formula.imp_semantically_equivalent_not_sup

deleted theorem first_order.language.bounded_formula.induction_on_all_ex

deleted theorem first_order.language.bounded_formula.induction_on_exists_not

deleted theorem first_order.language.bounded_formula.inf_semantically_equivalent_not_sup_not

deleted theorem first_order.language.bounded_formula.is_atomic.cast_le

deleted theorem first_order.language.bounded_formula.is_atomic.is_prenex

deleted theorem first_order.language.bounded_formula.is_atomic.is_qf

deleted theorem first_order.language.bounded_formula.is_atomic.lift_at

deleted theorem first_order.language.bounded_formula.is_atomic.relabel

deleted inductive first_order.language.bounded_formula.is_atomic

deleted theorem first_order.language.bounded_formula.is_prenex.cast_le

deleted theorem first_order.language.bounded_formula.is_prenex.induction_on_all_not

deleted theorem first_order.language.bounded_formula.is_prenex.lift_at

deleted theorem first_order.language.bounded_formula.is_prenex.relabel

deleted inductive first_order.language.bounded_formula.is_prenex

deleted theorem first_order.language.bounded_formula.is_prenex_to_prenex_imp

deleted theorem first_order.language.bounded_formula.is_prenex_to_prenex_imp_right

deleted theorem first_order.language.bounded_formula.is_qf.cast_le

deleted theorem first_order.language.bounded_formula.is_qf.induction_on_inf_not

deleted theorem first_order.language.bounded_formula.is_qf.induction_on_sup_not

deleted theorem first_order.language.bounded_formula.is_qf.is_prenex

deleted theorem first_order.language.bounded_formula.is_qf.lift_at

deleted theorem first_order.language.bounded_formula.is_qf.not

deleted theorem first_order.language.bounded_formula.is_qf.relabel

deleted theorem first_order.language.bounded_formula.is_qf.to_prenex_imp

deleted theorem first_order.language.bounded_formula.is_qf.to_prenex_imp_right

deleted inductive first_order.language.bounded_formula.is_qf

deleted theorem first_order.language.bounded_formula.is_qf_bot

deleted def first_order.language.bounded_formula.lift_at

deleted theorem first_order.language.bounded_formula.not_all_is_atomic

deleted theorem first_order.language.bounded_formula.not_all_is_qf

deleted theorem first_order.language.bounded_formula.not_ex_is_atomic

deleted theorem first_order.language.bounded_formula.not_ex_is_qf

deleted def first_order.language.bounded_formula.realize

deleted theorem first_order.language.bounded_formula.realize_all

deleted theorem first_order.language.bounded_formula.realize_all_lift_at_one_self

deleted theorem first_order.language.bounded_formula.realize_alls

deleted theorem first_order.language.bounded_formula.realize_bd_equal

deleted theorem first_order.language.bounded_formula.realize_bot

deleted theorem first_order.language.bounded_formula.realize_cast_le_of_eq

deleted theorem first_order.language.bounded_formula.realize_ex

deleted theorem first_order.language.bounded_formula.realize_exs

deleted theorem first_order.language.bounded_formula.realize_iff

deleted theorem first_order.language.bounded_formula.realize_imp

deleted theorem first_order.language.bounded_formula.realize_inf

deleted theorem first_order.language.bounded_formula.realize_lift_at

deleted theorem first_order.language.bounded_formula.realize_lift_at_one

deleted theorem first_order.language.bounded_formula.realize_lift_at_one_self

deleted theorem first_order.language.bounded_formula.realize_not

deleted theorem first_order.language.bounded_formula.realize_rel

deleted theorem first_order.language.bounded_formula.realize_relabel

deleted theorem first_order.language.bounded_formula.realize_sup

deleted theorem first_order.language.bounded_formula.realize_to_prenex

deleted theorem first_order.language.bounded_formula.realize_to_prenex_imp

deleted theorem first_order.language.bounded_formula.realize_to_prenex_imp_right

deleted theorem first_order.language.bounded_formula.realize_top

deleted def first_order.language.bounded_formula.relabel

deleted def first_order.language.bounded_formula.relabel_aux

deleted theorem first_order.language.bounded_formula.semantically_equivalent_all_lift_at

deleted theorem first_order.language.bounded_formula.semantically_equivalent_not_not

deleted theorem first_order.language.bounded_formula.semantically_equivalent_to_prenex

deleted theorem first_order.language.bounded_formula.sum_elim_comp_relabel_aux

deleted theorem first_order.language.bounded_formula.sup_semantically_equivalent_not_inf_not

deleted def first_order.language.bounded_formula.to_prenex

deleted def first_order.language.bounded_formula.to_prenex_imp

deleted def first_order.language.bounded_formula.to_prenex_imp_right

deleted theorem first_order.language.bounded_formula.to_prenex_is_prenex

deleted inductive first_order.language.bounded_formula

deleted def first_order.language.constants.term

deleted theorem first_order.language.embedding.realize_term

deleted theorem first_order.language.equiv.realize_bounded_formula

deleted theorem first_order.language.equiv.realize_formula

deleted theorem first_order.language.equiv.realize_term

deleted def first_order.language.formula.graph

deleted theorem first_order.language.formula.imp_semantically_equivalent_not_sup

deleted theorem first_order.language.formula.inf_semantically_equivalent_not_sup_not

deleted theorem first_order.language.formula.is_atomic_graph

deleted def first_order.language.formula.realize

deleted theorem first_order.language.formula.realize_bot

deleted theorem first_order.language.formula.realize_equal

deleted theorem first_order.language.formula.realize_graph

deleted theorem first_order.language.formula.realize_iff

deleted theorem first_order.language.formula.realize_imp

deleted theorem first_order.language.formula.realize_inf

deleted theorem first_order.language.formula.realize_not

deleted theorem first_order.language.formula.realize_rel

deleted theorem first_order.language.formula.realize_relabel

deleted theorem first_order.language.formula.realize_sup

deleted theorem first_order.language.formula.realize_top

deleted def first_order.language.formula.relabel

deleted theorem first_order.language.formula.semantically_equivalent_not_not

deleted theorem first_order.language.formula.sup_semantically_equivalent_not_inf_not

deleted def first_order.language.formula

deleted theorem first_order.language.hom.realize_term

deleted def first_order.language.relations.bounded_formula

deleted def first_order.language.relations.formula

deleted def first_order.language.sentence.realize

deleted def first_order.language.sentence

deleted def first_order.language.term.bd_equal

deleted theorem first_order.language.term.card_le

deleted theorem first_order.language.term.card_le_omega

deleted def first_order.language.term.equal

deleted def first_order.language.term.lift_at

deleted def first_order.language.term.list_decode

deleted theorem first_order.language.term.list_decode_encode_list

deleted def first_order.language.term.list_encode

deleted theorem first_order.language.term.list_encode_injective

deleted def first_order.language.term.realize

deleted theorem first_order.language.term.realize_con

deleted theorem first_order.language.term.realize_constants

deleted theorem first_order.language.term.realize_lift_at

deleted theorem first_order.language.term.realize_relabel

deleted def first_order.language.term.relabel

deleted inductive first_order.language.term

Modified src/model_theory/ultraproducts.lean

deleted theorem first_order.language.Theory.is_satisfiable_iff_is_finitely_satisfiable