mathlibdocumentation

model_theory.syntax

Basics on First-Order Syntax #

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

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]
def first_order.language.term.var_finset_left {L : first_order.language} {α : Type u'} {β : Type v'} [decidable_eq α] :
L.term β)

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
theorem first_order.language.term.relabel_id {L : first_order.language} {α : Type u'} (t : L.term α) :
@[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 : β → γ) :
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
def first_order.language.constants.term {L : first_order.language} {α : Type u'} (c : L.constants) :
L.term α

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
@[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_21), (ts i).subst tf)
• = tf a
@[simp]
def first_order.language.Lhom.on_term {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L →ᴸ L') :
L.term αL'.term α

Maps a term's symbols along a language map.

Equations
@[simp]
@[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') :
def first_order.language.Lequiv.on_term {L : first_order.language} {L' : first_order.language} {α : Type u'} (φ : L ≃ᴸ L') :
L.term α L'.term α

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`
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

A sentence is a formula with no free variables.

Equations

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 nL.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 nL.term α) :
L.formula α

Applies a relation to terms as a bounded formula.

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

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) :
def first_order.language.bounded_formula.restrict_free_var {L : first_order.language} {α : Type u'} {β : Type v'} [decidable_eq α] {n : } (φ : n) (f : (φ.free_var_finset) → β) :
n

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

Equations
def first_order.language.bounded_formula.alls {L : first_order.language} {α : Type u'} {n : } :
nL.formula α

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

Equations
def first_order.language.bounded_formula.exs {L : first_order.language} {α : Type u'} {n : } :
nL.formula α

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 nL'.relations n) (h : Π (n : ), L'.bounded_formula β (g (n + 1))L'.bounded_formula β (g n + 1)) {n : } :
nL'.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 nL'.relations n) (ft' : Π (n : ), L'.term fin n)L''.term fin n)) (fr' : Π (n : ), L'.relations nL''.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} :
@[simp]
theorem first_order.language.bounded_formula.relabel_aux_sum_inl {α : Type u'} {n : } (k : ) :
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
@[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]
theorem first_order.language.bounded_formula.relabel_sum_inl {L : first_order.language} {α : Type u'} {n : } (φ : n) :
@[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
@[simp]
def first_order.language.bounded_formula.to_formula {L : first_order.language} {α : Type u'} {n : } :
nL.formula fin n)

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

Equations
inductive first_order.language.bounded_formula.is_atomic {L : first_order.language} {α : Type u'} {n : } :
n → Prop

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.not_all_is_atomic {L : first_order.language} {α : Type u'} {n : } (φ : (n + 1)) :
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_atomic.is_qf {L : first_order.language} {α : Type u'} {n : } {φ : n} :
φ.is_atomic → φ.is_qf
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) :
theorem first_order.language.bounded_formula.not_all_is_qf {L : first_order.language} {α : Type u'} {n : } (φ : (n + 1)) :
theorem first_order.language.bounded_formula.not_ex_is_qf {L : first_order.language} {α : Type u'} {n : } (φ : (n + 1)) :
inductive first_order.language.bounded_formula.is_prenex {L : first_order.language} {α : Type u'} {n : } :
n → Prop

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_qf.is_prenex {L : first_order.language} {α : Type u'} {n : } {φ : n} :
φ.is_qf → φ.is_prenex
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_qfP ψ) (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
theorem first_order.language.bounded_formula.is_qf.to_prenex_imp_right {L : first_order.language} {α : Type u'} {n : } {φ ψ : n} :
ψ.is_qf = φ.imp ψ
def first_order.language.bounded_formula.to_prenex_imp {L : first_order.language} {α : Type u'} {n : } :
n n n

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
theorem first_order.language.bounded_formula.is_qf.to_prenex_imp {L : first_order.language} {α : Type u'} {n : } {φ ψ : n} :
φ.is_qf
theorem first_order.language.bounded_formula.is_prenex_to_prenex_imp {L : first_order.language} {α : Type u'} {n : } {φ ψ : n} (hφ : φ.is_prenex) (hψ : ψ.is_prenex) :
def first_order.language.bounded_formula.to_prenex {L : first_order.language} {α : Type u'} {n : } :
n n

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

Equations
@[simp]
def first_order.language.Lhom.on_bounded_formula {L : first_order.language} {L' : first_order.language} {α : Type u'} (g : L →ᴸ L') {k : } :
kL'.bounded_formula α k

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

Equations
@[simp]
@[simp]
theorem first_order.language.Lhom.comp_on_bounded_formula {L : first_order.language} {L' : first_order.language} {α : Type u'} {n : } {L'' : first_order.language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
def first_order.language.Lhom.on_formula {L : first_order.language} {L' : first_order.language} {α : Type u'} (g : L →ᴸ L') :
L.formula αL'.formula α

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 φ₀ = φ
@[simp]

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

Equations
@[simp]
theorem first_order.language.Lequiv.on_bounded_formula_apply {L : first_order.language} {L' : first_order.language} {α : Type u'} {n : } (φ : L ≃ᴸ L') (ᾰ : n) :

Maps a formula's symbols along a language equivalence.

Equations
@[simp]
@[simp]

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]
def first_order.language.formula.not {L : first_order.language} {α : Type u'} (φ : L.formula α) :
L.formula α

The negation of a formula.

Equations
@[protected]
def first_order.language.formula.imp {L : first_order.language} {α : Type u'} :
L.formula αL.formula αL.formula α

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
@[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