mathlib documentation

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 #

Implementation Notes #

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 β)finset α

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]
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
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
@[simp]
def first_order.language.term.constants_to_vars {L : first_order.language} {α : Type u'} {γ : Type u_5} :
(L.with_constants γ).term αL.term α)

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

Equations
def first_order.language.term.constants_vars_equiv {L : first_order.language} {α : Type u'} {γ : Type u_5} :
(L.with_constants γ).term α L.term α)

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

Equations
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
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
@[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]
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
@[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 nL.term fin 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)) :

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)) :

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)) :

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]

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 : } (φ : L.bounded_formula α (n + 1)) :

Puts an quantifier on a bounded formula.

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

The biimplication between two bounded formulas.

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.lift_at {L : first_order.language} {α : Type u'} {n : } (n' m : ) :
L.bounded_formula α nL.bounded_formula α (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 : } (φ : L.bounded_formula α n) :
first_order.language.bounded_formula.map_term_rel ft' fr' (λ (_x : ), id) (first_order.language.bounded_formula.map_term_rel ft fr (λ (_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 : } (φ : L.bounded_formula α 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 : } :

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 : } (ᾰ : L.bounded_formula α n) :
@[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) :
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 : } (φ : L.bounded_formula α k) :
L.bounded_formula β (n + k)

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

Equations
@[simp]
theorem first_order.language.bounded_formula.relabel_bot {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (g : α → β fin n) {k : } :
@[simp]
@[simp]
def first_order.language.bounded_formula.subst {L : first_order.language} {α : Type u'} {β : Type v'} {n : } (φ : L.bounded_formula α n) (f : α → L.term β) :

Substitutes the variables in a given formula with terms.

Equations
inductive first_order.language.bounded_formula.is_atomic {L : first_order.language} {α : Type u'} {n : } :
L.bounded_formula α 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.is_atomic.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : } {φ : L.bounded_formula α m} (h : φ.is_atomic) (f : α → β fin n) :
inductive first_order.language.bounded_formula.is_qf {L : first_order.language} {α : Type u'} {n : } :
L.bounded_formula α 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 : } {φ : L.bounded_formula α n} (h : φ.is_qf) :
theorem first_order.language.bounded_formula.is_qf.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : } {φ : L.bounded_formula α m} (h : φ.is_qf) (f : α → β fin n) :
inductive first_order.language.bounded_formula.is_prenex {L : first_order.language} {α : Type u'} {n : } :
L.bounded_formula α 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_prenex.induction_on_all_not {L : first_order.language} {α : Type u'} {n : } {P : Π {n : }, L.bounded_formula α n → Prop} {φ : L.bounded_formula α n} (h : φ.is_prenex) (hq : ∀ {m : } {ψ : L.bounded_formula α m}, ψ.is_qfP ψ) (ha : ∀ {m : } {ψ : L.bounded_formula α (m + 1)}, P ψP ψ.all) (hn : ∀ {m : } {ψ : L.bounded_formula α m}, P ψP ψ.not) :
P φ
theorem first_order.language.bounded_formula.is_prenex.relabel {L : first_order.language} {α : Type u'} {β : Type v'} {n m : } {φ : L.bounded_formula α m} (h : φ.is_prenex) (f : α → β fin n) :

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
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 φ₀ = φ

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

Equations

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

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