Fresh Logic: proof-theory and semantics for FM and nominal techniques

In this paper we introduce Fresh Logic, a natural deduction style first-order logic extended with term-formers and quantifiers derived from the model of names and binding in abstract syntax. Fresh Logic can be classical or intuitionistic depending on whether we include a law of excluded middle; we present a proof-normalisation procedure for the intuitionistic case and a semantics based on Kripke models in FM-sets for which it is sound and complete. Contents

• Type: Journal
• Year: 2007
• Where: JAPLL
• Authors: Murdoch Gabbay
• Keywords: Fresh Logic, JAPLL 2007, Natural Deduction Style, first-order Logic