### 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.

Original language | English |
---|---|

Pages (from-to) | 521-562 |

Number of pages | 42 |

Journal | Journal of Logic and Computation |

Volume | 18 |

Issue number | 4 |

DOIs | |

Publication status | Published - Aug 2008 |

### Keywords

- α-conversion
- First-order logic
- Meta-variables
- Nominal techniques
- Substitution

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

## Cite this

*Journal of Logic and Computation*,

*18*(4), 521-562. https://doi.org/10.1093/logcom/exm064