Double-Negation Elimination in Some Propositional Logics

TL;DR

This paper investigates conditions and axiom systems that guarantee the existence of double-negation-free proofs in propositional logics, using automated reasoning to analyze classical, infinite-valued, and intuitionistic logics.

Contribution

It provides new conditions and demonstrates the existence of double-negation-free proofs in various propositional logics, focusing on the Lukasiewicz system and extending to infinite-valued and intuitionistic logic.

Findings

Conditions for double-negation-free proofs in propositional logics

Existence of axiom systems guaranteeing double-negation-free proofs

Application of automated reasoning with OTTER in proof analysis

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.