Abstract
In informal mathematical usage we often reason about languages involving binding
of object-variables. We find ourselves writing assertions involving meta-variables
and capture-avoidance constraints on where object-variables can and cannot occur
free. Formalising such assertions is problematic because the standard logical
frameworks cannot express capture-avoidance constraints directly.
In this thesis we make the case for extending logical frameworks with metavariables
and capture-avoidance constraints. We use nominal techniques that allow
for a direct formalisation of meta-level assertions, while remaining close to informal
practice. Our focus is on derivability and we show that our derivation rules support
the following key features of meta-level reasoning:
• instantiation of meta-variables, by means of capturing substitution of terms
for meta-variables;
• ??-renaming of object-variables and capture-avoiding substitution of terms
for object-variables in the presence of meta-variables;
• generation of fresh object-variables inside a derivation.
We apply our nominal techniques to the following two logical frameworks:
• Equational logic. We investigate proof-theoretical properties, give a semantics
in nominal sets and compare the notion of ??-renaming to existing notions
of ??-equivalence with meta-variables. We also provide an axiomatisation of
capture-avoiding substitution, and show that it is sound and complete with
respect to the usual notion of capture-avoiding substitution.
• First-order logic with equality. We provide a sequent calculus with metavariables
and capture-avoidance constraints, and show that it represents
schemas of derivations in first-order logic. We also show how we can axiomatise
this notion of derivability in the calculus for equational logic.
Original language | English |
---|---|
Qualification | Doctor of Philosophy |
Awarding Institution |
|
Supervisors/Advisors |
|
Award date | 15 Nov 2007 |
Place of Publication | Eindhoven |
Publisher | |
Print ISBNs | 978-90-386-1138-9 |
DOIs | |
Publication status | Published - 2007 |