Permissive-nominal logic

11 years 8 months ago
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.
Gilles Dowek, Murdoch James Gabbay
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where PPDP
Authors Gilles Dowek, Murdoch James Gabbay
Comments (0)