| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 4663322 | Journal of Applied Logic | 2007 | 32 Pages |
Abstract
In this paper we introduce Fresh Logic, a natural deduction style first-order logic extended with term-formers and quantifiers derived from the FM-sets 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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Murdoch J. Gabbay,