Between Hilbert and Gentzen: four-valued consequence systems and structural reasoning | Archive for Mathematical Logic
Skip to main content
Springer Nature Link
Log in

Between Hilbert and Gentzen: four-valued consequence systems and structural reasoning

  • Published:
Archive for Mathematical Logic Aims and scope Submit manuscript

Abstract

Structural reasoning is simply reasoning that is governed exclusively by structural rules. In this context a proof system can be said to be structural if all of its inference rules are structural. A logic is considered to be structuralizable if it can be equipped with a sound and complete structural proof system. This paper provides a general formulation of the problem of structuralizability of a given logic, giving specific consideration to a family of logics that are based on the Dunn–Belnap four-valued semantics. It is shown how sound and complete structural proof systems can be constructed for a spectrum of logics within different logical frameworks.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Notes

  1. In the interests of brevity, I will refer to them simply as ‘structural’ and ‘logical’ rules respectively.

  2. A consequence relation in Tarski’s sense is usually understood as a relation that obeys reflexivity, monotonicity and transitivity (cut), all of which are purely structural principles.

  3. Cf. also an interesting distinction between the ‘structure-free’ and ‘structure-dependent’ rules for logical connectives presented by Nuel Belnap in [7, p. 31].

  4. A clause in disjunctive form is a disjunction of literals, where literal is an atomic formula or its negation.

  5. Usually one considers an ‘implicative form’ of clauses \(\varphi _1 \wedge \ldots \wedge \varphi _m \rightarrow \psi _1 \vee \ldots \vee \psi _n\) with an arrow instead of turnstile. The latter is more appropriate for the purposes of the present paper, however.

  6. Linear resolution is presented in detail in [30, pp. 61–80]. For an explanation of the relationship between resolution and cut see, e.g., [9, pp. 286–287].

  7. It is widely acknowledged that Hertz’s ideas were critical for the emergence of structural reasoning; for example, [28] stresses that the “very idea of sequent calculi and of structural rules was first conceived by Hertz”. Schroeder-Heister in [35] gives a detailed explanation of Hertz’s contribution, remarking that the calculi that were developed in the 1920s by Paul Hertz are structural systems. Remarkably, Hertz’s systems deal with sequents that have only one formula in the succedent, i.e., sequents that take the form \(\Gamma \vdash \psi \).

  8. Note, that Definition 1.2 employs a rather general idea of substitution, whereby any formula can be (simultaneously) substituted by some other formula; such substitutivity simply ensures structural invariance of a rule to which it is applied. This idea of substitutivity is compliant with Łoś and Suszko’s [29] structurality condition imposed on Tarskian consequence operation Cn: \(\varepsilon Cn(\varphi ) \subseteq Cn(\varepsilon \varphi ),\) for every endomorphism \(\varepsilon \) and every formula \(\varphi \). In this sense it is clear why the rule \(\varphi \wedge \psi \vdash \varphi \) cannot be regarded as structural under this definition: substituting, for example, \(\chi \) for \(\varphi \wedge \psi \) results in an invalid rule \(\chi \vdash \psi \).

  9. In referring to basic properties of connectives and consequence relations, I refer to properties that are exactly determined by primitive axioms and rules. Of course, there may also be derivative properties that are reflected by theorems of the system under consideration, as well as derivable (or even admissible) rules. Such derivative properties can be of a mixed, logical-structural nature, depending of the types of axioms and rules that are needed to obtain them. Moreover, as noted by an anonymous referee, [7] observes, that some properties of conjunction and disjunction are structure-dependent; this can be made more explicit by replacing Gentzen’s rule for \(\wedge \) and \(\vee \) by Ketonen’s.

  10. The subscript stands here of course for ‘conjunction, disjunction, negation’.

  11. Observe that, in [21], Gentzen deals with sequents of the Set-Set type when formulating sequent calculus for classical logic LK, albeit without the non-emptiness restriction. His calculus for intuitionistic logic LJ is an example of a system constructed in the finite Set-Fmla framework.

  12. Dunn’s original dissertation of 1966, which is now published in [16] contains (on pp. 115–116) essentially the same system with a reference to [4].

  13. Clearly, FDE is a Gentzen system in the sense of Definition 1.1 (as are all the consequence systems considered in this paper.) Interestingly, Anderson and Belnap, in using \(\rightarrow \) instead of \(\vdash \), treat their system as ‘a Hilbert-style formalism’ for axiomatizing the set of ‘tautological entailments’. In the final section, I will show how the systems constructed in this paper incorporate linearity of inferences; this is an important feature of Hilbert-style systems.

  14. In [38] another structural system FDE(-) was formulated, in which disjunctive and conjunctive contexts were taken separately. Adam Přenosil has pointed out to me that the deductive equivalence of FDE(-) with FDE remains in doubt, and that combined disjunctive-conjunctive (conjunctive-disjunctive) context can do a better job.

  15. Font and Verdú remark that for their purposes it is enough to deal with algebras \(\mathbb {A} = (A, \wedge , \lnot )\) of type (2, 1), and define as usual \(x \vee y = \lnot (\lnot x\wedge \lnot y)\), see [19, p. 389].

  16. Observations of the last two paragraphs, together with Lemma 6.4, was inspired by a comment of an anonymous referee.

  17. Inherent already by Hertz’s systems. As Schroeder-Heister observes, “Hertz was the first to consider tree-like proof structures, an idea that became essential for Gentzen’s later development of natural deduction and of the full sequent calculus” [35, p. 251].

  18. As Schroeder-Heister states: “Two particular features of structural reasoning which go beyond Gentzen style sequent calculi are the following:

    Sequents may occur as assumptions.

    and

    Cut is an indispensable rule which cannot be eliminated.

    The first feature normally implies the second one” [35, p. 247].

References

  1. Albuquerque, H., Přenosil, A., Rivieccio, U.: An algebraic view of super-Belnap logics. Stud. Logica 105, 1051–1086 (2017)

    Article  MathSciNet  Google Scholar 

  2. Anderson, A.R., Belnap, N.D.: Entailment: The Logic of Relevance and Necessity, vol. I. Princeton University Press, Princeton (1975)

    MATH  Google Scholar 

  3. Anderson, A.R., Belnap, N.D., Dunn, J.M.: Entailment: The Logic of Relevance and Necessity, vol. II. Princeton University Press, Princeton (1992)

    MATH  Google Scholar 

  4. Belnap, N.D.: A formal analysis of entailment. Technical report, U.S. Office of Naval Research, vol. 7. Group Psychology Branch, New Haven (1960)

  5. Belnap, N.D.: A useful four-valued logic. In: Dunn, J.M., Epstein, G. (eds.) Modern Uses of Multiple-Valued Logic, pp. 8–37. D. Reidel Publishing Company, Dordrecht (1977)

    Google Scholar 

  6. Belnap, N.D.: How a computer should think. In: Ryle, G. (ed.) Contemporary Aspects of Philosophy, pp. 30–55. Oriel Press (1977)

  7. Belnap, N.D.: Life in the undistributed middle. In: Došen, K., Schroeder-Heister, P. (eds.) Substructural Logics, pp. 31–41. Oxford University Press (1993)

  8. Béziau, J.-Y.: Bivalent semantics for De Morgan logic (the uselessness of four-valuedness). In: Carnielli, W.A., Coniglio, M.E., D’Ottaviano, I.M.L. (eds.) The Many Sides of Logic, pp. 391–402. College Publication, London (2009)

  9. Bimbó, K.: Proof Theory: Sequent Calculi and Related Formalisms. CRC Press, Boca Raton (2015)

  10. Buss, S., Johannsen, J.: On linear resolution. Journal on Satisfiability, Boolean Modeling, and Computation 10, 23–35 (2017)

    Article  MathSciNet  Google Scholar 

  11. Dunn, J.M.: Intuitive semantics for first-degree entailment and coupled trees. Philos. Stud. 29, 149–168 (1976)

    Article  MathSciNet  Google Scholar 

  12. Dunn, J.M.: Positive modal logic. Stud. Logica 55, 301–317 (1995)

  13. Dunn, J.M.: A comparative study of various model-theoretic treatments of negation: a history of formal negation. In: Gabbay, D.M., Wansing, H. (eds.) What is Negation?, pp. 23–51. Kluwer Academic Publishers, Dordrecht (1999)

  14. Dunn, J.M.: Partiality and its dual. Stud. Logica 66, 5–40 (2000)

    Article  MathSciNet  Google Scholar 

  15. Dunn, J.M., Hardegree, G.M.: Algebraic Methods in Philosophical Logic. Oxford University Press, Oxford (2001)

    MATH  Google Scholar 

  16. Dunn, J.M.: The Algebra of Intensional Logics, with an Introductory Essay by Katalin Bimbó, Logic PhDs, vol. 2. College Publications (2019)

  17. Font, J.M.: Belnap’s four-valued logic and De Morgan lattices. Log. J. IGPL 5, 413–440 (1997)

  18. Font, J.M., Guzmán, F., Verdú, V.: Characterization of the reduced matrices for the \(\{\wedge , \vee \}\)-fragment of classical logic. Bull. Sect. Log. 20, 124–128 (1991)

    Google Scholar 

  19. Font, J.M., Verdú, V.: Abstract characterization of a four-valued logic. In: Proceedings of the 18th International Symposium on Multiple-Valued Logic, pp. 389–396. The IEEE Computer Society Press (1988)

  20. Gentzen, G.: Über die Existenz unabhängiger Axiomensystem zu unendlichen Satzsystemen. Math. Ann. 107, 329–350 (1933)

  21. Gentzen, G.: Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39, I, 176–210, and II, 405–431 (1935)

  22. Gentzen, G.: The Collected Papers of Gerhard Gentzen. North-Holland Pub. Co., Amsterdam (1969)

    Google Scholar 

  23. Hertz, P.: Über Axiomensysteme für beliebige Satzsysteme. Math. Ann. 101, 457–514 (1929)

    Article  MathSciNet  Google Scholar 

  24. Humberstone, L.: The Connectives. MIT Press, Cambridge (2011)

    Book  Google Scholar 

  25. Jaśkowski, S.: On the rules of supposition in formal logic. Stud. Logica 1, 5–32 (1934)

    MATH  Google Scholar 

  26. Koslow, A.: A Structuralist Theory of Logic. Cambridge University Press (2005)

  27. Koslow, A.: Structuralist logic: implications, inferences and consequences. Log. Univers. 1, 167–181 (2007)

    Article  MathSciNet  Google Scholar 

  28. Legris, J.: Paul Hertz and the origins of structural reasoning. In: Jean-Yves, Béziau. (ed.) Universal Logic: An Anthology, pp. 3–10. Basel et al, Birkhäuser (2012)

    Chapter  Google Scholar 

  29. Łoś, J., Suszko, R.: Remarks on sentential logics. Indag. Math. 20, 177–183 (1958)

    Article  MathSciNet  Google Scholar 

  30. Loveland, D.W., Hodel, R.E., Sterrett, S.G.: Three Views of Logic: Mathematics, Philosophy and Computer Science. Princeton University Press, Princeton (2014)

    Book  Google Scholar 

  31. Omori, H., Wansing, H.: 40 years of FDE: an introductory overview. Stud. Logica 105, 1021–1049 (2017)

    Article  MathSciNet  Google Scholar 

  32. Restall, G.: An Introduction to Substructural Logics. Routlege, London (2000)

    Book  Google Scholar 

  33. Rivieccio, U.: An infinity of super-Belnap logics. J. Appl. Non-Class. Log. 22, 319–335 (2012)

  34. Ripley, D.: Anything goes. Topoi 34, 25–36 (2015)

    Article  MathSciNet  Google Scholar 

  35. Schroeder-Heister, P.: Resolution and the origins of structural reasoning: early proof-theoretic ideas of Hertz and Gentzen. Bull. Symbol. Log. 8, 246–265 (2002)

    Article  MathSciNet  Google Scholar 

  36. Shoesmith, D.J., Smiley, T.J.: Multiple Conclusion Logic. Cambridge University Press, Cambridge (1978)

    Book  Google Scholar 

  37. Shramko, Y.: Truth, falsehood, information and beyond: the American plan generalized. In: Bimbo, K. (ed.) J. Michael Dunn on Information Based Logics, Outstanding Contributions to Logic, vol. 8, pp. 191–212. Springer (2016)

  38. Shramko, Y.: New Essays on Belnap–Dunn Logic. In: Omori, H., Wansing, H. (eds.) First-degree entailment and structural reasoning. Synthese Library (2019)

  39. Shramko, Y.: Dual–Belnap logic and anything but falsehood. J. Appl. Log. IfCoLoG J. Log. Appl. 6, 413–433 (2019)

    MathSciNet  Google Scholar 

  40. Shramko, Y.: First-degree entailment and binary consequence systems. J. Appl. Log. IfCoLoG J. Log. Appl. 7, 1223–1242 (2020)

    Google Scholar 

  41. Shramko, Y., Dunn, J.M., Takenaka, T.: The trilattice of constructive truth values. J. Log. Comput. 11, 761–788 (2001)

    Article  MathSciNet  Google Scholar 

  42. Shramko, Y., Zaitsev, D., Belikov, A.: First-degree entailment and its relatives. Stud. Logica 105, 1291–1317 (2017)

    Article  MathSciNet  Google Scholar 

  43. Shramko, Y., Zaitsev, D., Belikov, A.: The Fmla–Fmla axiomatizations of the exactly true and non-falsity logics and some of their cousins. J. Philos. Log. 48, 787–808 (2019)

    Article  MathSciNet  Google Scholar 

  44. von Plato, J.: Gentzen’s logic Handbook of the History and Philosophy of Logic, vol. 5, pp. 667–721. Elsevier, Amsterdam (2009)

Download references

Acknowledgements

I would like to thank Adam Přenosil and Nadiia Kozachenko for valuable feedback concerning axiomatization of the system FDE\(_\textsc {s}\). I also thank the anonymous referees for their useful suggestions.

Author information

Authors and Affiliations

  1. Department of Philosophy, Kryvyi Rih State Pedagogical University, Kryvyi Rih, 50086, Ukraine

    Yaroslav Shramko

Authors
  1. Yaroslav Shramko
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Shramko, Y. Between Hilbert and Gentzen: four-valued consequence systems and structural reasoning. Arch. Math. Logic 61, 627–651 (2022). https://doi.org/10.1007/s00153-021-00806-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00153-021-00806-2

Keywords

Mathematics Subject Classification

Search

Navigation