Formalizing and Computing Propositional Quantifiers
Hugo Férée, Sam van Gool · 2023
A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC). The main contribution of this paper is to provide a formalization of Pitts’ result in the Coq proof assistant, and thus a verified implementation of Pitts’ construction. We in addition provide an OCaml program, extracted from the Coq formalization, which computes propositional formulas that realize intuitionistic versions of ∃ p φ and ∀ p φ from p and φ.