Logical calculi for reasoning with binding

A.H.J. Mathijssen

Research output: ThesisPhd Thesis 1 (Research TU/e / Graduation TU/e)

97 Downloads (Pure)

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 languageEnglish
QualificationDoctor of Philosophy
Awarding Institution
  • Department of Mathematics and Computer Science
Supervisors/Advisors
  • Groote, Jan Friso, Promotor
  • Gabbay, Jamie, Copromotor
Award date15 Nov 2007
Place of PublicationEindhoven
Publisher
Print ISBNs978-90-386-1138-9
DOIs
Publication statusPublished - 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