## 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 language | English |
---|---|

Title of host publication | PPDP'06 - Proceedings of the Eight ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming |

Pages | 189-200 |

Number of pages | 12 |

Volume | 2006 |

Publication status | Published - 2006 |

Event | PPDP'06 - 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming - Venice, Italy Duration: 10 Jul 2006 → 12 Jul 2006 |

### Conference

Conference | PPDP'06 - 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming |
---|---|

Country | Italy |

City | Venice |

Period | 10/07/06 → 12/07/06 |

## Keywords

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