Abstract
In informal mathematical usage we often reason about languages involving binding
of objectvariables. We find ourselves writing assertions involving metavariables
and captureavoidance constraints on where objectvariables can and cannot occur
free. Formalising such assertions is problematic because the standard logical
frameworks cannot express captureavoidance constraints directly.
In this thesis we make the case for extending logical frameworks with metavariables
and captureavoidance constraints. We use nominal techniques that allow
for a direct formalisation of metalevel 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 metalevel reasoning:
• instantiation of metavariables, by means of capturing substitution of terms
for metavariables;
• ??renaming of objectvariables and captureavoiding substitution of terms
for objectvariables in the presence of metavariables;
• generation of fresh objectvariables inside a derivation.
We apply our nominal techniques to the following two logical frameworks:
• Equational logic. We investigate prooftheoretical properties, give a semantics
in nominal sets and compare the notion of ??renaming to existing notions
of ??equivalence with metavariables. We also provide an axiomatisation of
captureavoiding substitution, and show that it is sound and complete with
respect to the usual notion of captureavoiding substitution.
• Firstorder logic with equality. We provide a sequent calculus with metavariables
and captureavoidance constraints, and show that it represents
schemas of derivations in firstorder 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  9789038611389 
DOIs  
Publication status  Published  2007 
Fingerprint Dive into the research topics of 'Logical calculi for reasoning with binding'. Together they form a unique fingerprint.
Cite this
Mathijssen, A. H. J. (2007). Logical calculi for reasoning with binding. Technische Universiteit Eindhoven. https://doi.org/10.6100/IR630460