An Anti-Locally-Nameless Approach to Formalizing Quantifiers

Olivier Laurent (1, 2)

1 LIP - Laboratoire de l'Informatique du Parallélisme
2 PLUME - Preuves et Langages

We investigate the possibility of formalizing quantifiers in proof theory while avoiding, as far as possible, the use of true binding structures, α-equivalence or variable renamings. We propose a solution with two kinds of variables in terms and formulas, as originally done by Gentzen. In this way formulas are first-order structures, and we are able to avoid capture problems in substitutions. However at the level of proofs and proof manipulations, some binding structure seems unavoidable. We give a representation with de Bruijn indices for proof rules which does not impact the formula representation and keeps the whole set of definitions firstorder.

Mots clés: quantifiers; proof assistant; formalization; proof theory; first-order logic; normalization

Domaines: Logique en informatique [cs.LO]; Logique [math.LO]

Olivier Laurent. An Anti-Locally-Nameless Approach to Formalizing Quantifiers. Certified Programs and Proofs, Jan 2021, virtual, Denmark. pp.300-312, ⟨10.1145/3437992.3439926⟩. ⟨hal-03096253⟩