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] [HvD20]
- J. Han, F. van Doorn, A formalization of forcing and the unprovability of the continuum hypothesis
A term on α
is either a variable indexed by an element of α
or a function symbol applied to simpler terms.
- var: {L : FirstOrder.Language} → {α : Type u'} → α → L.Term α
- func: {L : FirstOrder.Language} → {α : Type u'} → {l : ℕ} → L.Functions l → (Fin l → L.Term α) → L.Term α
Instances For
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
Instances For
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
Instances For
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)
Instances For
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 := ⋯ }
Instances For
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 ⋯)
Instances For
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 ⋯)
Instances For
The representation of a constant symbol as a term.
Equations
- c.term = FirstOrder.Language.func c default
Instances For
Applies a unary function to a term.
Equations
- f.apply₁ t = FirstOrder.Language.func f ![t]
Instances For
Applies a binary function to two terms.
Equations
- f.apply₂ t₁ t₂ = FirstOrder.Language.func f ![t₁, t₂]
Instances For
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)
Instances For
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
Instances For
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 := ⋯ }
Instances For
A bijection between terms with constants and terms with extra variables.
Equations
- FirstOrder.Language.Term.constantsVarsEquivLeft = FirstOrder.Language.Term.constantsVarsEquiv.trans (FirstOrder.Language.Term.relabelEquiv (Equiv.sumAssoc γ α β)).symm
Instances For
Equations
- FirstOrder.Language.Term.inhabitedOfVar = { default := FirstOrder.Language.var default }
Equations
- FirstOrder.Language.Term.inhabitedOfConstant = { default := default.term }
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')
Instances For
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
Instances For
Equations
- FirstOrder.«term&_» = Lean.ParserDescr.node `FirstOrder.term&_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 1023))
Instances For
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)
Instances For
Maps a term's symbols along a language equivalence.
Equations
- FirstOrder.Language.Lequiv.onTerm φ = { toFun := φ.toLHom.onTerm, invFun := φ.invLHom.onTerm, left_inv := ⋯, right_inv := ⋯ }
Instances For
BoundedFormula α n
is the type of formulas with free variables indexed by α
and up to n
additional free variables.
- falsum: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n
- equal: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.Term (α ⊕ Fin n) → L.Term (α ⊕ Fin n) → L.BoundedFormula α n
- rel: {L : FirstOrder.Language} → {α : Type u'} → {n l : ℕ} → L.Relations l → (Fin l → L.Term (α ⊕ Fin n)) → L.BoundedFormula α n
- imp: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → L.BoundedFormula α n → L.BoundedFormula α n
- all: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α (n + 1) → L.BoundedFormula α n
Instances For
A sentence is a formula with no free variables.
Instances For
A theory is a set of sentences.
Instances For
Applies a relation to terms as a bounded formula.
Equations
- R.boundedFormula ts = FirstOrder.Language.BoundedFormula.rel R ts
Instances For
Applies a unary relation to a term as a bounded formula.
Equations
- r.boundedFormula₁ t = r.boundedFormula ![t]
Instances For
Applies a binary relation to two terms as a bounded formula.
Equations
- r.boundedFormula₂ t₁ t₂ = r.boundedFormula ![t₁, t₂]
Instances For
The equality of two terms as a bounded formula.
Equations
- t₁.bdEqual t₂ = FirstOrder.Language.BoundedFormula.equal t₁ t₂
Instances For
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)
Instances For
Applies a unary relation to a term as a formula.
Equations
- r.formula₁ t = r.formula ![t]
Instances For
Applies a binary relation to two terms as a formula.
Equations
- r.formula₂ t₁ t₂ = r.formula ![t₁, t₂]
Instances For
The equality of two terms as a first-order formula.
Equations
- t₁.equal t₂ = (FirstOrder.Language.Term.relabel Sum.inl t₁).bdEqual (FirstOrder.Language.Term.relabel Sum.inl t₂)
Instances For
Equations
- FirstOrder.Language.BoundedFormula.instInhabited = { default := FirstOrder.Language.BoundedFormula.falsum }
Equations
- FirstOrder.Language.BoundedFormula.instBot = { bot := FirstOrder.Language.BoundedFormula.falsum }
The negation of a bounded formula is also a bounded formula.
Instances For
Puts an ∃
quantifier on a bounded formula.
Equations
- φ.ex = φ.not.all.not
Instances For
Equations
- FirstOrder.Language.BoundedFormula.instInf = { inf := fun (f g : L.BoundedFormula α n) => (f.imp g.not).not }
Equations
- FirstOrder.Language.BoundedFormula.instSup = { sup := fun (f g : L.BoundedFormula α n) => f.not.imp g }
The biimplication between two bounded formulas.
Instances For
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
Instances For
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
Instances For
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
Instances For
Places universal quantifiers on all extra variables of a bounded formula.
Instances For
Places existential quantifiers on all extra variables of a bounded formula.
Instances For
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
Instances For
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.
Instances For
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.
Instances For
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
Instances For
Relabels a bounded formula's variables along a particular function.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Relabels a bounded formula's free variables along a bijection.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Substitutes the variables in a given formula with terms.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A bijection sending formulas with constants to formulas with extra variables.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
take the disjunction of a finite set of formulas
Equations
- FirstOrder.Language.BoundedFormula.iSup s f = List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊔ x2) ⊥ (List.map f s.toList)
Instances For
take the conjunction of a finite set of formulas
Equations
- FirstOrder.Language.BoundedFormula.iInf s f = List.foldr (fun (x1 x2 : L.BoundedFormula α n) => x1 ⊓ x2) ⊤ (List.map f s.toList)
Instances For
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
Instances For
Maps a formula's symbols along a language map.
Equations
- g.onFormula = g.onBoundedFormula
Instances For
Maps a sentence's symbols along a language map.
Equations
- g.onSentence = g.onFormula
Instances For
Maps a theory's symbols along a language map.
Instances For
Maps a bounded formula's symbols along a language equivalence.
Equations
- φ.onBoundedFormula = { toFun := φ.toLHom.onBoundedFormula, invFun := φ.invLHom.onBoundedFormula, left_inv := ⋯, right_inv := ⋯ }
Instances For
Maps a formula's symbols along a language equivalence.
Equations
- φ.onFormula = φ.onBoundedFormula
Instances For
Maps a sentence's symbols along a language equivalence.
Equations
- φ.onSentence = φ.onFormula
Instances For
Equations
- FirstOrder.«term_='_» = Lean.ParserDescr.trailingNode `FirstOrder.term_='_ 88 88 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =' ") (Lean.ParserDescr.cat `term 89))
Instances For
Equations
- FirstOrder.«term_⟹_» = Lean.ParserDescr.trailingNode `FirstOrder.term_⟹_ 62 63 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ ") (Lean.ParserDescr.cat `term 62))
Instances For
Equations
- FirstOrder.«term∀'_» = Lean.ParserDescr.node `FirstOrder.term∀'_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀'") (Lean.ParserDescr.cat `term 110))
Instances For
Equations
- FirstOrder.«term∼_» = Lean.ParserDescr.node `FirstOrder.term∼_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 1023))
Instances For
Equations
- FirstOrder.«term_⇔_» = Lean.ParserDescr.trailingNode `FirstOrder.term_⇔_ 61 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ ") (Lean.ParserDescr.cat `term 62))
Instances For
Equations
- FirstOrder.«term∃'_» = Lean.ParserDescr.node `FirstOrder.term∃'_ 110 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃'") (Lean.ParserDescr.cat `term 110))
Instances For
Relabels a formula's variables along a particular function.
Equations
Instances For
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)
Instances For
The negation of a formula.
Equations
Instances For
The implication between formulas, as a formula.
Equations
- FirstOrder.Language.Formula.imp = FirstOrder.Language.BoundedFormula.imp
Instances For
Given a map f : α → β ⊕ γ
, iAlls f φ
transforms a L.Formula α
into a L.Formula β
by renaming variables with the map f
and then universally
quantifying over all variables Sum.inr _
.
Equations
- FirstOrder.Language.Formula.iAlls f φ = (FirstOrder.Language.BoundedFormula.relabel (fun (a : α) => Sum.map id (⇑(Classical.choice ⋯)) (f a)) φ).alls
Instances For
Given a map f : α → β ⊕ γ
, iExs f φ
transforms a L.Formula α
into a L.Formula β
by renaming variables with the map f
and then universally
quantifying over all variables Sum.inr _
.
Equations
- FirstOrder.Language.Formula.iExs f φ = (FirstOrder.Language.BoundedFormula.relabel (fun (a : α) => Sum.map id (⇑(Classical.choice ⋯)) (f a)) φ).exs
Instances For
The biimplication between formulas, as a formula.
Equations
- φ.iff ψ = FirstOrder.Language.BoundedFormula.iff φ ψ
Instances For
A bijection sending formulas to sentences with constants.
Equations
- FirstOrder.Language.Formula.equivSentence = (FirstOrder.Language.BoundedFormula.constantsVarsEquiv.trans (FirstOrder.Language.BoundedFormula.relabelEquiv (Equiv.sumEmpty α Empty))).symm
Instances For
The sentence indicating that a basic relation symbol is reflexive.
Equations
Instances For
The sentence indicating that a basic relation symbol is irreflexive.
Equations
Instances For
The sentence indicating that a basic relation symbol is symmetric.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sentence indicating that a basic relation symbol is antisymmetric.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sentence indicating that a basic relation symbol is transitive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The sentence indicating that a basic relation symbol is total.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A sentence indicating that a structure has n
distinct elements.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A theory indicating that a structure is infinite.
Equations
- L.infiniteTheory = Set.range (FirstOrder.Language.Sentence.cardGe L)
Instances For
A theory that indicates a structure is nonempty.
Equations
- L.nonemptyTheory = {FirstOrder.Language.Sentence.cardGe L 1}
Instances For
A theory indicating that each of a set of constants is distinct.