One-and-a-halfth-order logic

Murdoch Gabbay, Aad Mathijssen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Citations (Scopus)

Abstract

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 it. We 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. Copyright © 2006 ACM.

Original languageEnglish
Title of host publicationPPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
Pages189-200
Number of pages12
Volume2006
Publication statusPublished - 2006
EventPPDP'06 - 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming - Venice, Italy
Duration: 10 Jul 200612 Jul 2006

Conference

ConferencePPDP'06 - 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
CountryItaly
CityVenice
Period10/07/0612/07/06

Keywords

  • α-conversion
  • First-order logic
  • Fraenkel-Mostowski techniques
  • Higher-order logic
  • Meta-variables
  • Nominal terms

Fingerprint Dive into the research topics of 'One-and-a-halfth-order logic'. Together they form a unique fingerprint.

  • Cite this

    Gabbay, M., & Mathijssen, A. (2006). One-and-a-halfth-order logic. In PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (Vol. 2006, pp. 189-200)