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]
- var: {L : FirstOrder.Language} → {α : Type u'} → α → FirstOrder.Language.Term L α
- func: {L : FirstOrder.Language} → {α : Type u'} → {l : ℕ} → FirstOrder.Language.Functions L l → (Fin l → FirstOrder.Language.Term L α) → FirstOrder.Language.Term L α
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
- FirstOrder.Language.Term.varFinset (FirstOrder.Language.var i) = {i}
- FirstOrder.Language.Term.varFinset (FirstOrder.Language.func _f ts) = Finset.biUnion Finset.univ fun i => FirstOrder.Language.Term.varFinset (ts i)
Instances For
The Finset
of variables from the left side of a sum used in a given term.
Equations
- FirstOrder.Language.Term.varFinsetLeft (FirstOrder.Language.var (Sum.inl i)) = {i}
- FirstOrder.Language.Term.varFinsetLeft (FirstOrder.Language.var (Sum.inr _i)) = ∅
- FirstOrder.Language.Term.varFinsetLeft (FirstOrder.Language.func _f ts) = Finset.biUnion Finset.univ fun i => FirstOrder.Language.Term.varFinsetLeft (ts i)
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} => FirstOrder.Language.Term.relabel g (ts i)
Instances For
Relabels a term's variables along a bijection.
Instances For
Restricts a term to use only a set of the given variables.
Equations
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.Term.restrictVar (FirstOrder.Language.var a) f = FirstOrder.Language.var (f { val := a, property := (_ : a ∈ {a}) })
Instances For
Restricts a term to use only a set of the given variables on the left side of a sum.
Equations
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.Term.restrictVarLeft (FirstOrder.Language.var (Sum.inl a)) f = FirstOrder.Language.var (Sum.inl (f { val := a, property := (_ : a ∈ {a}) }))
- FirstOrder.Language.Term.restrictVarLeft (FirstOrder.Language.var (Sum.inr a)) _f = FirstOrder.Language.var (Sum.inr a)
Instances For
The representation of a constant symbol as a term.
Instances For
Applies a unary function to a term.
Instances For
Applies a binary function to two terms.
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.Term.constantsToVars (FirstOrder.Language.var a) = FirstOrder.Language.var (Sum.inr a)
Instances For
Sends a term with extra variables to a term with constants.
Equations
- FirstOrder.Language.Term.varsToConstants (FirstOrder.Language.var (Sum.inr a)) = FirstOrder.Language.var a
- FirstOrder.Language.Term.varsToConstants (FirstOrder.Language.var (Sum.inl c)) = FirstOrder.Language.Constants.term (Sum.inr c)
- FirstOrder.Language.Term.varsToConstants (FirstOrder.Language.func f ts) = FirstOrder.Language.func (Sum.inl f) fun i => FirstOrder.Language.Term.varsToConstants (ts i)
Instances For
A bijection between terms with constants and terms with extra variables.
Instances For
A bijection between terms with constants and terms with extra variables.
Instances For
Raises all of the Fin
-indexed variables of a term greater than or equal to m
by n'
.
Instances For
Substitutes the variables in a given term with terms.
Equations
- FirstOrder.Language.Term.subst (FirstOrder.Language.var a) x = x a
- FirstOrder.Language.Term.subst (FirstOrder.Language.func f ts) x = FirstOrder.Language.func f fun i => FirstOrder.Language.Term.subst (ts i) x
Instances For
Maps a term's symbols along a language map.
Equations
Instances For
Maps a term's symbols along a language equivalence.
Instances For
- falsum: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → FirstOrder.Language.BoundedFormula L α n
- equal: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → FirstOrder.Language.Term L (α ⊕ Fin n) → FirstOrder.Language.Term L (α ⊕ Fin n) → FirstOrder.Language.BoundedFormula L α n
- rel: {L : FirstOrder.Language} → {α : Type u'} → {n l : ℕ} → FirstOrder.Language.Relations L l → (Fin l → FirstOrder.Language.Term L (α ⊕ Fin n)) → FirstOrder.Language.BoundedFormula L α n
- imp: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → FirstOrder.Language.BoundedFormula L α n → FirstOrder.Language.BoundedFormula L α n → FirstOrder.Language.BoundedFormula L α n
- all: {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → FirstOrder.Language.BoundedFormula L α (n + 1) → FirstOrder.Language.BoundedFormula L α n
BoundedFormula α n
is the type of formulas with free variables indexed by α
and up to n
additional free variables.
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.
Instances For
Applies a unary relation to a term as a bounded formula.
Instances For
Applies a binary relation to two terms as a bounded formula.
Instances For
The equality of two terms as a bounded formula.
Instances For
Applies a relation to terms as a bounded formula.
Instances For
Applies a unary relation to a term as a formula.
Instances For
Applies a binary relation to two terms as a formula.
Instances For
The equality of two terms as a first-order formula.
Instances For
The negation of a bounded formula is also a bounded formula.
Instances For
Puts an ∃
quantifier on a bounded formula.
Instances For
The biimplication between two bounded formulas.
Instances For
The Finset
of variables used in a given formula.
Equations
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.BoundedFormula.freeVarFinset FirstOrder.Language.BoundedFormula.falsum = ∅
- FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.Term.varFinsetLeft t₁ ∪ FirstOrder.Language.Term.varFinsetLeft t₂
- FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.BoundedFormula.rel _R ts) = Finset.biUnion Finset.univ fun i => FirstOrder.Language.Term.varFinsetLeft (ts i)
- FirstOrder.Language.BoundedFormula.freeVarFinset (FirstOrder.Language.BoundedFormula.all f) = FirstOrder.Language.BoundedFormula.freeVarFinset f
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 (FirstOrder.Language.BoundedFormula.all f) = FirstOrder.Language.BoundedFormula.all (FirstOrder.Language.BoundedFormula.castLE (_ : x + 1 ≤ x + 1) f)
Instances For
Restricts a bounded formula to only use a particular set of free variables.
Instances For
Places universal quantifiers on all extra variables of a bounded formula.
Equations
Instances For
Places existential quantifiers on all extra variables of a bounded formula.
Equations
Instances For
Maps bounded formulas along a map of terms and a map of relations.
Equations
- One or more equations did not get rendered due to their size.
- 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 => ft x (ts i)
Instances For
Raises all of the Fin
-indexed variables of a formula greater than or equal to m
by n'
.
Instances For
An equivalence of bounded formulas given by an equivalence of terms and an equivalence of relations.
Instances For
Relabels a bounded formula's variables along a particular function.
Instances For
Relabels a bounded formula's free variables along a bijection.
Instances For
Substitutes the variables in a given formula with terms.
Instances For
A bijection sending formulas with constants to formulas with extra variables.
Instances For
Turns the extra variables of a bounded formula into free variables.
Equations
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.BoundedFormula.toFormula FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
- FirstOrder.Language.BoundedFormula.toFormula (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.Term.equal t₁ t₂
- FirstOrder.Language.BoundedFormula.toFormula (FirstOrder.Language.BoundedFormula.rel _R ts) = FirstOrder.Language.Relations.formula _R ts
Instances For
take the disjunction of a finite set of formulas
Instances For
take the conjunction of a finite set of formulas
Instances For
- equal: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (t₁ t₂ : FirstOrder.Language.Term L (α ⊕ Fin n)), FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.Term.bdEqual t₁ t₂)
- rel: ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} (R : FirstOrder.Language.Relations L l) (ts : Fin l → FirstOrder.Language.Term L (α ⊕ Fin n)), FirstOrder.Language.BoundedFormula.IsAtomic (FirstOrder.Language.Relations.boundedFormula R ts)
An atomic formula is either equality or a relation symbol applied to terms.
Note that ⊥
and ⊤
are not considered atomic in this convention.
Instances For
- falsum: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ}, FirstOrder.Language.BoundedFormula.IsQF FirstOrder.Language.BoundedFormula.falsum
- of_isAtomic: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n}, FirstOrder.Language.BoundedFormula.IsAtomic φ → FirstOrder.Language.BoundedFormula.IsQF φ
- imp: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ₁ φ₂ : FirstOrder.Language.BoundedFormula L α n}, FirstOrder.Language.BoundedFormula.IsQF φ₁ → FirstOrder.Language.BoundedFormula.IsQF φ₂ → FirstOrder.Language.BoundedFormula.IsQF (FirstOrder.Language.BoundedFormula.imp φ₁ φ₂)
A quantifier-free formula is a formula defined without quantifiers. These are all equivalent to boolean combinations of atomic formulas.
Instances For
- of_isQF: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α n}, FirstOrder.Language.BoundedFormula.IsQF φ → FirstOrder.Language.BoundedFormula.IsPrenex φ
- all: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α (n + 1)}, FirstOrder.Language.BoundedFormula.IsPrenex φ → FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.all φ)
- ex: ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : FirstOrder.Language.BoundedFormula L α (n + 1)}, FirstOrder.Language.BoundedFormula.IsPrenex φ → FirstOrder.Language.BoundedFormula.IsPrenex (FirstOrder.Language.BoundedFormula.ex φ)
Indicates that a bounded formula is in prenex normal form - that is, it consists of quantifiers applied to a quantifier-free formula.
Instances For
An auxiliary operation to FirstOrder.Language.BoundedFormula.toPrenex
.
If φ
is quantifier-free and ψ
is in prenex normal form, then φ.toPrenexImpRight ψ
is a prenex normal form for φ.imp ψ
.
Instances For
An auxiliary operation to FirstOrder.Language.BoundedFormula.toPrenex
.
If φ
and ψ
are in prenex normal form, then φ.toPrenexImp ψ
is a prenex normal form for φ.imp ψ
.
Instances For
For any bounded formula φ
, φ.toPrenex
is a semantically-equivalent formula in prenex normal
form.
Equations
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.BoundedFormula.toPrenex FirstOrder.Language.BoundedFormula.falsum = ⊥
- FirstOrder.Language.BoundedFormula.toPrenex (FirstOrder.Language.BoundedFormula.equal t₁ t₂) = FirstOrder.Language.Term.bdEqual t₁ t₂
- FirstOrder.Language.BoundedFormula.toPrenex (FirstOrder.Language.BoundedFormula.rel _R ts) = FirstOrder.Language.BoundedFormula.rel _R ts
- FirstOrder.Language.BoundedFormula.toPrenex (FirstOrder.Language.BoundedFormula.all f) = FirstOrder.Language.BoundedFormula.all (FirstOrder.Language.BoundedFormula.toPrenex f)
Instances For
Maps a bounded formula's symbols along a language map.
Equations
- One or more equations did not get rendered due to their size.
- FirstOrder.Language.LHom.onBoundedFormula g FirstOrder.Language.BoundedFormula.falsum = FirstOrder.Language.BoundedFormula.falsum
- FirstOrder.Language.LHom.onBoundedFormula g (FirstOrder.Language.BoundedFormula.all f) = FirstOrder.Language.BoundedFormula.all (FirstOrder.Language.LHom.onBoundedFormula g f)
Instances For
Maps a formula's symbols along a language map.
Instances For
Maps a sentence's symbols along a language map.
Instances For
Maps a theory's symbols along a language map.
Instances For
Maps a bounded formula's symbols along a language equivalence.
Instances For
Maps a formula's symbols along a language equivalence.
Instances For
Maps a sentence's symbols along a language equivalence.
Instances For
Relabels a formula's variables along a particular function.
Instances For
The graph of a function as a first-order formula.
Instances For
The negation of a formula.
Instances For
The implication between formulas, as a formula.
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 _
.
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 _
.
Instances For
The biimplication between formulas, as a formula.
Instances For
A bijection sending formulas to sentences with constants.
Instances For
The sentence indicating that a basic relation symbol is reflexive.
Instances For
The sentence indicating that a basic relation symbol is irreflexive.
Instances For
The sentence indicating that a basic relation symbol is symmetric.
Instances For
The sentence indicating that a basic relation symbol is antisymmetric.
Instances For
The sentence indicating that a basic relation symbol is transitive.
Instances For
The sentence indicating that a basic relation symbol is total.
Instances For
A sentence indicating that a structure has n
distinct elements.
Instances For
A theory indicating that a structure is infinite.
Instances For
A theory that indicates a structure is nonempty.
Instances For
A theory indicating that each of a set of constants is distinct.