Refutation Systems: An Overview and Some Applications to Philosophical Logics

  • Valentin GorankoEmail author
  • Gabriele Pulcini
  • Tomasz Skura
Conference paper
Part of the Logic in Asia: Studia Logica Library book series (LIAA)


Refutation systems are systems of formal, syntactic derivations, designed to derive the non-valid formulas or logical consequences of a given logic. Here we provide an overview with comprehensive references on the historical development of the theory of refutation systems and discuss some of their applications to philosophical logics.



The work of Valentin Goranko was partly supported by a research grant 2015-04388 of the Swedish Research Council. Gabriele Pulcini thankfully acknowledges the support from the Dutch Research Council (NWO) through the Open Competition-SSH project 406.18.TW.009 “A Sentence Uttered Makes a World Appear—Natural Language Interpretation as Abductive Model Generation”.


  1. Anderson, A.R., and N.D. Belnap. 1975. Entailment, vol. 1. Princeton: Princeton University Press.Google Scholar
  2. Avron, A. 1984. Relevance entailment: semantics and formal systems. Journal of Symbolic Logic 49: 334–342.CrossRefGoogle Scholar
  3. Avron, A. 1990. Relevance and paraconsistency - a new approach Part II: The formal systems. Notre Dame Journal of Formal Logic 31: 169–202.CrossRefGoogle Scholar
  4. Berger, G., and H. Tompits. 2013. On axiomatic rejection for the description logic ALC. In Proceedings of KDPD 2013, vol. 8439. Lecture notes in computer science, 65–82. Berlin: Springer.Google Scholar
  5. Bonatti, P. 1993. A Gentzen system for non-theorems. Technical report, Technische Universität Wien, Institut für Informationssysteme.Google Scholar
  6. Bonatti, P., and A.C. Varzi. 1995. On the meaning of complementary systems. In 10th international congress of logic, methodology and philosophy of science. Volume of abstracts, ed. E. Castagli, and M. Konig, 122.Google Scholar
  7. Bonatti, P.A. 1996. Sequent calculi for default and autoepistemic logics. In Proceedings of TABLEAUX ’96, 127–142.Google Scholar
  8. Bonatti, P.A., and N. Olivetti. 2002. Sequent calculi for propositional nonmonotonic logics. ACM Transactions on Computational Logic 3 (2): 226–278.CrossRefGoogle Scholar
  9. Borkowski, L. (ed.). 1970. J. Łukasiewicz: Selected works. Amsterdam: North-Holland Publishing Co.Google Scholar
  10. Bry, F., and S. Torge. 1998. A deduction method complete for refutation and finite satisfiability. In Proceedings of JELIA ’98, 122–138.Google Scholar
  11. Caferra, R., and N. Peltier. 2008. Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview. International Journal of Intelligent Systems 23 (10): 999–1020.CrossRefGoogle Scholar
  12. Caicedo, X. 1978. A formal system for the non-theorems of the propositional calculus. Notre Dame Journal of Formal Logic 19 (1): 147–151.CrossRefGoogle Scholar
  13. Carnielli, W.A., and M.E. Coniglio. 2016. Paraconsistent logic: Consistency, contradiction and negation. Berlin: Springer.Google Scholar
  14. Carnielli, W.A., and G. Pulcini. 2017. Cut-elimination and deductive polarization in complementary classical logic. Logic Journal of the IGPL 25 (3): 273–282.Google Scholar
  15. Citkin, A. 2013. Jankov-style formulas and refutation systems. Reports on Mathematical Logic Logic 48: 67–80.Google Scholar
  16. Citkin, A. 2015a. Characteristic inference rules. Logica Universalis 9 (1): 27–46.CrossRefGoogle Scholar
  17. Citkin, A. 2015b. A meta-logic of inference rules: Syntax. Logic and Logical Philosophy 24: 313–337.Google Scholar
  18. D’Agostino, M. 1999. Tableau methods for classical propositional logic. In Handbook of tableau methods, 45–123. Berlin: Springer.Google Scholar
  19. Dunn, J.M., and G. Restall. 2002. Relevance logic. In Handbook of philosophical Logic, vol. 6, ed. D.M. Gabbay, and F. Guenthner, 1–128. Kluwer.Google Scholar
  20. Dutkiewicz, R. 1989. The method of axiomatic rejection for the intuitionistic propositional logic. Studia Logica 48 (4): 449–459.CrossRefGoogle Scholar
  21. Egly, U., and H. Tompits. 1997. A sequent calculus for intuitionistic default logic. In Proceedings of the 12th workshop on logic programming WLP’97, Tech. Rep. PMS-FB-1997-10, 69–79. LMU, München.Google Scholar
  22. Fiorentini, C. 2015. Terminating sequent calculi for proving and refuting formulas in S4. Journal of Logic and Computation 25 (1): 179–205.CrossRefGoogle Scholar
  23. Fiorentini, C., and M. Ferrari. 2017. A forward unprovability calculus for intuitionistic propositional logic. In Proceedings of TABLEAUX 2017, vol. 10501, LNCS, 114–130. Berlin: Springer.Google Scholar
  24. Fiorentini, C., and M. Ferrari. 2018. Duality between unprovability and provability in forward proof-search for intuitionistic propositional logic. CoRR arXiv:abs/1804.06689.
  25. Garg, D., V. Genovese, and S. Negri. 2012. Countermodels from sequent calculi in multi-modal logics. In Proceedings of the 27th annual IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25–28, 2012, 315–324. IEEE Computer Society.Google Scholar
  26. Gentzen, G. 1935. Unstersuchungen über das logische Schliessen. Mathematische Zeitschrift 39: 176–210. English translation in (Szabo, 1969).Google Scholar
  27. Goranko, V. 1991. Proving unprovability in some normal modal logics. Bulletin of the Section of Logic, PAS 20 (1): 23–29.Google Scholar
  28. Goranko, V. 1994. Refutation systems in modal logic. Studia Logica 53 (2): 299–324.CrossRefGoogle Scholar
  29. Goranko, V., and T. Skura. 2018. Refutation systems in the finite. In Games, Cognition, Logic, College Publications, ed. M. Urbański, T. Skura, and P. Łupkowski, 2020, 173–184.Google Scholar
  30. Goré, R. 1999. Tableau methods for modal and temporal logics. In Handbook of Tableau methods, ed. M. D’Agostino, D. Gabbay, R. Hähnle and J. Posega, 297–396. Kluwer.Google Scholar
  31. Goré, R., and L. Postniece. 2008. Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic. Journal of Logic and Computation 20: 233–260.CrossRefGoogle Scholar
  32. Goudsmit, J.P. 2014. Admissibility and refutation: some characterisations of intermediate logics. Archive for Mathematical Logic 53 (7): 779–808.CrossRefGoogle Scholar
  33. Goudsmit, J.P. 2015. Intuitionistic rules : Admissible rules of intermediate logics. PhD thesis, University of Utrecht, Utrecht.Google Scholar
  34. Hailperin, T. 1961. A complete set of axioms for logical formulas invalid in some finite domains. ZML 7: 84–96.Google Scholar
  35. Härtig, K. 1960. Zur axiomatisierung der nicht-identitäten des aussagenkalkül. ZML 6: 240–247.Google Scholar
  36. Inoué, T. 1989. A note on Stahl’s opposite system. Mathematical Logic Quarterly 35 (5): 387–390.CrossRefGoogle Scholar
  37. Inoué, T. 1989. On Ishimoto’s theorem in axiomatic rejection - the philosophy of unprovability, (in Japanese). Philosophy of Science 22 (5): 77–93.Google Scholar
  38. Inoué, T. 1990. A note on unprovability-preserving sound translations. Logique Et Analyse 33 (31): 243–257.Google Scholar
  39. Inoué, T. 1994. On the atomic formula property of Härtig’s refutation calculus. Bulletin of the Section of Logic, PAS 23 (4): 146–150.Google Scholar
  40. Ishimoto, A. 1981. On the method of axiomatic rejection in classical propositional logic, (in Japanese). Philosophy of Science 14 (5): 45–60.Google Scholar
  41. Kleene, S.C. 1967. Mathematical logic. New Jersey: Wiley.Google Scholar
  42. Kreisel, G., and H. Putnam. 1957. Eine Unableitbarkeitsbeweismethode für den intuitionistischen Aussagenkalkül. Archiv für mathematische Logik und Grundlagenforschung 3: 74–78.CrossRefGoogle Scholar
  43. Kulicki, P. 2000. The use of axiomatic rejection. In Logica yearbook 1999. Filosophia.Google Scholar
  44. Kulicki, P. 2002. Remarks on axiomatic rejection in Aristotle’s syllogistic. Studies in Logic and Theory of Knowledge 5: 231–236.Google Scholar
  45. Kulicki, P. 2012. An axiomatisation of a pure calculus of names. Studia Logica 100 (5): 921–946.CrossRefGoogle Scholar
  46. Lemmon, E., and D. Scott. 1977. An introduction to modal logic, in collaboration with D. Scott. Oxford: Blackwell.Google Scholar
  47. Łukasiewicz, J. 1921. Logika dwuwartościowa (Two-valued logic). Przeglad Filozoficzny 23 (5): 189–205.Google Scholar
  48. Łukasiewicz, J. 1939. O sylogistyce Arystotelesa. Sprawozdania PAU 44: 220–227.Google Scholar
  49. Łukasiewicz, J. 1951. Aristotle’s syllogistic from the standpoint of modern formal logic. Oxford: Clarendon.Google Scholar
  50. Łukasiewicz, J. 1952. On the intuitionistic theory of deduction. Indagationes Mathematicae 14: 202–212.CrossRefGoogle Scholar
  51. Marcinkowski, J., and J. Michaliszyn. 2011. The ultimate undecidability result for the Halpern-Shoham logic. Proceeding of LICS 2011, 377–386.Google Scholar
  52. Mints, G. 1990. Gentzen-type systems and resolution rules. Lecture Notes in Computer Science 417: 198–231.CrossRefGoogle Scholar
  53. Mints, G. 1992. A short introduction to modal logic. CSLI.Google Scholar
  54. Morgan, C., A. Hertel, and P. Hertel. 2007. A sound and complete proof theory for propositional logical contingencies. Notre Dame Journal of Formal Logic 48 (4): 521–530.CrossRefGoogle Scholar
  55. Morgan, C.G. 1973. Sentential calculus for logical falsehoods. Notre Dame Journal of Formal Logic 14: 347–353.CrossRefGoogle Scholar
  56. Negri, S. 2013. On the duality of proofs and countermodels in labelled sequent calculi. In Proceedings of TABLEAUX 2013, 5–9.Google Scholar
  57. Negri, S. 2014. Proofs and countermodels in non-classical logics. Logica Universalis 8 (1): 25–60.CrossRefGoogle Scholar
  58. Negri, S., J. Von Plato, and A. Ranta. 2008. Structural proof theory. Cambridge: Cambridge University Press.Google Scholar
  59. Odintsov, S. 2008. Constructive negations and paraconsistency. Berlin: Springer.Google Scholar
  60. Oetsch, J., and H. Tompits. 2011. Gentzen-type refutation systems for three-valued logics with an application to disproving strong equivalence. In Proceedings of LPNMR 2011, 254–259.Google Scholar
  61. Pinto, L., and R. Dyckhoff. 1995. Loop-free construction of counter-models for intuitionistic propositional logic. In Symposia Gaussiana, 225–232.Google Scholar
  62. Pinto, L., and T. Uustalu. 2009. Proof search and counter-model construction for bi-intuitionistic propositional logic with labelled sequents. In Proceedings of TABLEAUX 2009, 295–309.Google Scholar
  63. Priest, G. 2002. Paraconsistent logic. In Handbook of philosophical logic, 287–393. Berlin: Springer.Google Scholar
  64. Pulcini, G., and A.C. Varzi. 2018. Paraconsistency in classical logic. Synthese 195 (12): 5485–5496.CrossRefGoogle Scholar
  65. Pulcini, G., and A.C. Varzi. 2019. Proof-nets for non-theorems. Forthcoming in Studia Logica.Google Scholar
  66. Scott, D. 1957. Completeness proofs for the intuitionistic sentential calculus. In Summaries of talks presented at the Summer Institute of Symbolic Logic, 2nd ed, 231–241. Princeton: Cornell University.Google Scholar
  67. Skura, T. 1989. A complete syntactical characterization of the intuitionistic logic. Reports on Mathematical Logic 23: 75–80.Google Scholar
  68. Skura, T. 1990. On pure refutation formulations of sentential logics. Bulletin of the Section of Logic, PAS 19 (3): 102–107.Google Scholar
  69. Skura, T. 1991. On decision procedures for sentential logics. Studia Logica 50 (2): 173–179.CrossRefGoogle Scholar
  70. Skura, T. 1992. Refutation calculi for certain intermediate propositional logics. Notre Dame Journal of Formal Logic 33 (4): 552–560.CrossRefGoogle Scholar
  71. Skura, T. 1994. Syntactic refutations against finite models in modal logic. Notre Dame Journal of Formal Logic 35 (4): 595–605.CrossRefGoogle Scholar
  72. Skura, T. 1995. A Łukasiewicz-style refutation system for the modal logic S4. Journal of Philosophical Logic 24 (6): 573–582.CrossRefGoogle Scholar
  73. Skura, T. 1996. Refutations and proofs in S4. In Proof theory of modal logic, ed. H. Wansing, 45–51. Dordrecht: Springer.CrossRefGoogle Scholar
  74. Skura, T. 1999. Aspects of refutation procedures in the intuitionistic logic and related modal systems. Wrocław: Wydawnictwo Uniwersytetu Wrocławskiego.Google Scholar
  75. Skura, T. 2002. Refutations, proofs, and models in the modal logic K4. Studia Logica 70 (2): 193–204.CrossRefGoogle Scholar
  76. Skura, T. 2004a. Maximality and refutability. Notre Dame Journal of Formal Logic 45: 65–72.CrossRefGoogle Scholar
  77. Skura, T. 2004b. Rules and refutation rules for the logic of finite n-ary trees. Journal of Logic and Computation 14 (3): 429–435.CrossRefGoogle Scholar
  78. Skura, T. 2005. Intuitionistic Socratic procedures. Journal of Applied Non-Classical Logics 15 (4): 453–464.CrossRefGoogle Scholar
  79. Skura, T. 2009. A refutation theory. Logica Universalis 3 (2): 293–302.CrossRefGoogle Scholar
  80. Skura, T. 2011a. On refutation rules. Logica Universalis 5 (2): 249–254.CrossRefGoogle Scholar
  81. Skura, T. 2011b. Refutation systems in propositional logic. In Handbook of philosophical logic, vol. 16, ed. D.M. Gabbay, and F. Guenthner, 115–157. Berlin: Springer.Google Scholar
  82. Skura, T. 2013. Refutation methods in modal propositional logic. Warszawa: Semper.Google Scholar
  83. Skura, T. 2016. What is a refutation system? In Let’s be logical, vol. 22, ed. A. Moktefi, A. Moretti, and F. Schang, 189–198. College Publications.Google Scholar
  84. Skura, T. 2017a. The greatest paraconsistent analogue of Intuitionistic Logic. In Proceedings of the 11th Panhellenic logic symposium, 71–76.Google Scholar
  85. Skura, T. 2017b. Refutations in Wansing’s logic. Reports on Mathematical Logic 52: 83–99.CrossRefGoogle Scholar
  86. Skura, T. 2019a. Implicational logic, relevance, and refutability. Logic and Logical Philosophy. forthcoming.Google Scholar
  87. Skura, T. 2019b. Refutation rules and refined model constructions in the modal logic S4. In Preparation.Google Scholar
  88. Słupecki, J. 1955. On Aristotelian syllogistic. Studia Philosophica 4: 275–300.Google Scholar
  89. Słupecki, J., and G. Bryll. 1973. Proof of Ł-decidability of Lewis system S5. Studia Logica 32 (1): 99–105.CrossRefGoogle Scholar
  90. Słupecki, J., G. Bryll, and U. Wybraniec-Skardowska. 1971. Theory of rejected propositions. I. Studia Logica 29 (1): 75–123.CrossRefGoogle Scholar
  91. Słupecki, J., G. Bryll, and U. Wybraniec-Skardowska. 1972. The theory of rejected propositions. II. Studia Logica 30 (1): 97–145.CrossRefGoogle Scholar
  92. Sochacki, R. 2007. Axiomatic rejection in the implicational-negational invariant sentential calculi of Łukasiewicz. Bulletin of the Section of Logic, PAS 36 (1/2): 1–6.Google Scholar
  93. Sochacki, R. 2010. Refutation methods in the study of logical systems. Opole: Wydawnictwo Uniwersytetu Opolskiego.Google Scholar
  94. Sochacki, R. 2011. Refutation systems for a system of nonsense-logic. Logic and Logical Philosophy 20 (3): 233–239.Google Scholar
  95. Stahl, G. 1958. An opposite and an expanded system. ZML 4: 244–247.Google Scholar
  96. Staszek, W. 1971. On proofs of rejection. Studia Logica 29 (1): 17–25.CrossRefGoogle Scholar
  97. Staszek, W. 1972. A certain interpretation of the theory of rejected propositions. Studia Logica 30 (1): 147–152.CrossRefGoogle Scholar
  98. Szabo, M. (ed.). 1969. The collected papers of Gerhard Gentzen. Amsterdam: North-Holland.Google Scholar
  99. Tamminga, A. 1994. Logics of rejection: Two systems of natural deduction. Logique Et Analyse 146: 169–208.Google Scholar
  100. Tiomkin, M.L. 1988. Proving unprovability. In Proceeding of LICS’88), 22–26.Google Scholar
  101. Tiomkin, M.L. 2013. A sequent calculus for a logic of contingencies. Journal of Applied Logic 11 (4): 530–535.CrossRefGoogle Scholar
  102. Trybus, A. 2018. A generalisation of a refutation-related method in paraconsistent logics. Logic and Logical Philosophy 27: 235–261.Google Scholar
  103. Varzi, A.C. 1990. Complementary sentential logics. Bulletin of the Section of Logic, PAS 19: 112–116.Google Scholar
  104. Varzi, A.C. 1992. Complementary logics for classical propositional languages. Kriterion. Zeitschrift für Philosophie 4: 20–24.Google Scholar
  105. Wajsberg, M. 1938. Untersuchungen über den Aussagenkalkül von A. Heyting. Wiadomości Matematyczne 46: 429–435.Google Scholar
  106. Wybraniec-Skardowska, U. 2016. On the mutual definability of the notions of entailment, rejection, and inconsistency. Axioms 5 (2): 15.CrossRefGoogle Scholar
  107. Wybraniec-Skardowska, U. 2018. Rejection in Łukasiewicz’s and Słupecki’s sense. In Lvov-Warsaw School. Past and Present, ed. A. Garrido, and U. Wybraniec-Skardowska, 575–598. Birkhäuser.Google Scholar
  108. Wybraniec-Skardowska, U., and J. Waldmajer. 2011. On pairs of dual consequence operations. Logica Universalis 5 (2): 177–203.CrossRefGoogle Scholar

Copyright information

© Springer Nature Singapore Pte Ltd. 2020

Authors and Affiliations

  • Valentin Goranko
    • 1
    • 2
    Email author
  • Gabriele Pulcini
    • 3
  • Tomasz Skura
    • 4
  1. 1.Stockholm UniversityStockholmSweden
  2. 2.University of Johannesburg (Visiting Professorship)JohannesburgSouth Africa
  3. 3.University of AmsterdamAmsterdamThe Netherlands
  4. 4.University of Zielona GóraZielona GóraPoland

Personalised recommendations