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

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.