Sciweavers

Share
LOGCOM
2008

One-and-a-halfth-order Logic

9 years 7 months ago
One-and-a-halfth-order Logic
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 metavariables. 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.
Murdoch James Gabbay, Aad Mathijssen
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where LOGCOM
Authors Murdoch James Gabbay, Aad Mathijssen
Comments (0)
books