Formulae-as-Types for an Involutive Negation

ABSTRACT. We are interested in the constructive interpretation of reasoning by contrapositive in classical logic, or, in other words, of an involutive negation.

We first review the impossibility of an involutive negation in the call-by-name lambda-C calculus: we conclude that it is a defect of the evaluation strategy, which makes captured stacks undistinguishable from continuations.

Then we introduce extensional and untyped calculi for both of classical sequent calculus and classical natural deduction with connectives for an involutive negation. The involutivity is achieved using focalisation and polarisation, which allow us to implement the idea that captured stacks, unlike continuations, can be inspected. Falsity is given a computational interpretation by delimiting control.

This establishes a formulae-as-types correspondence between the involutive negation in proof theory and a notion of high-level access to the stack theorised by Felleisen and Clements. This allows us to explain the isomorphism we have between not-forall and exists-not.