We study a conservative extension of classical propositional logic\ndistinguishing between four modes of statement: a proposition may be affirmed\nor denied, and it may be strong or classical. Proofs of strong propositions\nmust be constructive in some sense, whereas proofs of classical propositions\nproceed by contradiction. The system, in natural deduction style, is shown to\nbe sound and complete with respect to a Kripke semantics. We develop the system\nfrom the perspective of the propositions-as-types correspondence by deriving a\nterm assignment system with confluent reduction. The proof of strong\nnormalization relies on a translation to System F with Mendler-style recursion.\n