A Term Assignment for Polarized Bi-intuitionistic Logic and its Strong Normalization

Issue title: Logic for Pragmatics

Article type: Research Article

Authors: Biasi, Corrado | Aschieri, Federico

Affiliations: Department of Computer Science, Queen Mary University of London, London E1 4NS, Great Britain. E-mail: biasiman@dcs.qmul.ac.uk | Dipartimento di Informatica, SS.MM.FF.NN. Verona, Italy

Note: [] Address for correspondence: Department of Computer Science, Queen Mary University of London, London E1 4NS, Great Britain

Abstract: We propose a term assignment (let calculus) for Intuitionistic Logic for Pragmatics ILP_{AC}, a polarized sequent calculus which includes ordinary positive intuitionistic logic LJ^{⊃∩}, its dual LJ^{∖γ} and dual negations ( )^{⊥} which allow a formula to "communicate" with its dual fragment. We prove the strong normalization property for the term assignment which follows by soundly translating the let calculus into simply typed γ calculus with pairings and projections. A new and simple proof of strong normalization for the latter is also provided.

Keywords: subtractive logic, bi-intuitionistic logic, intuitionistic logic for pragmatics, lambda calculus, strong normalization

Journal: Fundamenta Informaticae, vol. 84, no. 2, pp. 185-205, 2008