Journal of Logic and Computation Advance Access originally published online on November 22, 2007
Journal of Logic and Computation 2008 18(4):521-562; doi:10.1093/logcom/exm064
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
One-and-a-halfth-order Logic
Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh EH14 4AS, UK. E-mail: murdoch.gabbay{at}gmail.com
Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB Eindhoven, The Netherlands.
E-mail: aad.mathijssen{at}gmail.com
 |
Abstract |
|---|
The practice of first-order logic is replete with meta-level concepts. Most notably there are meta-variables ranging over formulae, variables, and terms, and properties of syntax such as alpha-equivalence, capture-avoiding substitution and assumptions about freshness of variables with respect to meta-variables. We present one-and-a-halfth-order logic, in which these concepts are made explicit. We exhibit both sequent and algebraic 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.
Keywords: first-order logic; nominal techniques; substitution; 
-conversion; meta-variables
CiteULike 
Connotea 
Del.icio.us What's this?
This article has been cited by other articles:
|
|
 |
|
  M. J. Gabbay and A. Mathijssen A Nominal Axiomatization of the Lambda Calculus J Logic Computation, September 13, 2009; (2009) exp049v1. [Abstract] [PDF]
|
|
|
|
|
|
M. J. Gabbay and A. Mathijssen Nominal (Universal) Algebra: Equational Logic with Names and Binding J Logic Computation, July 5, 2009; (2009) exp033v1. [Abstract] [PDF]
|
|