Proofs and Refutations for Intuitionistic and Second-Order Logic (Extended Version)

TL;DR

This paper extends the lambda-PRK-calculus to classical second-order logic, integrating polymorphism and existential types, and demonstrates its desirable computational properties and characterization of the intuitionistic fragment.

Contribution

It introduces an extension of lambda-PRK for second-order logic with polymorphism and existential types, proving key computational properties and characterizing the intuitionistic fragment.

Findings

The extended lambda-PRK system enjoys type preservation, confluence, and strong normalization.

A syntactic restriction characterizes the intuitionistic fragment of second-order lambda-PRK.

Canonicity results are established for the extended system.

Abstract

The lambda-PRK-calculus is a typed lambda-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 lambda-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 lambda-PRK, and we study canonicity results.