Fusing Quantifiers and Connectives: Is Intuitionistic Logic Different?

Abstract

A paper by Dag Westerståhl and myself twenty years ago introduced operators that are both connectives and quantifiers. We introduced two binary operators that are classically interdefinable: one that fuses conjunction and existential quantification and one that fuses implication and universal quantification. We called the system PFO. A complete Gentzen-Prawitz style Natural Deduction axiomatization of classical PL was provided. For intuitionistic PL, however, it seemed that existential quantification should be fused with disjunction rather than with conjunction. Whether this was true, and if so why, were questions not answered at the time. Also, it seemed that there is no uniform definition of such a disjunctive-existential operator in classical PFO. This, too, remained a conjecture. In this paper, I return to these previously unresolved questions, and resolve them.