The Proof-Theoretic Validity of the Principles of Right Negation & Negation Introduction A Generalised Theory of Reductio ad Absurdum

This paper investigates the proof-theoretic validity of the sequent calculus principle of right negation (R¬) and the natural deduction principle of negation introduction (¬I) within classical logic. It argues that these principles should not be regarded just as inferential devices applicable to traditional reductio ad absurdum (RAA) derivations in which the antecedent collapses into contradiction and the assumption responsible for that collapse is discharged, yielding its negated form as the conclusion. Rather, the paper develops a generalised theory of RAA according to which every logically valid application of R¬ and ¬I possesses a reductio structure. Under this framework, a derivation qualifies as reductio whenever a conclusion, or at least one conclusion in a multiconclusion proof, stands in a law of excluded middle (LEM) and law of non-contradiction (LNC) relationship to an assumption or inferentially significant formula occurring within the antecedent. Through a systematic examination of traditional and non-traditional derivations in both sequent calculus and natural deduction, including contradiction-based, arbitrary-assumption, arbitrary-conclusion, and contradiction-free constructions, the paper demonstrates three principal results. First, R¬ and ¬I function as genuine reductio-generating principles within traditional RAA derivations. Second, they permit the derivation of arbitrary conclusions through assumption discharge, thus providing a proof-theoretically motivated alternative to the use of right weakening (RW), L⊥, and ⊥E. Third, their legitimacy remains intact in contradiction-free multiconclusion derivations, where their operation is grounded in logical validity rather than antecedent collapse. The study concludes that R¬ and ¬I should be understood as general reductio-generating principles embedded within the foundations of classical proof systems.