Abstract
In this paper I elaborate a proof system that is able to prove all classical first order logic consequences of consistent premise sets, without proving trivial consequences of inconsistent premises (as in A, ¬A ⊢ B). Essentially this result is obtained by formally distinguishing consequences that are the result of merely decomposing the premises into their subformulas from consequences that may be the result of also composing ‘new’, more complex formulas. I require that, whenever ‘new’ formulas are derived, they are to be preceded by a special +-symbol and these +-preceded formulas are not to be decomposed. By doing this, the proofs are separated into a decomposition phase followed by a composition phase. The proofs are recursive, axiomatizable and, as they do not trivialize inconsistent premise sets, they define a very strong non-transitive paraconsistent logic, for which I also provide an adequate semantics.
I am indebted to the referees for providing useful comments on a former draft and for pointing my attention to some interesting related literature.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Batens, D.: It might have been classical logic. Logique et Analyse, http://logica.ugent.be/centrum/preprints/PCLs.pdf
Batens, D.: Inconsistency-adaptive logics. In: Orłowska, E. (ed.) Logic at Work. Essays Dedicated to the Memory of Helena Rasiowa, pp. 445–472. Physica Verlag (Springer) (1999)
Batens, D.: A formal approach to problem solving. In: Delrieux, C., Legris, J. (eds.) Computer Modeling of Scientific Reasoning, pp. 15–26. Universidad Nacional del Sur, Bahia Blanca (2003)
Batens, D., Provijn, D.: Pushing the search paths in the proofs. A study in proof heuristics. Logique et Analyse 173-175, 113–134 (2001) (appeared 2003)
Besnard, P., Hunter, A.: Quasi-classical logic: Non-trivializable classical reasoning from incosistent information. In: Froidevaux, C., Kohlas, J. (eds.) ECSQARU 1995. LNCS, vol. 946, pp. 44–51. Springer, Heidelberg (1995)
Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. The Journal of Symbolic Logic 22(3), 250–268 (1957)
D’Agostino, M., Floridi, L.: The enduring scandal of deduction. Synthese 167(2) (2009)
Gentzen, G.: Untersuchungen über das logische schließen. ii. Mathematische Zeitschrift 39, 405–431 (1935) ISSN 0025-5874
Hunter, A.: Reasoning with contradictory information using quasi-classical logic. Journal of Logic and Computation 10, 677–703 (1999)
Hunter, A.: A semantic tableau version of first-order quasi-classical logic. In: Benferhat, S., Besnard, P. (eds.) ECSQARU 2001. LNCS (LNAI), vol. 2143, pp. 544–555. Springer, Heidelberg (2001)
Jago, M.: Logical information and epistemic space. Synthese 167(2) (2009)
Provijn, D.: Prospectieve dynamiek. Filosofische en technische onderbouwing van doelgerichte bewijzen en bewijsheuristieken. PhD thesis, Universiteit Gent, Belgium (2005) (unpublished PhD thesis)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Verdée, P. (2011). Strong Paraconsistency by Separating Composition and Decomposition in Classical Logic. In: Beklemishev, L.D., de Queiroz, R. (eds) Logic, Language, Information and Computation. WoLLIC 2011. Lecture Notes in Computer Science(), vol 6642. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20920-8_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-20920-8_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20919-2
Online ISBN: 978-3-642-20920-8
eBook Packages: Computer ScienceComputer Science (R0)