A sequent calculus for nominal logic
Murdoch J. Gabbay, James Cheney · 2004
Nominal logic is a theory of names and binding based on the primitive concepts of freshness and swapping, with a self-dual N - (or "new")-quantifier, originally presented as a Hilbert-style axiom system extending first-order logic. We present a sequent calculus for nominal logic called Fresh Logic, or FL, admitting cut-elimination. We use FL to provide a proof-theoretic foundation for nominal logic programming and show how to interpret $FOL^{\\Delta abla}$, another logic with a self-dual quantifier, within FL.