Logical calculi for reasoning with binding

A.H.J. Mathijssen

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

    120 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
    • 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