Double-Negation Elimination in Some Propositional Logics

Studia Logica 80 (2-3):195-234 (2005)

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 formn(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
Keywords Philosophy   Logic   Mathematical Logic and Foundations   Computational Linguistics
Categories (categorize this paper)
DOI 10.1007/s11225-005-8469-4
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 43,865
Through your library

References found in this work BETA

Formal Logic. Prior - 1955 - Oxford University Press.
A Machine-Oriented Logic Based on the Resolution Principle.J. A. Robinson - 1966 - Journal of Symbolic Logic 31 (3):515-516.

View all 13 references / Add more references

Citations of this work BETA

Add more citations

Similar books and articles

A Hierarchy of Weak Double Negations.Norihiro Kamide - 2013 - Studia Logica 101 (6):1277-1297.
Defining Double Negation Elimination.G. Restall - 2000 - Logic Journal of the IGPL 8 (6):853-860.
Negation and Paraconsistent Logics.Soma Dutta & Mihir K. Chakraborty - 2011 - Logica Universalis 5 (1):165-176.
Modal Translations in Substructural Logics.Kosta Došen - 1992 - Journal of Philosophical Logic 21 (3):283 - 336.
Sequent Calculi for Visser's Propositional Logics.Kentaro Kikuchi & Ryo Kashima - 2001 - Notre Dame Journal of Formal Logic 42 (1):1-22.
Glivenko Theorems for Substructural Logics Over FL.Nikolaos Galatos & Hiroakira Ono - 2006 - Journal of Symbolic Logic 71 (4):1353 - 1384.
Axiomatizations of Intuitionistic Double Negation.Milan Bozic & Kosta Došen - 1983 - Bulletin of the Section of Logic 12 (2):99-102.
Normal Modal Substructural Logics with Strong Negation.Norihiro Kamide - 2003 - Journal of Philosophical Logic 32 (6):589-612.


Added to PP index

Total views
51 ( #162,639 of 2,266,145 )

Recent downloads (6 months)
2 ( #598,676 of 2,266,145 )

How can I increase my downloads?


My notes

Sign in to use this feature