Skip to main content
SpringerLink
Log in

Proofs and Countermodels in Non-Classical Logics

  • Published:
Logica Universalis Aims and scope Submit manuscript

Abstract

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable non-classical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class is found. The method is a synthesis of a generation of calculi with internalized relational semantics, a Tait–Schütte–Takeuti style completeness proof, and procedures to finitize the countermodel construction. Finitizations for intuitionistic propositional logic are obtained through the search for a minimal derivation, through pruning of infinite branches in search trees by means of a suitable syntactic counterpart of semantic filtration, or through a proof-theoretic embedding into an appropriate provability logic. A number of examples illustrates the method, its subtleties, challenges, and present scope.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Hodges W, et al. (eds.) Logic: from foundations to applications, pp. 1–32. Oxford Science Publications, Oxford (1996)

  2. Baaz M., Ciabattoni A., Fermüller C.: Hypersequent calculi for Gödel logics—a survey. J. Logic Comput. 13, 835–861 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  3. Basin D., Matthews S., Viganò L.: Natural deduction for non-classical logics. Studia Logica 60, 119–160 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  4. Blackburn P.: Internalizing labelled deduction. J. Logic Comput. 10, 137–168 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  5. Blackburn, P.M., de Rijke, Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)

  6. Boretti, B., Negri, S.: Decidability for Priorean linear time using a fixed-point labelled calculus. In: Giese, M., Waaler, A. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Computer Science, vol. 5607, pp. 108–122. Springer, Berlin (2009)

  7. Brünnler K.: Deep sequent systems for modal logic. Arch. Math. Logic 48, 551–577 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  8. Castellini, C.: Automated Reasoning in Quantified Modal and Temporal Logic. Ph.D. thesis, School of Informatics, University of Edinburgh (2005)

  9. Catach, L.: TABLEAUX: a general theorem prover for modal logic. J. Autom. Reason. 7, 489–510 (1991)

    Google Scholar 

  10. Cerrato, C.: Modal sequents. In: Wansing (ed.) Proof Theory of Modal Logic Kluwer Academic Publishers, Dordrecht pp. 141–166 (1996)

  11. Ciabattoni, A., Galatos, N., Terui, K.: From axioms to analytic rules in nonclassical logics. In: Proc. Logic in Computer Science. IEEE Computer Society, pp. 229–240 (2008)

  12. D’Agostino, M.: Investigations into the Complexity of some Propositional Calculi. Ph.D. thesis, Oxford University Computing Laboratory, Oxford (1990)

  13. Dummett M.A.E., Lemmon E.J.: Modal logics between S4 and S5. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 5, 250–264 (1959)

    Article  MATH  MathSciNet  Google Scholar 

  14. Dyckhoff R.: Contraction-free sequent calculi for intuitionistic logic. J. Symbol. Logic 57, 795–807 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  15. Dyckhoff R., Negri S.: Proof analysis in intermediate logics. Arch. Math. Logic 51, 71–92 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  16. Dyckhoff, R., Negri, S.: A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel–McKinsey–Tarski embedding. J. Logic Comput. (2013). doi:10.1093/logcom/ext036

  17. Fairtlough, M., Mendler, M.: Propositional lax logic. Inf. Comput. 137, 1–33

  18. Ferrari M., Fiorentini C., Fiorino G.: Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models. J. Autom. Reason. 51, 129–149 (2013)

    Article  MathSciNet  Google Scholar 

  19. Fitch F.B.: Tree proofs in modal logic. J. Symbol. Logic 31, 152 (1966)

    Google Scholar 

  20. Fitting M.: Prefixed tableaus and nested sequents. Ann. Pure Appl. Logic 163, 291–313 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  21. Gabbay D.: A general filtration method for modal logics. J. Philos. Logic 1, 29–34 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  22. Gabbay D.: Labelled Deductive Systems. Oxford University Press, Oxford (1996)

    MATH  Google Scholar 

  23. Galmiche D., Salhi Y.: Sequent calculi and decidability for intuitionistic hybrid logic. Inf. Comput. 209, 1447–1463 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  24. Garg, G.: Proof Theory for Authorization Logic and Its Application to a Practical File System. PhD thesis, Carnegie Mellon University (2009)

  25. Garg, G., Genovese, V., Negri, S.: Counter-models from sequent calculi in multi-modal logics. LICS 2012, IEEE Computer Society, pp. 315–324 (2012)

  26. Genovese, V.: Modalities in Access Control: Logics, Proof-Theory and Applications. PhD thesis, University of Luxembourg and University of Torino (2012)

  27. Goranko, V.: Refutation systems in modal logic. Studia Logica 53, 299–324 (1994)

    Google Scholar 

  28. Goré, R.: Tableau methods for modal and temporal logics. In: D’Agostino, M., et al. (eds.) Handbook of Tableau Methods. Kluwer, Dordrecht (1998)

  29. Goré R., Nguyen L.: Clausal tableaux for multimodal logics of belief. Fund. Inf. 94, 21–40 (2009)

    MATH  Google Scholar 

  30. Goré R., Postniece L.: Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic. J. Logic Comput. 20, 233–260 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  31. Goré, R., Ramanayake, R.: Labelled tree sequents, tree hypersequents and nested (deep) sequents. In: Advances in Modal Logic, vol. 9. College Publications, London (2012)

  32. Gödel, K.: Eine Interpretation des intuitionistischen Aussagenkalküls, Ergebnisse eines mathematischen Kolloquiums 4, 39–40 (1933) [English tr. in Gödel’s Collected Works I, 300–303 (1986)]

  33. Hakli R., Negri S.: Reasoning about collectively accepted group beliefs. J. Philos. Logic 40, 531–555 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  34. Negri, S., Hakli, R.: Does the deduction theorem fail for modal logic? Synthese 187, 849–867 (2012)

    Google Scholar 

  35. Kashima R.: Cut-free sequent calculi for some tense logics. Studia Logica 53, 119–135 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  36. Ketonen, O.: Untersuchungen zum Prädikatenkalkül. Annales Acad. Sci. Fenn, Ser. A.I. 23 (1944)

  37. McKinsey J.C., Tarski A.: Some theorems about the sentential calculi of Lewis and Heyting. J. Symbol. Logic 13, 1–15 (1948)

    Article  MATH  MathSciNet  Google Scholar 

  38. Kushida H., Okada M.: A proof-theoretic study of the correspondence of classical logic and modal logic. J. Symbol. Logic 68, 1403–1414 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  39. Larchey-Wendling, D.: Combining proof-search and counter-model construction for deciding Gödel–Dummett logic. In: Proc. CADE-18, LNCS 2392, pp. 94–110 (2002)

  40. Maffezioli, P., Naibo, A., Negri, S.: The Church–Fitch knowability paradox in the light of structural proof theory. Synthese 190, 2677–2716 (2013)

    Google Scholar 

  41. Massacci, F.: Single step tableaux for modal logics: methodology, computations, algorithms. J. Autom. Reason. 24, 319–364 (2000)

    Google Scholar 

  42. Minari P.: Labeled sequent calculi for modal logics and implicit contractions. Arch. Math. Logic 52, 881–907 (2013)

    Article  MATH  MathSciNet  Google Scholar 

  43. Mints G.: Indexed systems of sequents and cut-elimination. J. Philos. Logic 26, 671–696 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  44. Negri S.: Contraction-free sequent calculi for geometric theories, with an application to Barr’s theorem. Arch. Math. Logic 42, 389–401 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  45. Negri S.: Proof analysis in modal logic. J. Philos. Logic 34, 507–544 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  46. Negri, S.: Kripke completeness revisited. In: Primiero, G., Rahman S. (eds.) Acts of Knowledge—History, Philosophy and Logic, pp. 247–282. College Publications (2009)

  47. Negri S.: Proof theory for modal logic. Philosophy Compass 6, 523–538 (2011)

    Article  Google Scholar 

  48. Negri, S.: Proof analysis beyond geometric theories: from rule systems to systems of rules. J. Logic Comput. (in press)

  49. Negri, S., von Plato, J.: Cut elimination in the presence of axioms. Bull. Symbol. Logic 4, 418–435 (1998)

    Google Scholar 

  50. Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)

  51. Negri, S., von Plato, J.: Proof Analysis. Cambridge University Press, Cambridge (2011)

  52. Nerode, A.: Some lectures on modal logic. In: Bauer, F.L. (ed.) Logic, Algebra, and Computation, NATO ASI Series, vol. F79, pp. 281–334. Springer, Berlin (1991)

  53. Orlowska, E., Golińska Pilarek, J.: Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic, vol. 33. Springer, Berlin (2011)

  54. Pinto, L., Dyckhoff, R.: Loop-free construction of counter-models for intuitionistic propositional logic. In: Behara et al. (eds.) Symposia Gaussiana, Conf. A, pp. 225–232. de Gruyter, Berlin (1995)

  55. Poggiolesi F.: A purely syntactic and cut-free sequent calculus for the modal logic of provability. Rev. Symbol. Logic 2, 593–611 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  56. Poggiolesi, F.: Gentzen Calculi for Modal Propositional Logic. Springer, New York (2010)

  57. Restall, G.: Comparing modal sequent systems (2006). http://consequently.org/papers/comparingmodal

  58. Rothenberg, R.: On the relationship between hypersequent calculi and labelled sequent calculi for intermediate logics with geometric Kripke semantics. PhD thesis, University of St Andrews (2010)

  59. Russo, A.: Modal labelled deductive systems. Dept. of Computing, Imperial College, London, Technical Report, vol. 95(7) (1995)

  60. Salerno, J. (ed.): New Essays on the Knowability Paradox. Oxford University Press, Oxford (2009)

  61. Schroeder-Heister, P.: Proof-Theoretic Semantics. Stanford Encyclopedia of Philosophy, online edition (2012)

  62. Schütte K.(1956) Ein System des verknüpfenden Schliessens, Archiv für mathematische Logik und Grundlagenforschung 2, 55–67

  63. Simpson, A.: Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, School of Informatics, University of Edinburgh (1994)

  64. Skura, T.: Refutation systems in propositional logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 16, pp. 115–157. Springer, New York (2011)

  65. Stewart, C., Stouppa, P.: A Systematic Proof Theory for Several Modal Logics, Advances in Modal Logic, vol. 5, pp. 309–333. King’s College Publication, London (2005)

  66. Takeuti, G.: Proof Theory, 2nd edn. North-Holland, Amsterdam (1987)

  67. Troelstra, A., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)

  68. Viganò L.: Labelled Non-Classical Logics. Kluwer, Dordrecht (2000)

    Book  MATH  Google Scholar 

  69. Wansing, H.(ed.): Proof Theory of Modal Logic. Proceedings of the Workshop Held at the University of Hamburg, Hamburg, Applied Logic Series, vol. 2, pp. 19–20, (1993). Kluwer Academic Publishers, Dordrecht (1996)

  70. Wansing, H.: Translation of hypersequents into display sequents. Logic J. IGPL 6, 719–33 (1998)

    Google Scholar 

  71. Wansing, H.: Sequent systems for modal logics. In: Gabbay, D., Guenther F. (eds.) Handbook of Philosophical Logic, 2nd edn, vol. 8, pp. 61–145. Kluwer, Dordrecht (2002)

Download references

Author information

Authors and Affiliations

  1. Department of Philosophy, University of Helsinki, P.O. Box 24, Helsinki, Finland

    Sara Negri

Authors
  1. Sara Negri
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sara Negri.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Negri, S. Proofs and Countermodels in Non-Classical Logics. Log. Univers. 8, 25–60 (2014). https://doi.org/10.1007/s11787-014-0097-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11787-014-0097-1

Mathematics Subject Classification (2010)

Keywords

Search

Navigation