Documentation

Mathlib.ModelTheory.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 FirstOrder.Language.Term (L : 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

The Finset of variables used in a given term.

Equations
def FirstOrder.Language.Term.varFinsetLeft {L : Language} {α : Type u'} {β : Type v'} [DecidableEq α] :
L.Term (α β)Finset α

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

Equations
def FirstOrder.Language.Term.relabel {L : Language} {α : Type u'} {β : Type v'} (g : αβ) :
L.Term αL.Term β

Relabels a term's variables along a particular function.

Equations
theorem FirstOrder.Language.Term.relabel_id {L : Language} {α : Type u'} (t : L.Term α) :
@[simp]
theorem FirstOrder.Language.Term.relabel_relabel {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (f : αβ) (g : βγ) (t : L.Term α) :
relabel g (relabel f t) = relabel (g f) t
@[simp]
theorem FirstOrder.Language.Term.relabel_comp_relabel {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (f : αβ) (g : βγ) :
def FirstOrder.Language.Term.relabelEquiv {L : Language} {α : Type u'} {β : Type v'} (g : α β) :
L.Term α L.Term β

Relabels a term's variables along a bijection.

Equations
@[simp]
theorem FirstOrder.Language.Term.relabelEquiv_symm_apply {L : Language} {α : Type u'} {β : Type v'} (g : α β) (a✝ : L.Term β) :
(relabelEquiv g).symm a✝ = relabel (⇑g.symm) a✝
@[simp]
theorem FirstOrder.Language.Term.relabelEquiv_apply {L : Language} {α : Type u'} {β : Type v'} (g : α β) (a✝ : L.Term α) :
(relabelEquiv g) a✝ = relabel (⇑g) a✝
def FirstOrder.Language.Term.restrictVar {L : Language} {α : Type u'} {β : Type v'} [DecidableEq α] (t : L.Term α) (_f : { x : α // x t.varFinset }β) :
L.Term β

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

Equations
def FirstOrder.Language.Term.restrictVarLeft {L : Language} {α : Type u'} {β : Type v'} [DecidableEq α] {γ : Type u_2} (t : L.Term (α γ)) (_f : { x : α // x t.varFinsetLeft }β) :
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 FirstOrder.Language.Functions.apply₁ {L : Language} {α : Type u'} (f : L.Functions 1) (t : L.Term α) :
L.Term α

Applies a unary function to a term.

Equations
def FirstOrder.Language.Functions.apply₂ {L : Language} {α : Type u'} (f : L.Functions 2) (t₁ t₂ : L.Term α) :
L.Term α

Applies a binary function to two terms.

Equations
def FirstOrder.Language.Term.constantsToVars {L : Language} {α : Type u'} {γ : Type u_1} :
(L.withConstants γ).Term αL.Term (γ α)

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

Equations
def FirstOrder.Language.Term.constantsVarsEquiv {L : Language} {α : Type u'} {γ : Type u_1} :
(L.withConstants γ).Term α L.Term (γ α)

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

Equations
@[simp]
def FirstOrder.Language.Term.constantsVarsEquivLeft {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} :
(L.withConstants γ).Term (α β) L.Term ((γ α) β)

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

Equations
@[simp]
@[simp]
theorem FirstOrder.Language.Term.constantsVarsEquivLeft_symm_apply {L : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} (t : L.Term ((γ α) β)) :
def FirstOrder.Language.Term.liftAt {L : 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
def FirstOrder.Language.Term.subst {L : Language} {α : Type u'} {β : Type v'} :
L.Term α(αL.Term β)L.Term β

Substitutes the variables in a given term with terms.

Equations

&n is notation for the n-th free variable of a bounded formula.

Equations
def FirstOrder.Language.LHom.onTerm {L : Language} {L' : Language} {α : Type u'} (φ : L →ᴸ L') :
L.Term αL'.Term α

Maps a term's symbols along a language map.

Equations
@[simp]
theorem FirstOrder.Language.LHom.comp_onTerm {L : Language} {L' : Language} {α : Type u'} {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
(φ.comp ψ).onTerm = φ.onTerm ψ.onTerm
def FirstOrder.Language.LEquiv.onTerm {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') :
L.Term α L'.Term α

Maps a term's symbols along a language equivalence.

Equations
@[simp]
theorem FirstOrder.Language.LEquiv.onTerm_apply {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') (a✝ : L.Term α) :
φ.onTerm a✝ = φ.toLHom.onTerm a✝
@[simp]
theorem FirstOrder.Language.LEquiv.onTerm_symm_apply {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') (a✝ : L'.Term α) :
φ.onTerm.symm a✝ = φ.invLHom.onTerm a✝
@[deprecated FirstOrder.Language.LEquiv.onTerm (since := "2025-03-31")]
def FirstOrder.Language.Lequiv.onTerm {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') :
L.Term α L'.Term α

Maps a term's symbols along a language equivalence. Deprecated in favor of LEquiv.onTerm.

Equations
inductive FirstOrder.Language.BoundedFormula (L : Language) (α : Type u') :
Type (max u v u')

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

Instances For
@[reducible, inline]
abbrev FirstOrder.Language.Formula (L : Language) (α : Type u') :
Type (max u v u')

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

Equations
@[reducible, inline]

A sentence is a formula with no free variables.

Equations
@[reducible, inline]
abbrev FirstOrder.Language.Theory (L : Language) :
Type (max u v)

A theory is a set of sentences.

Equations
def FirstOrder.Language.Relations.boundedFormula {L : 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 FirstOrder.Language.Relations.boundedFormula₁ {L : 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 FirstOrder.Language.Relations.boundedFormula₂ {L : 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 FirstOrder.Language.Term.bdEqual {L : Language} {α : Type u'} {n : } (t₁ t₂ : L.Term (α Fin n)) :

The equality of two terms as a bounded formula.

Equations
def FirstOrder.Language.Relations.formula {L : 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 FirstOrder.Language.Relations.formula₁ {L : Language} {α : Type u'} (r : L.Relations 1) (t : L.Term α) :
L.Formula α

Applies a unary relation to a term as a formula.

Equations
def FirstOrder.Language.Relations.formula₂ {L : 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 FirstOrder.Language.Term.equal {L : Language} {α : Type u'} (t₁ t₂ : L.Term α) :
L.Formula α

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

Equations
@[match_pattern]

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

Equations
@[match_pattern]
def FirstOrder.Language.BoundedFormula.ex {L : Language} {α : Type u'} {n : } (φ : L.BoundedFormula α (n + 1)) :

Puts an quantifier on a bounded formula.

Equations
def FirstOrder.Language.BoundedFormula.iff {L : Language} {α : Type u'} {n : } (φ ψ : L.BoundedFormula α n) :

The biimplication between two bounded formulas.

Equations
@[simp]
theorem FirstOrder.Language.BoundedFormula.castLE_rfl {L : Language} {α : Type u'} {n : } (h : n n) (φ : L.BoundedFormula α n) :
castLE h φ = φ
@[simp]
theorem FirstOrder.Language.BoundedFormula.castLE_castLE {L : Language} {α : Type u'} {k m n : } (km : k m) (mn : m n) (φ : L.BoundedFormula α k) :
castLE mn (castLE km φ) = castLE φ
@[simp]
theorem FirstOrder.Language.BoundedFormula.castLE_comp_castLE {L : Language} {α : Type u'} {k m n : } (km : k m) (mn : m n) :
def FirstOrder.Language.BoundedFormula.restrictFreeVar {L : Language} {α : Type u'} {β : Type v'} [DecidableEq α] {n : } (φ : L.BoundedFormula α n) (_f : { x : α // x φ.freeVarFinset }β) :

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 FirstOrder.Language.BoundedFormula.liftAt {L : Language} {α : Type u'} {n : } (n' _m : ) :
L.BoundedFormula α nL.BoundedFormula α (n + n')

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem FirstOrder.Language.BoundedFormula.mapTermRel_mapTermRel {L : Language} {L' : Language} {α : Type u'} {β : Type v'} {γ : Type u_1} {L'' : 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.BoundedFormula α n) :
mapTermRel ft' fr' (fun (x : ) => id) (mapTermRel ft fr (fun (x : ) => id) φ) = mapTermRel (fun (x : ) => ft' x ft x) (fun (x : ) => fr' x fr x) (fun (x : ) => id) φ
@[simp]
theorem FirstOrder.Language.BoundedFormula.mapTermRel_id_id_id {L : Language} {α : Type u'} {n : } (φ : L.BoundedFormula α n) :
mapTermRel (fun (x : ) => id) (fun (x : ) => id) (fun (x : ) => id) φ = φ
def FirstOrder.Language.BoundedFormula.mapTermRelEquiv {L : Language} {L' : 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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem FirstOrder.Language.BoundedFormula.mapTermRelEquiv_apply {L : Language} {L' : Language} {α : Type u'} {β : Type v'} (ft : (n : ) → L.Term (α Fin n) L'.Term (β Fin n)) (fr : (n : ) → L.Relations n L'.Relations n) {n : } (a✝ : L.BoundedFormula α n) :
(mapTermRelEquiv ft fr) a✝ = mapTermRel (fun (n : ) => (ft n)) (fun (n : ) => (fr n)) (fun (x : ) => id) a✝
@[simp]
theorem FirstOrder.Language.BoundedFormula.mapTermRelEquiv_symm_apply {L : Language} {L' : Language} {α : Type u'} {β : Type v'} (ft : (n : ) → L.Term (α Fin n) L'.Term (β Fin n)) (fr : (n : ) → L.Relations n L'.Relations n) {n : } (a✝ : L'.BoundedFormula β n) :
(mapTermRelEquiv ft fr).symm a✝ = mapTermRel (fun (n : ) => (ft n).symm) (fun (n : ) => (fr n).symm) (fun (x : ) => id) a✝
def FirstOrder.Language.BoundedFormula.relabelAux {α : 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 FirstOrder.Language.BoundedFormula.sumElim_comp_relabelAux {M : Type w} {α : Type u'} {β : Type v'} {n m : } {g : αβ Fin n} {v : βM} {xs : Fin (n + m)M} :
@[deprecated FirstOrder.Language.BoundedFormula.sumElim_comp_relabelAux (since := "2025-02-21")]
theorem FirstOrder.Language.BoundedFormula.sum_elim_comp_relabelAux {M : Type w} {α : Type u'} {β : Type v'} {n m : } {g : αβ Fin n} {v : βM} {xs : Fin (n + m)M} :

Alias of FirstOrder.Language.BoundedFormula.sumElim_comp_relabelAux.

@[deprecated FirstOrder.Language.BoundedFormula.relabelAux_sumInl (since := "2025-02-21")]

Alias of FirstOrder.Language.BoundedFormula.relabelAux_sumInl.

def FirstOrder.Language.BoundedFormula.relabel {L : Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α k) :
L.BoundedFormula β (n + k)

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

Equations
  • One or more equations did not get rendered due to their size.
def FirstOrder.Language.BoundedFormula.relabelEquiv {L : Language} {α : Type u'} {β : Type v'} (g : α β) {k : } :

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem FirstOrder.Language.BoundedFormula.relabel_falsum {L : Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } :
@[simp]
theorem FirstOrder.Language.BoundedFormula.relabel_bot {L : Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } :
@[simp]
theorem FirstOrder.Language.BoundedFormula.relabel_imp {L : Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ ψ : L.BoundedFormula α k) :
relabel g (φ.imp ψ) = (relabel g φ).imp (relabel g ψ)
@[simp]
theorem FirstOrder.Language.BoundedFormula.relabel_not {L : Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α k) :
relabel g φ.not = (relabel g φ).not
@[simp]
theorem FirstOrder.Language.BoundedFormula.relabel_all {L : Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α (k + 1)) :
relabel g φ.all = (relabel g φ).all
@[simp]
theorem FirstOrder.Language.BoundedFormula.relabel_ex {L : Language} {α : Type u'} {β : Type v'} {n : } (g : αβ Fin n) {k : } (φ : L.BoundedFormula α (k + 1)) :
relabel g φ.ex = (relabel g φ).ex
@[simp]
@[deprecated FirstOrder.Language.BoundedFormula.relabel_sumInl (since := "2025-02-21")]

Alias of FirstOrder.Language.BoundedFormula.relabel_sumInl.

def FirstOrder.Language.BoundedFormula.subst {L : Language} {α : Type u'} {β : Type v'} {n : } (φ : L.BoundedFormula α n) (f : αL.Term β) :

Substitutes the variables in a given formula with terms.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations
  • One or more equations did not get rendered due to their size.
noncomputable def FirstOrder.Language.BoundedFormula.iSup {L : Language} {α : Type u'} {β : Type v'} {n : } [Finite β] (f : βL.BoundedFormula α n) :

Take the disjunction of a finite set of formulas

Equations
noncomputable def FirstOrder.Language.BoundedFormula.iInf {L : Language} {α : Type u'} {β : Type v'} {n : } [Finite β] (f : βL.BoundedFormula α n) :

Take the conjunction of a finite set of formulas

Equations
@[simp]
theorem FirstOrder.Language.LHom.comp_onBoundedFormula {L : Language} {L' : Language} {α : Type u'} {n : } {L'' : Language} (φ : L' →ᴸ L'') (ψ : L →ᴸ L') :
def FirstOrder.Language.LHom.onFormula {L : Language} {L' : 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
def FirstOrder.Language.LHom.onTheory {L : Language} {L' : Language} (g : L →ᴸ L') (T : L.Theory) :

Maps a theory's symbols along a language map.

Equations
@[simp]
theorem FirstOrder.Language.LHom.mem_onTheory {L : Language} {L' : Language} {g : L →ᴸ L'} {T : L.Theory} {φ : L'.Sentence} :
φ g.onTheory T φ₀T, g.onSentence φ₀ = φ
def FirstOrder.Language.LEquiv.onBoundedFormula {L : Language} {L' : Language} {α : Type u'} {n : } (φ : L ≃ᴸ L') :

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

Equations
@[simp]
theorem FirstOrder.Language.LEquiv.onBoundedFormula_apply {L : Language} {L' : Language} {α : Type u'} {n : } (φ : L ≃ᴸ L') (a✝ : L.BoundedFormula α n) :
@[simp]
theorem FirstOrder.Language.LEquiv.onBoundedFormula_symm_apply {L : Language} {L' : Language} {α : Type u'} {n : } (φ : L ≃ᴸ L') (a✝ : L'.BoundedFormula α n) :
def FirstOrder.Language.LEquiv.onFormula {L : Language} {L' : Language} {α : Type u'} (φ : L ≃ᴸ L') :
L.Formula α L'.Formula α

Maps a formula's symbols along a language equivalence.

Equations
@[simp]
@[simp]

Maps a sentence's symbols along a language equivalence.

Equations

The equality of two terms as a bounded formula.

Equations

The implication between two bounded formulas

Equations

The universal quantifier over bounded formulas

Equations

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

Equations

The biimplication between two bounded formulas.

Equations

Puts an quantifier on a bounded formula.

Equations
def FirstOrder.Language.Formula.relabel {L : Language} {α : Type u'} {β : Type v'} (g : αβ) :
L.Formula αL.Formula β

Relabels a formula's variables along a particular function.

Equations
def FirstOrder.Language.Formula.graph {L : Language} {n : } (f : L.Functions n) :
L.Formula (Fin (n + 1))

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

Equations
@[reducible, inline]
abbrev FirstOrder.Language.Formula.not {L : Language} {α : Type u'} (φ : L.Formula α) :
L.Formula α

The negation of a formula.

Equations
@[reducible, inline]
abbrev FirstOrder.Language.Formula.imp {L : Language} {α : Type u'} :
L.Formula αL.Formula αL.Formula α

The implication between formulas, as a formula.

Equations
noncomputable def FirstOrder.Language.Formula.iAlls {L : Language} {α : Type u'} (β : Type v') [Finite β] (φ : L.Formula (α β)) :
L.Formula α

iAlls f φ transforms a L.Formula (α ⊕ β) into a L.Formula β by universally quantifying over all variables Sum.inr _.

Equations
noncomputable def FirstOrder.Language.Formula.iExs {L : Language} {α : Type u'} (β : Type v') [Finite β] (φ : L.Formula (α β)) :
L.Formula α

iExs f φ transforms a L.Formula (α ⊕ β) into a L.Formula β by existentially quantifying over all variables Sum.inr _.

Equations
noncomputable def FirstOrder.Language.Formula.iExsUnique {L : Language} {α : Type u'} (β : Type v') [Finite β] (φ : L.Formula (α β)) :
L.Formula α

iExsUnique f φ transforms a L.Formula (α ⊕ β) into a L.Formula β by existentially quantifying over all variables Sum.inr _ and asserting that the solution should be unique

Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
abbrev FirstOrder.Language.Formula.iff {L : Language} {α : Type u'} (φ ψ : L.Formula α) :
L.Formula α

The biimplication between formulas, as a formula.

Equations

The sentence indicating that a basic relation symbol is reflexive.

Equations

The sentence indicating that a basic relation symbol is irreflexive.

Equations

The sentence indicating that a basic relation symbol is symmetric.

Equations
  • One or more equations did not get rendered due to their size.

The sentence indicating that a basic relation symbol is antisymmetric.

Equations
  • One or more equations did not get rendered due to their size.

The sentence indicating that a basic relation symbol is transitive.

Equations
  • One or more equations did not get rendered due to their size.

The sentence indicating that a basic relation symbol is total.

Equations
  • One or more equations did not get rendered due to their size.

A sentence indicating that a structure has n distinct elements.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations