Permissive-nominal logic

Permissive-Nominal Logic (PNL) is an extension of firstorder logic where term-formers can bind names in their arguments. This allows for direct axiomatisations with binders, such as the ∀-quantifier of first-order logic itself and the λ-binder of the lambda-calculus. This also allows us to finitely axiomatise arithmetic. Like first- and higher-order logic and unlike other nominal logics, equality reasoning is not necessary to α-rename. All this gives PNL much of the expressive power of higher-order logic, but terms, derivations and models of PNL are first-order in character, and the logic seems to strike a good balance between expressivity and simplicity. Categories and Subject Descriptors F.4.1 [Mathematical Logic]: Proof theory—Nominal techniques General Terms Theory Keywords First-order logic, permissive-nominal terms, mechanized mathematics.

• Type: Journal
• Year: 2010
• Where: PPDP
• Authors: Gilles Dowek, Murdoch James Gabbay
• Keywords: Keywords First-order Logic, Logic, PPDP 2010, Programming Languages, firstorder Logic