Classical Fω, orthogonality and symmetric candidates

We present a version of system F ω , called inlMMLBox , in which the layer of type constructors is essentially the traditional one of F ω , whereas provability of types is classical. The proof-term calculus accounting for the classical reasoning is a variant of Barbanera and Berardi’s symmetric λ -calculus. We prove that the whole calculus is strongly normalising. For the layer of type constructors, we use Tait and Girard’s reducibility method combined with orthogonality techniques. For the (classical) layer of terms, we use Barbanera and Berardi’s method based on a symmetric notion of reducibility candidate. We prove that orthogonality does not capture the fixpoint construction of symmetric candidates. We establish the consistency of inlMMLBox , and relate the calculus to the traditional system F ω , also when the latter is extended with axioms for classical logic.