Proofs and Refutations for Intuitionistic and Second-Order Logic

BARENBAUM, PABLO; FREUND, TEODORO

Varsovia

Conferencia; 31st EACSL Annual Conference on Computer Science Logic (CSL 2023); 2023

Universidad de Varsovia

The λ^{PRK}-calculus is a typed λ-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend λ^{PRK} to encompass classical second-order logic, by incorporating parametric polymorphism and existential types. The system is shown to enjoy good computational properties, such as type preservation, confluence, and strong normalization, which is established by means of a reducibility argument. We identify a syntactic restriction on proofs that characterizes exactly the intuitionistic fragment of second-order λ^{PRK}, and we study canonicity results.