Classical Gentzen-type Methods in Propositional Many-valued Logics

  • Arnon Avron
Part of the Studies in Fuzziness and Soft Computing book series (STUDFUZZ, volume 114)


A classical Gentzen-type system is one which employs two-sided sequents, together with structural and logical rules of a certain characteristic form. A decent Gentzen-type system should allow for direct proofs, which means that it should admit some useful forms of cut elimination and the subformula property. In this survey we explain the main difficulty in developing classical Gentzen-type systems with these properties for many-valued logics. We then illustrate with numerous examples the various possible ways of overcoming this difficulty, and the strong connection between semantic completeness and cut-elimination in each case. Our examples include practically all 3-valued and 4-valued logics, as well as Gödel finite-valued logics and some well-known infinite-valued logics.


Atomic Formula Strong Completeness Propositional Constant Strong Soundness Subformula Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Arieli, O. and Avron, A.: Logical bilattices and inconsistent data, in Proc. 9th IEEE Annual Symp. on Logic in Computer Science (LICS’94), IEEE Press (1994) 468–476Google Scholar
  2. 2.
    Arieli, O. and Avron, A.: Reasoning with logical bilattices, J. of Logic, Language and Information, vol. 5, no. 1 (1996) 25–63MathSciNetMATHGoogle Scholar
  3. 3.
    Arieli, O. and Avron, A.: The value of four values, Artificial Intelligence, vol. 102, no. 1 (1998) 97–141MathSciNetMATHCrossRefGoogle Scholar
  4. 4.
    Anderson, A.R. and Belnap, N.D.: Entailment, vol. I. Princeton University Press (1975)Google Scholar
  5. 5.
    Anderson, A.R. and Belnap, N.D.: Entailment, vol. II. Princeton University Press (1992)Google Scholar
  6. 6.
    Avellone, A., Ferrari, M. and Miglioli, P.: Duplication-free tableaux calculi together with cut-free and contraction-free sequent calculi for the interpolable propositional intermediate logics, Logic Journal of IGPL, vol. 7 (1999) 447–480MathSciNetMATHCrossRefGoogle Scholar
  7. 7.
    Avron, A. and Konikowska, B.: Decomposition proof systems for GödelDummett logics, Studia Logica, vol. 69 (2001) 197–219MathSciNetMATHCrossRefGoogle Scholar
  8. 8.
    Avron, A. and Lev, I.: Canonical propositional gentzen-type systems, in Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR 2001) (Goré, R., Leitsch, A. and Nipkow, T. eds.), Springer Verlag, LNAI 2083 (2001) 529–544Google Scholar
  9. 9.
    Avron, A.: Relevant entailment–semantics and formal systems, Journal of Symbolic Logic, vol. 49 (1984) 334–342MathSciNetMATHCrossRefGoogle Scholar
  10. 10.
    Avron, A.: On an implication connective of RM, Notre Dame Journal of Formal Logic, vol. 27 (1986) 201–209MathSciNetMATHCrossRefGoogle Scholar
  11. 11.
    Avron, A.: A constructive analysis of RM, Journal of Symbolic Logic, vol. 52 (1987) 939–951MathSciNetMATHCrossRefGoogle Scholar
  12. 12.
    Avron, A.: Natural 3-valued logics: Characterization and proof theory, J. of Symbolic Logic, vol. 56, no. 1 (1991) 276–294MathSciNetMATHCrossRefGoogle Scholar
  13. 13.
    Avron, A.: Simple consequence relations, Information and Computation, vol. 92, no. 1 (1991) 105–139MathSciNetMATHCrossRefGoogle Scholar
  14. 14.
    Avron, A.: Gentzen-type systems, resolution and tableaux, Journal of Automated Reasoning, vol. 10 (1993) 265–281MathSciNetMATHCrossRefGoogle Scholar
  15. 15.
    Avron, A.: Multiplicative Conjunction as an Extensional Conjunction, Logic Journal of the IGPL, vol. 5 (1997) 181–208MathSciNetMATHCrossRefGoogle Scholar
  16. 16.
    Avron, A.: On the expressive power of three-valued and four-valued languages, Journal of Logic and Computation, vol. 9 (1999) 977–994MathSciNetMATHCrossRefGoogle Scholar
  17. 17.
    Belnap, N.D.: How computers should think, in Contemporary Aspects of Philosophy ( Ryle, G. ed.), Oriel Press, Stocksfield, England (1977) 30–56Google Scholar
  18. 18.
    Belnap, N.D.: A useful four-valued logic, in Modern Uses of Multiple-Valued Logic ( Epstein, G. and Dunn, J.M. eds.), Reidel, Dordrecht (1977) 7–37Google Scholar
  19. 19.
    Baaz, M., Fermüller, C.G. and, Salzer, G.: Automated deduction for many-valued logics, in Handbook of Automated Reasoning (Robinson, A. and Voronkov, A. eds. ), Elsevier Science Publishers (2000)Google Scholar
  20. 20.
    Busch, D.: Sequent formalizations of three-valued logic, in Partiality, Modality, and Nonmonotonicity, Studies in Logic, Language and Information, CSLI Publications (1996) 45–75Google Scholar
  21. 21.
    da Costa, N.C.A.: On the theory of inconsistent formal systems, Notre Dame Journal of Formal Logic, vol. 15 (1974) 497–510MathSciNetMATHCrossRefGoogle Scholar
  22. 22.
    D’Ottaviano, I.L.M. and da Costa, N.C.A.: Sur un problemè de Jankowski, C.R. Acad. Sc. Paris, vol. 270, Sèrie A (1970) 1349–1353Google Scholar
  23. 23.
    Dunn, J.M. and Meyer, R.K.: Algebraic completeness results for dummett’s lc and its extensions, Z. math. Logik und Grundlagen der Mathematik, vol. 17 (1971) 225–230MathSciNetMATHCrossRefGoogle Scholar
  24. 24.
    D’Ottaviano, I.L.M.: The completeness and compactness of a three-valued first-order logic, Revista Colombiana de Matematicas, vol. XIX, no. 1–2 (1985) 31–42MathSciNetGoogle Scholar
  25. 25.
    Dummett, M.: A propositional calculus with a denumerable matrix, Journal of Symbolic Logic, vol. 24 (1959) 96–107MathSciNetGoogle Scholar
  26. 26.
    Dunn, J.M.: Relevance logic and entailment, in [34], vol. III, ch. 3 (1986) 117224Google Scholar
  27. 27.
    Dyckhoff, R.: A deterministic terminating sequent calculus for Gödel-Dummett logic, Logic Journal of IGPL, vol. 7 (1999) 319–326MathSciNetMATHCrossRefGoogle Scholar
  28. 28.
    Epstein, R.L.: The semantic foundation of logic, vol. I: propositional logics, ch. IX. Kluwer Academic Publisher (1990)Google Scholar
  29. 29.
    Fitting, M.: Bilattices in logic programming, in 20th Int. Symp. on Multiple-Valued Logic (Epstein, G. ed. ), IEEE Press (1990) 238–246Google Scholar
  30. 30.
    Fitting, M.: Kleene’s logic, generalized, Journal of Logic and Computation, vol. 1 (1990) 797–810CrossRefGoogle Scholar
  31. 31.
    Fitting, M.: Bilattices and the semantics of logic programming, Journal of Logic Programming, vol. 11, no. 2 (1991) 91–116MathSciNetMATHCrossRefGoogle Scholar
  32. 32.
    Fitting, M.: Kleene’s three-valued logics and their children, Fundamenta Informaticae, vol. 20 (1994) 113–131MathSciNetMATHGoogle Scholar
  33. 33.
    Gentzen, G.: Investigations into logical deduction, in The Collected Works of Gerhard Gentzen ( Szabo, M.E. ed.), North Holland, Amsterdam (1969) 68–131Google Scholar
  34. 34.
    Gabbay, D.M. and Guenthner, F.: Handbook of Philosophical Logic. D. Reidel Publishing company (1986)Google Scholar
  35. 35.
    Ginsberg, M.L.: Multiple-valued logics, in Readings in Non-Monotonic Reasoning ( Ginsberg, M.L. ed.), Los-Altos, CA (1987) 251–258Google Scholar
  36. 36.
    Ginsberg, M.L.: Multivalued logics: A uniform approach to reasoning in AI, Computer Intelligence, vol. 4 (1988) 256–316Google Scholar
  37. 37.
    Girard, J.-Y.: Linear logic, Theoretical Computer Science, vol. 50 (1987) 1–102MathSciNetMATHCrossRefGoogle Scholar
  38. 38.
    Girard, J.-Y.: Proof Theory and Logical Complexity. Bibliopolis (1987)Google Scholar
  39. 39.
    Gödel, K.: On the intuitionistic propositional calculus, in Collected Work of K. Gödel (Feferman, S. and all, eds.), vol. I, Oxford University Press (1986) 222–225Google Scholar
  40. 40.
    Hähnle, R.: Tableaux for multiple-valued logics, in Handbook of Tableau Methods (D’Agostino, M., Gabbay, D.M., Hähnle, R. and Posegga, J. eds. ), Kluwer Publishing Company (1999) 529–580CrossRefGoogle Scholar
  41. 41.
    Hajek, P.: Metamathematics of Fuzzy Logic. Kluwer Academic Publishers (1998)Google Scholar
  42. 42.
    Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall International, U.K. (1986)Google Scholar
  43. 43.
    Kleene, S.C.: Introduction to metamathematics. Van Nostrad (1950)Google Scholar
  44. 44.
    Los, J. and Suszko, R.: Remarks on sentential logics, Indagationes Mathematicae, vol. 20 (1958) 177–183MathSciNetGoogle Scholar
  45. 45.
    Lukasiewicz, J.: On 3-valued logic, in Polish Logic (McCall, S. ed.), Oxford University Press (1967)Google Scholar
  46. 46.
    Monteiro, A.: Construction des algebres de Lukasiewicz trivalentes dans les algebres de Boole monadiques, i Mat. Jap., vol. 12 (1967) 1–23MathSciNetMATHGoogle Scholar
  47. 47.
    Ohnishi, M. and Matsumoto, K.: Gentzen methods in modal calculi, Osaka Mathematical Journal, vol. 9 (1957) 113–130MathSciNetMATHGoogle Scholar
  48. 48.
    Rozoner, L.I.: On interpretation of inconsistent theories, Information Sciences, vol. 47 (1989) 243–266MathSciNetCrossRefGoogle Scholar
  49. 49.
    Schmitt, P.H.: Computational aspects of three-valued logic, in Proceedings of the 8th Conference on Automated Deduction, Springer Verlag, LNCS 230 (1986) 190–198Google Scholar
  50. 50.
    Scott, D.S.: Completeness and axiomatization in many-valued logics, in Proc. of the Tarski symposium, vol. XXV of Proc. of Symposia in Pure Mathematics, ( Rhode Island ), American Mathematical Society (1974) 411–435Google Scholar
  51. 51.
    Scott, D.S.: Rules and derived rules, in Logical Theory and Semantical Analysis ( Stenlund, S. ed.), Reidel, Dordrecht (1974) 147–161CrossRefGoogle Scholar
  52. 52.
    Scroggs, S.J.: Extensions of the Lewis system s5, Journal of Symbolic Logic, vol. 16 (1951) 112–120MathSciNetMATHCrossRefGoogle Scholar
  53. 53.
    Schroeder-Heister, P. and Dosen, K. eds.: Substructural Logics. Oxford University Press (1993)Google Scholar
  54. 54.
    Slupecki, J.: Der volle dreiwertige aussagenkalkül, Corn. rend. Soc. Sci. Lett. de Varsovie, vol. 29 (1936) 9–11MATHGoogle Scholar
  55. 55.
    Sobocinski, B.: Axiomatization of partial system of three-valued calculus of propositions The Journal of Computing Systems, vol. 11, no. 1 (1952) 23–55MathSciNetGoogle Scholar
  56. 56.
    Sonobe, O.: A Gentzen-type formulation of some intermediate propositional logics, J. of Tsuda College, vol. 7 (1975) 7–14MathSciNetGoogle Scholar
  57. 57.
    Troelstra, A.S. and Schwichtenberg, H.: Basic Proof Theory, 2nd Edition. Cambridge University Press (2000)Google Scholar
  58. 58.
    Urquhart, A.: Many-valued logic, in [34], vol. III, ch. 2 (1986) 71–116Google Scholar
  59. 59.
    Visser, A.: On the completeness principle: A study of provability in Heyting’s arithmetic, Annals of Mathematical Logic, vol. 22 (1982) 263–295MathSciNetMATHCrossRefGoogle Scholar
  60. 60.
    Wójcicki, R.: Lectures on Propositional Calculi. Warsaw: Ossolineum (1984)MATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Arnon Avron
    • 1
  1. 1.School of Computer ScienceTel-Aviv UniversityRamat AvivIsrael

Personalised recommendations