# mathlib3documentation

model_theory.syntax

# Basics on First-Order Syntax #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines first-order terms, formulas, sentences, and theories in a style inspired by the Flypitch project.

## Main Definitions #

• A `first_order.language.term` is defined so that `L.term α` is the type of `L`-terms with free variables indexed by `α`.
• A `first_order.language.formula` is defined so that `L.formula α` is the type of `L`-formulas with free variables indexed by `α`.
• A `first_order.language.sentence` is a formula with no free variables.
• A `first_order.language.Theory` is a set of sentences.
• The variables of terms and formulas can be relabelled with `first_order.language.term.relabel`, `first_order.language.bounded_formula.relabel`, and `first_order.language.formula.relabel`.
• Given an operation on terms and an operation on relations, `first_order.language.bounded_formula.map_term_rel` gives an operation on formulas.
• `first_order.language.bounded_formula.cast_le` adds more `fin`-indexed variables.
• `first_order.language.bounded_formula.lift_at` raises the indexes of the `fin`-indexed variables above a particular index.
• `first_order.language.term.subst` and `first_order.language.bounded_formula.subst` substitute variables with given terms.
• Language maps can act on syntactic objects with functions such as `first_order.language.Lhom.on_formula`.
• `first_order.language.term.constants_vars_equiv` and `first_order.language.bounded_formula.constants_vars_equiv` switch terms and formulas between having constants in the language and having extra variables indexed by the same type.

## Implementation Notes #

• Formulas use a modified version of de Bruijn variables. Specifically, a `L.bounded_formula α n` is a formula with some variables indexed by a type `α`, which cannot be quantified over, and some indexed by `fin n`, which can. For any `φ : L.bounded_formula α (n + 1)`, we define the formula `∀' φ : L.bounded_formula α n` by universally quantifying over the variable indexed by `n : fin (n + 1)`.

## References #

For the Flypitch project:

inductive first_order.language.term (L : first_order.language) (α : Type u') :
Type (max u u')

A term on `α` is either a variable indexed by an element of `α` or a function symbol applied to simpler terms.

Instances for `first_order.language.term`
@[simp]

The `finset` of variables used in a given term.

Equations
@[simp]

The `finset` of variables from the left side of a sum used in a given term.

Equations
@[simp]
def first_order.language.term.relabel {L : first_order.language} {α : Type u'} {β : Type v'} (g : α β) :
L.term α L.term β

Relabels a term's variables along a particular function.

Equations
@[simp]
theorem first_order.language.term.relabel_relabel {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} (f : α β) (g : β γ) (t : L.term α) :
@[simp]
theorem first_order.language.term.relabel_comp_relabel {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} (f : α β) (g : β γ) :
@[simp]
theorem first_order.language.term.relabel_equiv_apply {L : first_order.language} {α : Type u'} {β : Type v'} (g : α β) (ᾰ : L.term α) :
def first_order.language.term.relabel_equiv {L : first_order.language} {α : Type u'} {β : Type v'} (g : α β) :
L.term α L.term β

Relabels a term's variables along a bijection.

Equations
@[simp]
theorem first_order.language.term.relabel_equiv_symm_apply {L : first_order.language} {α : Type u'} {β : Type v'} (g : α β) (ᾰ : L.term β) :
def first_order.language.term.restrict_var {L : first_order.language} {α : Type u'} {β : Type v'} [decidable_eq α] (t : L.term α) (f : (t.var_finset) β) :
L.term β

Restricts a term to use only a set of the given variables.

Equations
def first_order.language.term.restrict_var_left {L : first_order.language} {α : Type u'} {β : Type v'} [decidable_eq α] {γ : Type u_1} (t : L.term γ)) (f : (t.var_finset_left) β) :
L.term γ)

Restricts a term to use only a set of the given variables on the left side of a sum.

Equations

The representation of a constant symbol as a term.

Equations
def first_order.language.functions.apply₁ {L : first_order.language} {α : Type u'} (f : L.functions 1) (t : L.term α) :
L.term α

Applies a unary function to a term.

Equations
def first_order.language.functions.apply₂ {L : first_order.language} {α : Type u'} (f : L.functions 2) (t₁ t₂ : L.term α) :
L.term α

Applies a binary function to two terms.

Equations
@[simp]

Sends a term with constants to a term with extra variables.

Equations
@[simp]

Sends a term with extra variables to a term with constants.

Equations
@[simp]

A bijection between terms with constants and terms with extra variables.

Equations
@[simp]
theorem first_order.language.term.constants_vars_equiv_symm_apply {L : first_order.language} {α : Type u'} {γ : Type u_5} (ᾰ : L.term α)) :
def first_order.language.term.constants_vars_equiv_left {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} :
(L.with_constants γ).term β) L.term ((γ α) β)

A bijection between terms with constants and terms with extra variables.

Equations
@[simp]
theorem first_order.language.term.constants_vars_equiv_left_apply {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} (t : (L.with_constants γ).term β)) :
@[simp]
theorem first_order.language.term.constants_vars_equiv_left_symm_apply {L : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} (t : L.term ((γ α) β)) :
@[protected, instance]
Equations
@[protected, instance]
Equations
def first_order.language.term.lift_at {L : first_order.language} {α : Type u'} {n : } (n' m : ) :
L.term fin n) L.term fin (n + n'))

Raises all of the `fin`-indexed variables of a term greater than or equal to `m` by `n'`.

Equations
@[simp]
def first_order.language.term.subst {L : first_order.language} {α : Type u'} {β : Type v'} :
L.term α L.term β) L.term β

Substitutes the variables in a given term with terms.

Equations
• tf = (λ (i : fin a_24), (ts i).subst tf)
• = tf a
@[simp]

Maps a term's symbols along a language map.

Equations
@[simp]
theorem first_order.language.Lhom.comp_on_term {L : first_order.language} {L' : first_order.language} {α : Type u'} {L'' : first_order.language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :

Maps a term's symbols along a language equivalence.

Equations
@[simp]
theorem first_order.language.Lequiv.on_term_symm_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') (ᾰ : L'.term α) :
(φ.on_term.symm) ᾰ = φ.inv_Lhom.on_term
@[simp]
theorem first_order.language.Lequiv.on_term_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') (ᾰ : L.term α) :
(φ.on_term) ᾰ = φ.to_Lhom.on_term
inductive first_order.language.bounded_formula (L : first_order.language) (α : Type u') :
Type (max u v u')

`bounded_formula α n` is the type of formulas with free variables indexed by `α` and up to `n` additional free variables.

Instances for `first_order.language.bounded_formula`
@[reducible]
def first_order.language.formula (L : first_order.language) (α : Type u') :
Type (max u v u')

`formula α` is the type of formulas with all free variables indexed by `α`.

Equations
@[reducible]

A sentence is a formula with no free variables.

Equations
@[reducible]

A theory is a set of sentences.

Equations
def first_order.language.relations.bounded_formula {L : first_order.language} {α : Type u'} {n l : } (R : L.relations n) (ts : fin n L.term fin l)) :
l

Applies a relation to terms as a bounded formula.

Equations
def first_order.language.relations.bounded_formula₁ {L : first_order.language} {α : Type u'} {n : } (r : L.relations 1) (t : L.term fin n)) :
n

Applies a unary relation to a term as a bounded formula.

Equations
def first_order.language.relations.bounded_formula₂ {L : first_order.language} {α : Type u'} {n : } (r : L.relations 2) (t₁ t₂ : L.term fin n)) :
n

Applies a binary relation to two terms as a bounded formula.

Equations
def first_order.language.term.bd_equal {L : first_order.language} {α : Type u'} {n : } (t₁ t₂ : L.term fin n)) :
n

The equality of two terms as a bounded formula.

Equations
def first_order.language.relations.formula {L : first_order.language} {α : Type u'} {n : } (R : L.relations n) (ts : fin n L.term α) :
L.formula α

Applies a relation to terms as a bounded formula.

Equations

Applies a unary relation to a term as a formula.

Equations
def first_order.language.relations.formula₂ {L : first_order.language} {α : Type u'} (r : L.relations 2) (t₁ t₂ : L.term α) :
L.formula α

Applies a binary relation to two terms as a formula.

Equations
def first_order.language.term.equal {L : first_order.language} {α : Type u'} (t₁ t₂ : L.term α) :
L.formula α

The equality of two terms as a first-order formula.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
def first_order.language.bounded_formula.not {L : first_order.language} {α : Type u'} {n : } (φ : n) :
n

The negation of a bounded formula is also a bounded formula.

Equations
@[protected]
def first_order.language.bounded_formula.ex {L : first_order.language} {α : Type u'} {n : } (φ : (n + 1)) :
n

Puts an `∃` quantifier on a bounded formula.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
def first_order.language.bounded_formula.iff {L : first_order.language} {α : Type u'} {n : } (φ ψ : n) :
n

The biimplication between two bounded formulas.

Equations
@[simp]

The `finset` of variables used in a given formula.

Equations
@[simp]
def first_order.language.bounded_formula.cast_le {L : first_order.language} {α : Type u'} {m n : } (h : m n) :
m n

Casts `L.bounded_formula α m` as `L.bounded_formula α n`, where `m ≤ n`.

Equations
@[simp]
theorem first_order.language.bounded_formula.cast_le_rfl {L : first_order.language} {α : Type u'} {n : } (h : n n) (φ : n) :
@[simp]
theorem first_order.language.bounded_formula.cast_le_cast_le {L : first_order.language} {α : Type u'} {k m n : } (km : k m) (mn : m n) (φ : k) :
@[simp]
theorem first_order.language.bounded_formula.cast_le_comp_cast_le {L : first_order.language} {α : Type u'} {k m n : } (km : k m) (mn : m n) :

Restricts a bounded formula to only use a particular set of free variables.

Equations

Places universal quantifiers on all extra variables of a bounded formula.

Equations

Places existential quantifiers on all extra variables of a bounded formula.

Equations
def first_order.language.bounded_formula.map_term_rel {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} {g : } (ft : Π (n : ), L.term fin n) L'.term fin (g n))) (fr : Π (n : ), L.relations n L'.relations n) (h : Π (n : ), L'.bounded_formula β (g (n + 1)) L'.bounded_formula β (g n + 1)) {n : } :
n L'.bounded_formula β (g n)

Maps bounded formulas along a map of terms and a map of relations.

Equations
def first_order.language.bounded_formula.lift_at {L : first_order.language} {α : Type u'} {n : } (n' m : ) :
n (n + n')

Raises all of the `fin`-indexed variables of a formula greater than or equal to `m` by `n'`.

Equations
@[simp]
theorem first_order.language.bounded_formula.map_term_rel_map_term_rel {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} {γ : Type u_5} {L'' : first_order.language} (ft : Π (n : ), L.term fin n) L'.term fin n)) (fr : Π (n : ), L.relations n L'.relations n) (ft' : Π (n : ), L'.term fin n) L''.term fin n)) (fr' : Π (n : ), L'.relations n L''.relations n) {n : } (φ : n) :
(λ (_x : ), id) (λ (_x : ), id) φ) = first_order.language.bounded_formula.map_term_rel (λ (_x : ), ft' _x ft _x) (λ (_x : ), fr' _x fr _x) (λ (_x : ), id) φ
@[simp]
theorem first_order.language.bounded_formula.map_term_rel_id_id_id {L : first_order.language} {α : Type u'} {n : } (φ : n) :
first_order.language.bounded_formula.map_term_rel (λ (_x : ), id) (λ (_x : ), id) (λ (_x : ), id) φ = φ
def first_order.language.bounded_formula.map_term_rel_equiv {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} (ft : Π (n : ), L.term fin n) L'.term fin n)) (fr : Π (n : ), L.relations n L'.relations n) {n : } :
n L'.bounded_formula β n

An equivalence of bounded formulas given by an equivalence of terms and an equivalence of relations.

Equations
@[simp]
theorem first_order.language.bounded_formula.map_term_rel_equiv_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} (ft : Π (n : ), L.term fin n) L'.term fin n)) (fr : Π (n : ), L.relations n L'.relations n) {n : } (ᾰ : n) :
= first_order.language.bounded_formula.map_term_rel (λ (n : ), (ft n)) (λ (n : ), (fr n)) (λ (_x : ), id)
@[simp]
theorem first_order.language.bounded_formula.map_term_rel_equiv_symm_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} {β : Type v'} (ft : Π (n : ), L.term fin n) L'.term fin n)) (fr : Π (n : ), L.relations n L'.relations n) {n : } (ᾰ : L'.bounded_formula β n) :
= first_order.language.bounded_formula.map_term_rel (λ (n : ), ((ft n).symm)) (λ (n : ), ((fr n).symm)) (λ (_x : ), id)
def first_order.language.bounded_formula.relabel_aux {α : Type u'} {β : Type v'} {n : } (g : α β fin n) (k : ) :
α fin k β fin (n + k)

A function to help relabel the variables in bounded formulas.

Equations
@[simp]
theorem first_order.language.bounded_formula.sum_elim_comp_relabel_aux {M : Type w} {α : Type u'} {β : Type v'} {n m : } {g : α β fin n} {v : β M} {xs : fin (n + m) M} :
def first_order.language.bounded_formula.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (g : α β fin n) {k : } (φ : k) :
(n + k)

Relabels a bounded formula's variables along a particular function.

Equations
def first_order.language.bounded_formula.relabel_equiv {L : first_order.language} {α : Type u'} {β : Type v'} (g : α β) {k : } :
k k

Relabels a bounded formula's free variables along a bijection.

Equations
@[simp]
theorem first_order.language.bounded_formula.relabel_falsum {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (g : α β fin n) {k : } :
@[simp]
theorem first_order.language.bounded_formula.relabel_bot {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (g : α β fin n) {k : } :
@[simp]
theorem first_order.language.bounded_formula.relabel_imp {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (g : α β fin n) {k : } (φ ψ : k) :
@[simp]
theorem first_order.language.bounded_formula.relabel_not {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (g : α β fin n) {k : } (φ : k) :
@[simp]
theorem first_order.language.bounded_formula.relabel_all {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (g : α β fin n) {k : } (φ : (k + 1)) :
@[simp]
theorem first_order.language.bounded_formula.relabel_ex {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (g : α β fin n) {k : } (φ : (k + 1)) :
@[simp]
def first_order.language.bounded_formula.subst {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (φ : n) (f : α L.term β) :
n

Substitutes the variables in a given formula with terms.

Equations

A bijection sending formulas with constants to formulas with extra variables.

Equations
@[simp]

Turns the extra variables of a bounded formula into free variables.

Equations

An atomic formula is either equality or a relation symbol applied to terms. Note that `⊥` and `⊤` are not considered atomic in this convention.

theorem first_order.language.bounded_formula.is_atomic.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : } {φ : m} (h : φ.is_atomic) (f : α β fin n) :
theorem first_order.language.bounded_formula.is_atomic.lift_at {L : first_order.language} {α : Type u'} {l : } {φ : l} {k m : } (h : φ.is_atomic) :
theorem first_order.language.bounded_formula.is_atomic.cast_le {L : first_order.language} {α : Type u'} {n l : } {φ : l} {h : l n} (hφ : φ.is_atomic) :
inductive first_order.language.bounded_formula.is_qf {L : first_order.language} {α : Type u'} {n : } :
n Prop

A quantifier-free formula is a formula defined without quantifiers. These are all equivalent to boolean combinations of atomic formulas.

theorem first_order.language.bounded_formula.is_qf.not {L : first_order.language} {α : Type u'} {n : } {φ : n} (h : φ.is_qf) :
theorem first_order.language.bounded_formula.is_qf.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : } {φ : m} (h : φ.is_qf) (f : α β fin n) :
theorem first_order.language.bounded_formula.is_qf.lift_at {L : first_order.language} {α : Type u'} {l : } {φ : l} {k m : } (h : φ.is_qf) :
theorem first_order.language.bounded_formula.is_qf.cast_le {L : first_order.language} {α : Type u'} {n l : } {φ : l} {h : l n} (hφ : φ.is_qf) :

Indicates that a bounded formula is in prenex normal form - that is, it consists of quantifiers applied to a quantifier-free formula.

theorem first_order.language.bounded_formula.is_prenex.induction_on_all_not {L : first_order.language} {α : Type u'} {n : } {P : Π {n : }, n Prop} {φ : n} (h : φ.is_prenex) (hq : {m : } {ψ : m}, ψ.is_qf P ψ) (ha : {m : } {ψ : (m + 1)}, P ψ P ψ.all) (hn : {m : } {ψ : m}, P ψ P ψ.not) :
P φ
theorem first_order.language.bounded_formula.is_prenex.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : } {φ : m} (h : φ.is_prenex) (f : α β fin n) :
theorem first_order.language.bounded_formula.is_prenex.cast_le {L : first_order.language} {α : Type u'} {l : } {φ : l} (hφ : φ.is_prenex) {n : } {h : l n} :
theorem first_order.language.bounded_formula.is_prenex.lift_at {L : first_order.language} {α : Type u'} {l : } {φ : l} {k m : } (h : φ.is_prenex) :

An auxiliary operation to `first_order.language.bounded_formula.to_prenex`. If `φ` is quantifier-free and `ψ` is in prenex normal form, then `φ.to_prenex_imp_right ψ` is a prenex normal form for `φ.imp ψ`.

Equations

An auxiliary operation to `first_order.language.bounded_formula.to_prenex`. If `φ` and `ψ` are in prenex normal form, then `φ.to_prenex_imp ψ` is a prenex normal form for `φ.imp ψ`.

Equations

For any bounded formula `φ`, `φ.to_prenex` is a semantically-equivalent formula in prenex normal form.

Equations
@[simp]

Maps a bounded formula's symbols along a language map.

Equations
@[simp]

Maps a formula's symbols along a language map.

Equations

Maps a sentence's symbols along a language map.

Equations

Maps a theory's symbols along a language map.

Equations
@[simp]
theorem first_order.language.Lhom.mem_on_Theory {L : first_order.language} {L' : first_order.language} {g : L →ᴸ L'} {T : L.Theory} {φ : L'.sentence} :
φ g.on_Theory T (φ₀ : L.sentence), φ₀ T g.on_sentence φ₀ = φ

Maps a bounded formula's symbols along a language equivalence.

Equations
@[simp]

Maps a formula's symbols along a language equivalence.

Equations

Maps a sentence's symbols along a language equivalence.

Equations
def first_order.language.formula.relabel {L : first_order.language} {α : Type u'} {β : Type v'} (g : α β) :
L.formula α L.formula β

Relabels a formula's variables along a particular function.

Equations

The graph of a function as a first-order formula.

Equations
@[protected]

The negation of a formula.

Equations
@[protected]

The implication between formulas, as a formula.

Equations
@[protected]
def first_order.language.formula.iff {L : first_order.language} {α : Type u'} (φ ψ : L.formula α) :
L.formula α

The biimplication between formulas, as a formula.

Equations

A bijection sending formulas to sentences with constants.

Equations
@[protected]

The sentence indicating that a basic relation symbol is reflexive.

Equations
@[protected]

The sentence indicating that a basic relation symbol is irreflexive.

Equations
@[protected]

The sentence indicating that a basic relation symbol is symmetric.

Equations
@[protected]

The sentence indicating that a basic relation symbol is antisymmetric.

Equations
@[protected]

The sentence indicating that a basic relation symbol is transitive.

Equations
@[protected]

The sentence indicating that a basic relation symbol is total.

Equations
@[protected]

A sentence indicating that a structure has `n` distinct elements.

Equations

A theory indicating that a structure is infinite.

Equations
Instances for `first_order.language.infinite_theory`

A theory that indicates a structure is nonempty.

Equations
Instances for `first_order.language.nonempty_theory`

A theory indicating that each of a set of constants is distinct.

Equations