Double-Negation Elimination in Some Propositional Logics
<|reference_start|>Double-Negation Elimination in Some Propositional Logics: This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none of its deduced steps contains a term of the form n(n(t)) for some term t, where n denotes negation. The first question asks for conditions on the hypotheses that, if satisfied, guarantee the existence of a double-negation-free proof when the conclusion is free of double negation. The second question asks about the existence of an axiom system for classical propositional calculus whose use, for theorems with a conclusion free of double negation, guarantees the existence of a double-negation-free proof. After giving conditions that answer the first question, we answer the second question by focusing on the Lukasiewicz three-axiom system. We then extend our studies to infinite-valued sentential calculus and to intuitionistic logic and generalize the notion of being double-negation free. The double-negation proofs of interest rely exclusively on the inference rule condensed detachment, a rule that combines modus ponens with an appropriately general rule of substitution. The automated reasoning program OTTER played an indispensable role in this study.<|reference_end|>
@article{beeson2003double-negation,
    title={Double-Negation Elimination in Some Propositional Logics},
    author={Michael Beeson, Robert Veroff, Larry Wos},
    journal={arXiv preprint arXiv:cs/0301026},
    year={2003},
    number={Preprint ANL/MCS-P1014-1202},
    archivePrefix={arXiv},
    eprint={cs/0301026},
    primaryClass={cs.LO}
}