by Mark Bickford, Robert L. Constable
In this article we explore uses of the intersection type as another form of universal quantification. This concept can be expressed naturally in type theories that allow polymorphic terms, such as Computational Type Theory and Intuitionistic Type Theory. We have found this quantifier to be very useful both in theory and in practice. When we use the uniform universal quantifier, we obtain more efficient realizers of constructive content. Moreover, we have been able to find the computational content in classical results by restating them using these quantifiers.
Theorems stated in terms of the usual universal quantifier and implication can sometimes be restated with the corresponding polymorphic versions and given new proofs that construct more uniform, polymorphic, witnesses that are also more efficient.
We illustrate these ideas in the realm of pure logic. We first show how to prove a lemma from Smullyan's book First Order Logic and extract its well hidden computational content. Then we show how to precisely characterize the computational content of theorems in minimal first-order logic, the logic underlying Minlog which Helmut Schwichtenberg and his collaborators have used to create many beautiful examples of how to find efficient computational content from both constructive as well as classical proofs.
bibTex ref: BicCon12poly