Syntax of first-order logic #

This file defines the syntax of first-order logic.

Definitions #

Language defines first-order languages.
L.Term n and L.Formula n are terms and formulas for a first-order language L, with variables as well-scoped de Bruijn indexes in Fin n.
L.Subst n m, defined as Fin n → L.Term m, is the parallel de Bruijn substitutions that substitutes n variables into terms in L.Term m.
Term.subst and Formula.subst are substitutions of terms and formulas.
Operations over L.Subst, including identical substitution idₛ, composition ∘ₛ, variable shifting Subst.shift, substitution lifting ⇑ₛ (the "up" operation in Autosubst paper), single variable substitution ↦ₛ, etc.

Equational theory #

We formalize the equational theory of de Bruijn substitutions, extending the Autosubst paper with well-scoped syntax and a much richer set of operations.

We tag the rewriting rules in Autosubst paper with the simp set syntax_simp. Tactic syntax_simp uses these rules to rewrite FOL syntaxes to their normal forms, e.g.

example {L : Language} {n m : ℕ} {t : L.Term (n + 1)} {t' : L.Term n} {σ : L.Subst n m} :
    t[↦ₛ t']ₜ[σ]ₜ = t[⇑ₛσ]ₜ[↦ₛ t'[σ]ₜ]ₜ := by
  syntax_simp

This is not a complete decision procedure like the Autosubst paper does, though it already solves a lot of equalities.

Design note #

Syntax representations. Our definition is a nameless representation with de Bruijn index, in favor of its simplicity with well-defined capture-avoiding substitution. We don't want our syntactic definition rely on meta-level constructions (e.g. HOAS). In comparison, Mathlib's model theory folder uses a locally nameless representation.
Well-scoped syntax. We start from a non-well-scoped design, where L.Formula takes any index in ℕ as its variable. Switching to well-scoped design gives some advantages:
1. it makes definitions simpler in many cases, e.g. Language.Order requires two Formula 2s for less-equal ⪯ and less-than ≺. In non-well-scoped design, one would require a formula with a proof that only 0 and 1 are used.
2. it's easier to prove computability results, since substitutions as ℕ → L.Term are not encodable, but Fin n → L.Term m are.
3. The proof system can admit empty structure (see Proof.lean for more details).
Equality. Equality can be defined as a primitive notion (which is what we are doing) or an optional binary relation. The advantage to define it as a primitive notion is that we can enforce equalities to be interpreted as true equality, and we can ship prw tactic on equalities along with iffs.

References #

Autosubst: Reasoning with de Bruijn Terms and Parallel Substitution. Steven Schäfer, Tobias Tebbi, Gert Smolka. https://www.ps.uni-saarland.de/Publications/documents/SchaeferEtAl_2015_Autosubst_-Reasoning.pdf
Completeness and Decidability of de Bruijn Substitution Algebra in Coq. Steven Schäfer, Gert Smolka, Tobias Tebbi. https://www.ps.uni-saarland.de/Publications/documents/SchaeferEtAl_2015_Completeness.pdf
1001 Representations of Syntax with Binding. Jesper Cockx. https://jesper.sikanda.be/posts/1001-syntax-representations.html