The Functional Interpretation of the Existential Quantifier
Ruy J. G. B. de Queiroz, Dov M. Gabbay · Logic Journal of IGPL · 1995
We are concerned with showing how ‘labelled’ Natural Deduction presentation systems based on an extension of the so-called Curry-Howard functional interpretation can help us understand and generalise most of the deduction calculi designed to deal with the logical notion of existential quantification. We present the labelling mechanism for ‘∃xD.F(x)’ using what we call ‘ɛ-terms’, which have the form of ‘a’) in a dual form to the ‘Ax.f(x)’ terms of ∀xD.F(x)in the sense that the ‘witness’ (‘α’ in the term above) is chosen (and hidden) at the time of assertion/introduction. With the intention of demonstrating the generality of our framework, we provide a brief comparison with some other calculi of existentials, including the model-theoretic interpretations of Skolem and Herbrand, indicating the way in which some of the classical results on prenex normal forms can be extended to a wide range of logics. The essential ingredient is to look at the conceptual framework of labelled natural deduction as an attempted reconstruction of Frege's functional calculus where the devices of the Begriffsschrift (i.e. connectives and quantifiers) work separately from, yet in harmony with, those of the Grundgesetze (i.e. abstractors)1.