A sequent calculus for nominal logic

Abstract

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 FO/spl lambda//spl nabla/, another logic with a self-dual quantifier, within FL.