Double-Negation Elimination in Some Propositional Logics
| dc.creator | Beeson, Michael | |
| dc.creator | Veroff, Robert | |
| dc.creator | Wos, Larry | |
| dc.date | 2003-01-24 | |
| dc.date.accessioned | 2026-07-07T03:19:23Z | |
| dc.date.available | 2026-07-07T03:19:23Z | |
| dc.description | 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. | |
| dc.description | 32 pages, no figures | |
| dc.identifier | https://arxiv.org/abs/cs/0301026 | |
| dc.identifier | http://arxiv.org/abs/cs/0301026 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/31439 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | F.4.1 | |
| dc.title | Double-Negation Elimination in Some Propositional Logics | |
| dc.type | text |