A Simpler Proof Theory for Nominal Logic

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Nominal logic is a variant of first-order logic equipped with a “fresh-name quantifier” И and other features useful for reasoning about languages with bound names. Its original presentation was as a Hilbert axiomatic theory, but several attempts have been made to provide more convenient Gentzen-style sequent or natural deduction calculi for nominal logic. Unfortunately, the rules for И in these calculi involve complicated side-conditions, so using and proving properties of these calculi is difficult. This paper presents an improved sequent calculus NL ⇒ for nominal logic. Basic results such as cut-elimination and conservativity with respect to nominal logic are proved. Also, NL ⇒ is used to solve an open problem, namely relating nominal logic’s И-quantifier and the self-dual ∇-quantifier of Miller and Tiu’s FOλ∇
Original languageEnglish
Title of host publicationFoundations of Software Science and Computational Structures
Subtitle of host publication8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings
EditorsVladimiro Sassone
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-31982-5
ISBN (Print)978-3-540-25388-4
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'A Simpler Proof Theory for Nominal Logic'. Together they form a unique fingerprint.

Cite this