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
FirstOrder.Language.Term
is defined so thatL.Term α
is the type ofL
-terms with free variables indexed byα
. - A
FirstOrder.Language.Formula
is defined so thatL.Formula α
is the type ofL
-formulas with free variables indexed byα
. - A
FirstOrder.Language.Sentence
is a formula with no free variables. - A
FirstOrder.Language.Theory
is a set of sentences. - The variables of terms and formulas can be relabelled with
FirstOrder.Language.Term.relabel
,FirstOrder.Language.BoundedFormula.relabel
, andFirstOrder.Language.Formula.relabel
. - Given an operation on terms and an operation on relations,
FirstOrder.Language.BoundedFormula.mapTermRel
gives an operation on formulas. FirstOrder.Language.BoundedFormula.castLE
adds moreFin
-indexed variables.FirstOrder.Language.BoundedFormula.liftAt
raises the indexes of theFin
-indexed variables above a particular index.FirstOrder.Language.Term.subst
andFirstOrder.Language.BoundedFormula.subst
substitute variables with given terms.- Language maps can act on syntactic objects with functions such as
FirstOrder.Language.LHom.onFormula
. FirstOrder.Language.Term.constantsVarsEquiv
andFirstOrder.Language.BoundedFormula.constantsVarsEquiv
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.BoundedFormula α n
is a formula with some variables indexed by a typeα
, which cannot be quantified over, and some indexed byFin n
, which can. For anyφ : L.BoundedFormula α (n + 1)
, we define the formula∀' φ : L.BoundedFormula α n
by universally quantifying over the variable indexed byn : Fin (n + 1)
.
References #
For the Flypitch project:
- [J. Han, F. van Doorn, A formal proof of the independence of the continuum hypothesis] [flypitch_cpp]
- [J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis][flypitch_itp]
A term on α
is either a variable indexed by an element of α
or a function symbol applied to simpler terms.
Equations
- (FirstOrder.Language.var a).instDecidableEq (FirstOrder.Language.var b) = decidable_of_iff (a = b) ⋯
- (FirstOrder.Language.func f xs).instDecidableEq (FirstOrder.Language.func g ys) = if h : m = n then decidable_of_iff (f = ⋯ ▸ g ∧ ∀ (i : Fin m), xs i = ys (Fin.cast h i)) ⋯ else isFalse ⋯
- (FirstOrder.Language.var a).instDecidableEq (FirstOrder.Language.func _f _ts) = isFalse ⋯
- (FirstOrder.Language.func _f _ts).instDecidableEq (FirstOrder.Language.var a) = isFalse ⋯
The Finset
of variables used in a given term.
Equations
- (FirstOrder.Language.var i).varFinset = {i}
- (FirstOrder.Language.func _f ts).varFinset = Finset.univ.biUnion fun (i : Fin l) => (ts i).varFinset
The Finset
of variables from the left side of a sum used in a given term.
Equations
- (FirstOrder.Language.var (Sum.inl i)).varFinsetLeft = {i}
- (FirstOrder.Language.var (Sum.inr _i)).varFinsetLeft = ∅
- (FirstOrder.Language.func _f ts).varFinsetLeft = Finset.univ.biUnion fun (i : Fin l) => (ts i).varFinsetLeft
Relabels a term's variables along a particular function.
Equations
- FirstOrder.Language.Term.relabel g (FirstOrder.Language.var i) = FirstOrder.Language.var (g i)
- FirstOrder.Language.Term.relabel g (FirstOrder.Language.func _f ts) = FirstOrder.Language.func _f fun {i : Fin l} => FirstOrder.Language.Term.relabel g (ts i)
Relabels a term's variables along a bijection.
Equations
- FirstOrder.Language.Term.relabelEquiv g = { toFun := FirstOrder.Language.Term.relabel ⇑g, invFun := FirstOrder.Language.Term.relabel ⇑g.symm, left_inv := ⋯, right_inv := ⋯ }
Restricts a term to use only a set of the given variables.
Equations
- (FirstOrder.Language.var a).restrictVar f = FirstOrder.Language.var (f ⟨a, ⋯⟩)
- (FirstOrder.Language.func F ts).restrictVar f = FirstOrder.Language.func F fun (i : Fin l) => (ts i).restrictVar (f ∘ Set.inclusion ⋯)
Restricts a term to use only a set of the given variables on the left side of a sum.
Equations
- (FirstOrder.Language.var (Sum.inl a)).restrictVarLeft f = FirstOrder.Language.var (Sum.inl (f ⟨a, ⋯⟩))
- (FirstOrder.Language.var (Sum.inr a)).restrictVarLeft _f = FirstOrder.Language.var (Sum.inr a)
- (FirstOrder.Language.func F ts).restrictVarLeft f = FirstOrder.Language.func F fun (i : Fin l) => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)
The representation of a constant symbol as a term.
Equations
Sends a term with constants to a term with extra variables.
Equations
- One or more equations did not get rendered due to their size.
- (FirstOrder.Language.var a).constantsToVars = FirstOrder.Language.var (Sum.inr a)
Sends a term with extra variables to a term with constants.
Equations
- (FirstOrder.Language.var (Sum.inr a)).varsToConstants = FirstOrder.Language.var a
- (FirstOrder.Language.var (Sum.inl c)).varsToConstants = FirstOrder.Language.Constants.term (Sum.inr c)
- (FirstOrder.Language.func f ts).varsToConstants = FirstOrder.Language.func (Sum.inl f) fun (i : Fin l) => (ts i).varsToConstants
A bijection between terms with constants and terms with extra variables.
Equations
- FirstOrder.Language.Term.constantsVarsEquiv = { toFun := FirstOrder.Language.Term.constantsToVars, invFun := FirstOrder.Language.Term.varsToConstants, left_inv := ⋯, right_inv := ⋯ }
A bijection between terms with constants and terms with extra variables.
Equations
Raises all of the Fin
-indexed variables of a term greater than or equal to m
by n'
.
Equations
- FirstOrder.Language.Term.liftAt n' m = FirstOrder.Language.Term.relabel (Sum.map id fun (i : Fin n) => if ↑i < m then Fin.castAdd n' i else i.addNat n')
Substitutes the variables in a given term with terms.
Equations
- (FirstOrder.Language.var a).subst x✝ = x✝ a
- (FirstOrder.Language.func f ts).subst x✝ = FirstOrder.Language.func f fun (i : Fin l) => (ts i).subst x✝
&n
is notation for the n
-th free variable of a bounded formula.
Equations
- FirstOrder.«term&_» = Lean.ParserDescr.node `FirstOrder.«term&_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 1023))
Maps a term's symbols along a language map.
Equations
- φ.onTerm (FirstOrder.Language.var i) = FirstOrder.Language.var i
- φ.onTerm (FirstOrder.Language.func _f ts) = FirstOrder.Language.func (φ.onFunction _f) fun (i : Fin l) => φ.onTerm (ts i)
Maps a term's symbols along a language equivalence. Deprecated in favor of LEquiv.onTerm
.
BoundedFormula α n
is the type of formulas with free variables indexed by α
and up to n
additional free variables.
- falsum {L : Language} {α : Type u'} {n : ℕ} : L.BoundedFormula α n
- equal {L : Language} {α : Type u'} {n : ℕ} (t₁ t₂ : L.Term (α ⊕ Fin n)) : L.BoundedFormula α n
- rel {L : Language} {α : Type u'} {n l : ℕ} (R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)) : L.BoundedFormula α n
- imp
{L : Language}
{α : Type u'}
{n : ℕ}
(f₁ f₂ : L.BoundedFormula α n)
: L.BoundedFormula α n
The implication between two bounded formulas
- all
{L : Language}
{α : Type u'}
{n : ℕ}
(f : L.BoundedFormula α (n + 1))
: L.BoundedFormula α n
The universal quantifier over bounded formulas
Formula α
is the type of formulas with all free variables indexed by α
.
Equations
- L.Formula α = L.BoundedFormula α 0
Applies a relation to terms as a bounded formula.
Equations
Applies a unary relation to a term as a bounded formula.
Equations
- r.boundedFormula₁ t = r.boundedFormula ![t]
Applies a binary relation to two terms as a bounded formula.
Equations
- r.boundedFormula₂ t₁ t₂ = r.boundedFormula ![t₁, t₂]
The equality of two terms as a bounded formula.
Equations
- t₁.bdEqual t₂ = FirstOrder.Language.BoundedFormula.equal t₁ t₂
Applies a relation to terms as a bounded formula.
Equations
- R.formula ts = R.boundedFormula fun (i : Fin n) => FirstOrder.Language.Term.relabel Sum.inl (ts i)
The equality of two terms as a first-order formula.
Equations
Equations
The negation of a bounded formula is also a bounded formula.
Puts an ∃
quantifier on a bounded formula.
Equations
- FirstOrder.Language.BoundedFormula.instMin = { min := fun (f g : L.BoundedFormula α n) => (f.imp g.not).not }
Equations
- FirstOrder.Language.BoundedFormula.instMax = { max := fun (f g : L.BoundedFormula α n) => f.not.imp g }
The biimplication between two bounded formulas.
The Finset
of variables used in a given formula.
Equations
- FirstOrder.Language.BoundedFormula.falsum.freeVarFinset = ∅
- (FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset = t₁.varFinsetLeft ∪ t₂.varFinsetLeft
- (FirstOrder.Language.BoundedFormula.rel _R ts).freeVarFinset = Finset.univ.biUnion fun (i : Fin l) => (ts i).varFinsetLeft
- (f₁.imp f₂).freeVarFinset = f₁.freeVarFinset ∪ f₂.freeVarFinset
- f.all.freeVarFinset = f.freeVarFinset
Casts L.BoundedFormula α m
as L.BoundedFormula α n
, where m ≤ n
.
Equations
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.BoundedFormula.castLE x✝ FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
- FirstOrder.Language.BoundedFormula.castLE x✝ (f₁.imp f₂) = (FirstOrder.Language.BoundedFormula.castLE x✝ f₁).imp (FirstOrder.Language.BoundedFormula.castLE x✝ f₂)
- FirstOrder.Language.BoundedFormula.castLE x✝ f.all = (FirstOrder.Language.BoundedFormula.castLE ⋯ f).all
Restricts a bounded formula to only use a particular set of free variables.
Equations
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.BoundedFormula.falsum.restrictFreeVar _f = FirstOrder.Language.BoundedFormula.falsum
- (FirstOrder.Language.BoundedFormula.rel R ts).restrictFreeVar f = FirstOrder.Language.BoundedFormula.rel R fun (i : Fin l) => (ts i).restrictVarLeft (f ∘ Set.inclusion ⋯)
- (φ₁.imp φ₂).restrictFreeVar f = (φ₁.restrictFreeVar (f ∘ Set.inclusion ⋯)).imp (φ₂.restrictFreeVar (f ∘ Set.inclusion ⋯))
- φ.all.restrictFreeVar f = (φ.restrictFreeVar f).all
Maps bounded formulas along a map of terms and a map of relations.
Equations
- FirstOrder.Language.BoundedFormula.mapTermRel ft fr h FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
- FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.BoundedFormula.equal (ft x✝ t₁) (ft x✝ t₂)
- FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (FirstOrder.Language.BoundedFormula.rel _R ts) = FirstOrder.Language.BoundedFormula.rel (fr l _R) fun (i : Fin l) => ft x✝ (ts i)
- FirstOrder.Language.BoundedFormula.mapTermRel ft fr h (f₁.imp f₂) = (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f₁).imp (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f₂)
- FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f.all = (h x✝ (FirstOrder.Language.BoundedFormula.mapTermRel ft fr h f)).all
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.
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.
A function to help relabel the variables in bounded formulas.
Equations
- FirstOrder.Language.BoundedFormula.relabelAux g k = Sum.map id ⇑finSumFinEquiv ∘ ⇑(Equiv.sumAssoc β (Fin n) (Fin k)) ∘ Sum.map g id
Alias of FirstOrder.Language.BoundedFormula.sumElim_comp_relabelAux
.
Alias of FirstOrder.Language.BoundedFormula.relabelAux_sumInl
.
Relabels a bounded formula's variables along a particular function.
Equations
- One or more equations did not get rendered due to their size.
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.
Turns the extra variables of a bounded formula into free variables.
Equations
- FirstOrder.Language.BoundedFormula.falsum.toFormula = FirstOrder.Language.BoundedFormula.falsum
- (FirstOrder.Language.BoundedFormula.equal t₁ t₂).toFormula = t₁.equal t₂
- (FirstOrder.Language.BoundedFormula.rel _R ts).toFormula = _R.formula ts
- (f₁.imp f₂).toFormula = FirstOrder.Language.BoundedFormula.imp f₁.toFormula f₂.toFormula
- f.all.toFormula = (FirstOrder.Language.BoundedFormula.relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f.toFormula).all
Take the disjunction of a finite set of formulas
Equations
- FirstOrder.Language.BoundedFormula.iSup f = List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊔ x2) ⊥ (List.map f Finset.univ.toList)
Take the conjunction of a finite set of formulas
Equations
- FirstOrder.Language.BoundedFormula.iInf f = List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊓ x2) ⊤ (List.map f Finset.univ.toList)
Maps a bounded formula's symbols along a language map.
Equations
- g.onBoundedFormula FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
- g.onBoundedFormula (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = (g.onTerm t₁).bdEqual (g.onTerm t₂)
- g.onBoundedFormula (FirstOrder.Language.BoundedFormula.rel _R ts) = (g.onRelation _R).boundedFormula (g.onTerm ∘ ts)
- g.onBoundedFormula (f₁.imp f₂) = (g.onBoundedFormula f₁).imp (g.onBoundedFormula f₂)
- g.onBoundedFormula f.all = (g.onBoundedFormula f).all
Maps a sentence's symbols along a language map.
Equations
- g.onSentence = g.onFormula
Maps a bounded formula's symbols along a language equivalence.
Equations
- φ.onBoundedFormula = { toFun := φ.toLHom.onBoundedFormula, invFun := φ.invLHom.onBoundedFormula, left_inv := ⋯, right_inv := ⋯ }
The equality of two terms as a bounded formula.
Equations
- FirstOrder.«term_='_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_='_» 88 88 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =' ") (Lean.ParserDescr.cat `term 89))
The implication between two bounded formulas
Equations
- FirstOrder.«term_⟹_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_⟹_» 62 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ ") (Lean.ParserDescr.cat `term 62))
The universal quantifier over bounded formulas
Equations
- FirstOrder.«term∀'_» = Lean.ParserDescr.node `FirstOrder.«term∀'_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀'") (Lean.ParserDescr.cat `term 110))
The negation of a bounded formula is also a bounded formula.
Equations
- FirstOrder.«term∼_» = Lean.ParserDescr.node `FirstOrder.«term∼_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 1023))
The biimplication between two bounded formulas.
Equations
- FirstOrder.«term_⇔_» = Lean.ParserDescr.trailingNode `FirstOrder.«term_⇔_» 61 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ ") (Lean.ParserDescr.cat `term 62))
Puts an ∃
quantifier on a bounded formula.
Equations
- FirstOrder.«term∃'_» = Lean.ParserDescr.node `FirstOrder.«term∃'_» 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃'") (Lean.ParserDescr.cat `term 110))
Relabels a formula's variables along a particular function.
The graph of a function as a first-order formula.
Equations
- FirstOrder.Language.Formula.graph f = (FirstOrder.Language.var 0).equal (FirstOrder.Language.func f fun (i : Fin n) => FirstOrder.Language.var i.succ)
The negation of a formula.
Equations
The implication between formulas, as a formula.
iAlls f φ
transforms a L.Formula (α ⊕ β)
into a L.Formula β
by universally
quantifying over all variables Sum.inr _
.
Equations
- FirstOrder.Language.Formula.iAlls β φ = (FirstOrder.Language.BoundedFormula.relabel (fun (a : α ⊕ β) => Sum.map id (⇑(Classical.choice ⋯)) a) φ).alls
iExs f φ
transforms a L.Formula (α ⊕ β)
into a L.Formula β
by existentially
quantifying over all variables Sum.inr _
.
Equations
- FirstOrder.Language.Formula.iExs β φ = (FirstOrder.Language.BoundedFormula.relabel (fun (a : α ⊕ β) => Sum.map id (⇑(Classical.choice ⋯)) a) φ).exs
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.
The biimplication between formulas, as a formula.
Equations
A bijection sending formulas to sentences with constants.
The sentence indicating that a basic relation symbol is reflexive.
Equations
- r.reflexive = (r.boundedFormula₂ ((FirstOrder.Language.var ∘ Sum.inr) 0) ((FirstOrder.Language.var ∘ Sum.inr) 0)).all
The sentence indicating that a basic relation symbol is irreflexive.
Equations
- r.irreflexive = (r.boundedFormula₂ ((FirstOrder.Language.var ∘ Sum.inr) 0) ((FirstOrder.Language.var ∘ Sum.inr) 0)).not.all
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 a structure is infinite.
Equations
Instances For
A theory that indicates a structure is nonempty.
Equations
Instances For
A theory indicating that each of a set of constants is distinct.