Formalizing and computing propositional quantifiers
summary
Pitts’ 1992 result — propositional quantifiers definable inside intuitionistic propositional logic — is fully formalized in Coq formalization and an executable OCaml extractor is produced that computes formulas realizing ∃p φ and ∀p φ. The development formalizes a terminating g4ip proof search, bootstraps Pitts’ mutual definition into a verified algorithm, and proves correctness; extracted code works but exhibits exponential growth (e.g. five nested arrows yields interpolants of several thousand nodes), with room for pruning.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 0:46Pig's theorem overview
- 3:18Second-order quantifiers
- 5:01Syntactic vs semantic proofs
- 6:51G4ip calculus intro
- 8:16EP and AP formulas
- 12:14Math to code translation
- 15:24Weight function refinement
- 16:50Iris and Coq libraries
- 18:16Main theorem proof
- 19:01OCaml demo and performance
- 20:48Future directions
- 21:32Q&A