## Double-Negation Elimination in Some Propositional Logics

Title | Double-Negation Elimination in Some Propositional Logics |

Publication Type | Journal Article |

Year of Publication | 2005 |

Authors | Beeson, M, Veroff, R, Wos, L |

Journal | Studia Logica |

Volume | 80 |

Issue | 2 |

Pagination | 195-234 |

Date Published | 04/2005 |

Other Numbers | ANL/MCS-P1014-1202 |

Abstract | 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. |

http://www.mcs.anl.gov/papers/P1014.pdf |