Formalizing Logical Metatheory:
Semantical Cut-Elimination
using Kripke Models for first-order Predicate Logic
Hugo Herbelin and Gyesik Lee
We propose a new approach to dealing with binding issues when
formalizing the metatheory of a logical system with variables such as
first-order predicate logic. In our approach, the syntax is
represented with locally traced names.
The style is similar
to Pollack-McKinna's locally-named approach, in which two sorts of
named variables are used. The main difference is that (locally bound)
variables occurring in an expression are controlled by the type of
that expression.
This approach has been adopted to formalize in Coq a
Kripke-based semantical cut-elimination of intuitionistic first-order
predicate logic.
The five main features of our paper are as follows:
- First, we show that the roles of constants and free variables
can be merged in studying the metatheory of a logical system.
- Second, there is no need for an extra syntax for well-formed
terms and formulae.
- Third, we emphasize the role of simultaneous substitution and
renaming.
- Fourth, the so-called Exists-Fresh quantification style, the
traditional method used to address the binding problems, is
revisited.
- Fifth, the cut-elimination is based on normalization by
evaluation (NBE).
During the formalization work, we attempted to employ common
statements for logicians, and we have also retained the simplicity of
the programming part.
- Formalizing Logical Metatheory: Semantical Cut-Elimination
using Kripke Models for first-order Predicate Logic.
Hugo Herbelin and Gyesik Lee. Submitted.
[Draft]
The proof scripts along with required libraries can be downloaded
as a gzip'd tarball [Kripke.tgz].
Extracting the files creates a directory called Kripke consisting
of two subdirectories with_parameters
and without_parameters.
- The directory with_parameters:
- It contains formalization in usual style.
- That is, there are two kinds of variable
names, (localy bound) variables and parameters.
- The directory without_parameters:
- It contains formalization
where no parameters (the so-called free variables) are
allowed.
- Parameters are merged with constants.
- That is, Constants play the role of parameters.
- The above paper is based on this version.
Both directories contain a Makefile such that you can compile
and generate all the documents by using make.
The proof scripts can be compiled on Coq8.3.pl3 and Coq8.3.pl4. It
should also work with Coq8.2pl3.
- Catarina Coquand.
A formalised proof of the soundness and completeness
of a simply typed lambda-calculus with explicit
substitutions.
Higher-Order and Symbolic Computation 15(1), 57-90, 2002.
- Hugo Herbelin and Gyesik Lee.
Forcing-based cut-elimination for Gentzen-style intuitionistic
sequent calculus.
Logic, Language, Information and Computation, 16th International
Workshop, Wollic 2009,
LNAI 5514: 209-217.
- James McKinna and Randy Pollack.
Some lambda calculus and type theory formalized.
Journal of Automated Reasoning 23(3-4), 373-409 (1999)