Permissive-Nominal Logic (journal version)

Abstract

Permissive-Nominal Logic (PNL) is an extension of first-order predicate logic in which term-formers can bind names in their arguments. This allows for direct axiomatisations with binders, such as of the lambda-binder of the lambda-calculus or the forall-binder of first-order logic. It also allows us to finitely axiomatise arithmetic, and similarly to axiomatise 'nominal' datatypes-with-binding. Just like first- and higher-order logic, equality reasoning is not necessary to alpha-rename. This gives PNL much of the expressive power of higher-order logic, but models and derivations of PNL are first-order in character, and the logic seems to strike a good balance between expressivity and simplicity.

References in corpus (3)

• LISA -- A Modern Proof System
• Isabelle: The Next 700 Theorem Provers
• Permissive nominal terms and their unification: an infinite, co-infinite approach to nominal techniques

Cited by in corpus (5)

• Nominal Coalgebraic Data Types with Applications to Lambda Calculus
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
• Finite and infinite support in nominal algebra and logic: nominal completeness theorems for free
• Semantics out of context: nominal absolute denotations for first-order logic and computation