One-and-a-halfth-order logic

M.J. Gabbay, A.H.J. Mathijssen

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    16 Citaten (Scopus)


    The practice of first-order logic is replete with meta-level concepts. Most notably there are the meta-variables themselves (ranging over predicates, variables, and terms), assumptions about freshness of variables with respect to these meta-variables, alpha-equivalence and capture-avoiding substitution. We present one-and-a-halfth-order logic, in which these concepts are made explicit. We exhibit both algebraic and sequent specifications of one-and-a-halfth-order logic derivability, show them equivalent, show that the derivations satisfy cut-elimination, and prove correctness of an interpretation of first-order logic within itWe discuss the technicalities in a wider context as a case-study for nominal algebra, as a logic in its own right, as an algebraisation of logic, as an example of how other systems might be treated, and also as a theoretical foundation for future implementation.
    Originele taal-2Engels
    TitelProceedings 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'06, Venice, Italy, July 10-12, 2006)
    Plaats van productieNew York
    UitgeverijAssociation for Computing Machinery, Inc
    ISBN van geprinte versie1-59593-388-3
    StatusGepubliceerd - 2006


    Duik in de onderzoeksthema's van 'One-and-a-halfth-order logic'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit