A Constructive Logic with Classical Proofs and Refutations

BARENBAUM, PABLO; FREUND, TEODORO

Roma

Conferencia; 2021 Symposium on Logic in Computer Science (LICS); 2021

Università di Roma (Sapienza)

We study a conservative extension of classical propositional logicdistinguishing between four modes of statement: a proposition may be affirmed or denied, and it may be strong or classical. Proofs of strong propositions must be constructive in some sense, whereas proofs of classical propositions proceed by contradiction. The system, in natural deduction style, is shown to be sound and complete with respect to a Kripke semantics. We develop the system from the perspective of the propositions-as-types correspondence by deriving a term assignment system with confluent reduction. The proof of strong normalization relies on a translation to System F with Mendler-style recursion.