A simple sequent calculus for nominal logic

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Nominal logic is a variant of first-order logic that provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over fresh names (names not appearing in any values considered so far). Previous attempts have been made to develop convenient rules for reasoning with the new-quantifier, but we argue that none of these attempts is completely satisfactory. In this article we develop a new sequent calculus for nominal logic in which the rules for the new-quantifier are much simpler than in previous attempts. We also prove several structural and metatheoretic properties, including cut-elimination, consistency and equivalence to Pitts' axiomatization of nominal logic.
Original languageEnglish
Pages (from-to)699-726
Number of pages28
JournalJournal of Logic and Computation
Issue number4
Early online date19 May 2014
Publication statusPublished - Aug 2016


Dive into the research topics of 'A simple sequent calculus for nominal logic'. Together they form a unique fingerprint.

Cite this