A Constructive Logic with Classical Proofs and Refutations (Extended Version)

TL;DR

This paper introduces a conservative extension of classical propositional logic that differentiates between affirmation/denial and strong/classical modes, providing a natural deduction system with soundness, completeness, and normalization properties.

Contribution

It presents a novel logical framework combining constructive and classical proofs, along with a term assignment system and normalization proof via translation to System F.

Findings

Sound and complete Kripke semantics for the logic

A confluent reduction system for the proof calculus

Strong normalization established through translation to System F

Abstract

We study a conservative extension of classical propositional logic distinguishing 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.