Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 16:35 715f984a

View on Github →

feat(model_theory/terms_and_formulas): Prenex Normal Form (#12558) Defines first_order.language.bounded_formula.to_prenex, a function which takes a formula and outputs an equivalent formula in prenex normal form. Proves inductive principles based on the fact that every formula is equivalent to one in prenex normal form.

Estimated changes

Modified src/data/fin/tuple/basic.lean

added theorem fin.snoc_comp_cast_succ

Modified src/model_theory/terms_and_formulas.lean

added theorem first_order.language.Theory.semantically_equivalent.refl

added theorem first_order.language.Theory.semantically_equivalent.symm

added theorem first_order.language.Theory.semantically_equivalent.trans

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_to_prenex_imp

added theorem first_order.language.bounded_formula.imp_semantically_equivalent_to_prenex_imp_right

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.is_atomic.cast_le

added theorem first_order.language.bounded_formula.is_atomic.lift_at

added theorem first_order.language.bounded_formula.is_prenex.cast_le

added theorem first_order.language.bounded_formula.is_prenex.lift_at

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.lift_at

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 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 theorem first_order.language.bounded_formula.semantically_equivalent_to_prenex

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 theorem first_order.language.formula.is_atomic_graph