A survey of nonstandard sequent calculi. (English) Zbl 1318.03056
Summary: The paper is a brief survey of some sequent calculi (SC) which do not follow strictly the shape of sequent calculus introduced by Gentzen. We propose the following rough classification of all SC: Systems which are based on some deviations from the ordinary notion of a sequent are called generalised; remaining ones are called ordinary. Among the latter we distinguish three types according to the proportion between the number of primitive sequents and rules. In particular, in one of these types, called Gentzen’s type, we have a subtype of standard SC due to Gentzen. Hence by nonstandard ones we mean all these ordinary SC where other kinds of rules are applied than those admitted in standard Gentzen’s sequent calculi. We describe briefly some of the most interesting or important nonstandard SC belonging to the three abovementioned types.
References:
| [1] | Ajdukiewicz, K., Sprache und Sinn, Erkenntniss IV:100-138, 1934. · Zbl 1048.03009 |
| [2] | Anderson, A. R., and N. D. Belnap, Entailment: the Logic of Relewance and Necessity, vol. I, Princeton University Press, Princeton 1975. · Zbl 0323.02030 |
| [3] | Andrews, P. B., An Introduction to Mathematical Logic and Type Theory: to Truth through Proof, Harcourt Academic Press, Orlando 1986. · Zbl 0617.03001 |
| [4] | Avron A.: Simple Consequence Relations. Information and Computation 92, 105-139 (1991) · Zbl 0733.03007 · doi:10.1016/0890-5401(91)90023-U |
| [5] | Avron, A., The Method of Hypersequents in the Proof Theory of Propositional Non- Classical Logics, in W. Hodges et al. (eds.), Logic: From Foundations to Applications, Oxford Science Publication, Oxford, 1996, pp. 1-32. · Zbl 0861.03043 |
| [6] | Belnap N. D.: Display Logic. Journal of Philosophical Logic 11, 375-417 (1982) · Zbl 0509.03008 |
| [7] | Bernays, P., Betrachtungen zum Sequenzen-Kalkul, in A. T. Tymieniecka (ed.), Contributions to Logic and Methodology in honor of J. M. Bocheński, North-Holland, Amsterdam 1965, pp. 1-44. · Zbl 0192.02901 |
| [8] | Blamey S, Humberstone L.: A Perspective on Modal Sequent Logic. Publications of the Research Institute for Mathematical Sciences, Kyoto University 27, 763-782 (1991) · Zbl 0766.03008 · doi:10.2977/prims/1195169271 |
| [9] | Carnielli W.A.: On Sequents and Tableaux for Many-valued Logics. Journal of Non-Classical Logic 8(1), 59-76 (1991) · Zbl 0774.03006 |
| [10] | Ciabattoni, A., R. Ramanayake, and H. Wansing, Hypersequent and Display Calculi - a unified pespective, Studia Logica, this issue. · Zbl 1344.03043 |
| [11] | Curry, H. B., Foundations of Mathematical Logic, McGraw-Hill, New York 1963. · Zbl 0163.24209 |
| [12] | Dos̆en K.: Sequent-systems for Modal Logic. Journal of Symbolic Logic 50, 149-159 (1985) · Zbl 0562.03009 · doi:10.2307/2273797 |
| [13] | Dos̆en K.: Logical constants as punctuation marks. Notre Dame Journal of Formal Logic 30, 362-381 (1989) · Zbl 0692.03003 · doi:10.1305/ndjfl/1093635154 |
| [14] | Dunn, J. M., and G. M. Hardegree, Algebraic Methods in Philosophical Logic, Clarendon, Oxford 2001. · Zbl 1014.03002 |
| [15] | Ebbinghaus, H. D., J. Flum, and W. Thomas, Mathematical Logic, Springer, Berlin 1984. · Zbl 0556.03001 |
| [16] | Ershow, Y. L., and E. A. Palyutin, Mathematical Logic, MIR, Moscow 1984. · Zbl 1286.03004 |
| [17] | Feys, R., and J. Ladriere, Supplementary notes, in Recherches sur la deduction logique, french translation of Gentzen, Press Univ. de France, Paris 1955. · Zbl 0813.03012 |
| [18] | Forbes, G., Modern Logic, New York 2001. · Zbl 1286.03004 |
| [19] | Gabbay, D., LDS - Labelled Deductive Systems, Clarendon Press, Oxford 1996. · Zbl 0858.03004 |
| [20] | Garson, J.W. Modal Logic for Philosophers, Cambridge University Press, Cambridge 2006. · Zbl 1109.03001 |
| [21] | Gentzen G.: Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen. Mathematische Annalen 107, 329-350 (1932) · Zbl 0005.33803 · doi:10.1007/BF01448897 |
| [22] | Gentzen, G., Untersuchungen über das Logische Schliessen, Mathematische Zeitschrift 39:176-210 and 39:405-431, 1934. · Zbl 0010.14501 |
| [23] | Gentzen G.: Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen 112, 493-565 (1936) · Zbl 0014.38801 · doi:10.1007/BF01565428 |
| [24] | Hasenjaeger, G., Introduction to the Basic Concepts and Problems of Modern Logic, Reidel, Dordrecht 1972. · Zbl 0222.02001 |
| [25] | Hermes, H., Einführung in die Mathematische Logik, Teubner, Stuttgart 1963. · Zbl 0115.00503 |
| [26] | Hertz P.: Über Axiomensysteme für beliebige Satzsysteme. Mathematische Annalen 101, 457-514 (1929) · JFM 55.0627.01 · doi:10.1007/BF01454856 |
| [27] | Hudelmayer, J., and P. Schroeder-Heister, Classical Lambek Calculus, in P. Baumgartner, R. Hähnle, and J. Possega (eds.), Theorem Proving with Analytic Tableaux and Related Methods. 4th International Workshop, TABLEAUX’95 (St. Goar, May 7-10, 1995), Springer LNAI, Bd. 918, 1995, pp. 247-262. · Zbl 1325.03070 |
| [28] | Indrzejczak A.: Generalised Sequent Calculus for Propositional Modal Logics. Logica Trianguli 1, 15-31 (1997) · Zbl 0916.03018 |
| [29] | Indrzejczak A.: Suszko’s Contribution to the Theory of Nonaxiomatic Proof Systems. Bulletin of the Section of logic 38(3-4), 151-162 (2009) · Zbl 1286.03004 |
| [30] | Indrzejczak, A., Natural Deduction, Hybrid Systems and Modal Logics, Springer 2010. · Zbl 1236.03002 |
| [31] | Indrzejczak, A., Rachunki sekwentowe w logice klasycznej, Wyd. UŁ, Łódź 2013. · Zbl 1380.03002 |
| [32] | Jaśkowski S.: On the Rules of Suppositions in Formal Logic. Studia Logica 1, 5-32 (1934) · Zbl 0011.09702 |
| [33] | Kalish, D., and R. Montague, Logic, Techniques of Formal Reasoning, Harcourt, Brace and World, New York 1964. |
| [34] | Kashima R.: Cut-free sequent calculi for some tense logics. Studia Logica 53, 119-135 (1994) · Zbl 0813.03012 · doi:10.1007/BF01053026 |
| [35] | Kleene, S. C., Introduction to Metamathematics, North Holland, Amsterdam 1952. · Zbl 0047.00703 |
| [36] | Kleene, S. C., Mathematical Logic, Willey, New York 1967. · Zbl 0509.03008 |
| [37] | Leblanc H.: Proof routines for the propositional calculus. Notre Dame Journal of Formal Logic 4(2), 81-104 (1963) · Zbl 0199.00301 · doi:10.1305/ndjfl/1093957500 |
| [38] | Leblanc H.: Two separation theorems for natural deduction. Notre Dame Journal of Formal Logic 7(2), 81-104 (1966) · Zbl 0173.00301 · doi:10.1305/ndjfl/1093958557 |
| [39] | Lemmon, E. J., Beginning Logic, Nelson, London 1965. · Zbl 0158.24406 |
| [40] | Leszczyńska-Jasion D, Urbański M, Wiśniewski A.: Socratic Trees. Studia Logica 101(5), 959-986 (2013) · Zbl 1325.03070 · doi:10.1007/s11225-012-9404-0 |
| [41] | Ławrow, I. A., and L. L. Maksimowa, Zadania z teorii mnogości, logiki matematycznej i teorii algorytmów, PWN, Warszawa 2004. |
| [42] | Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge 2001. · Zbl 1113.03051 |
| [43] | Nishimura H.: A Study of Some Tense Logics by Gentzen’s Sequential Method. Publications of the Research Institute for Mathematical Sciences, Kyoto University 16, 343-353 (1980) · Zbl 0446.03013 · doi:10.2977/prims/1195187208 |
| [44] | von Plato J.: Natural deduction with general elimination rules. Archiv for Mathematical Logic 40, 541-567 (1980) · Zbl 1021.03050 · doi:10.1007/s001530100091 |
| [45] | Poggiolesi, F., Gentzen Calculi for Modal Propositional Logic, Springer 2011. · Zbl 1232.03007 |
| [46] | Popper K.: Logic without assumptions. Proceedings of the Aristotelian Society 47, 251-292 (1947) |
| [47] | Popper, K., New foundations for Logic, Mind 56:1947. · Zbl 0029.19608 |
| [48] | Quine, W. Van O., Methods of Logic, Colt, New York 1950. · Zbl 0038.14811 |
| [49] | Rieger, L., Algebraic Methods of Mathematical Logic, Academia, Prague 1967. · Zbl 0218.02001 |
| [50] | Rousseau, G., Sequents in Many Valued Logic, Fundamenta Mathematicae LX(1):22-23, 1967. · Zbl 0154.25504 |
| [51] | Schroeder-Heister P.: Popper’s theory of deductive inference and the concept of a logical constant. History and Philosophy of Logic 5, 79-110 (1984) · Zbl 0568.03004 · doi:10.1080/01445348408837064 |
| [52] | Schroeder-Heister P.: Resolution and the origins of structural reasoning: early proof-theoretic ideas of Hertz and Gentzen. The Bulletin of Symbolic Logic 8(2), 246-265 (2002) · Zbl 1005.03004 · doi:10.2178/bsl/1182353872 |
| [53] | Schroeder-Heister, P., Popper’s structuralist theory of logic, in I. Jarvie, K. Milford, D. Miller (eds.), Karl Popper: A Centenary Assesment, vol III: Science, Ashgate Publishing: Aldershot 2006, pp. 17-36. |
| [54] | Schütte, K., Proof Theory, Springer, Berlin 1977. · Zbl 0367.02012 |
| [55] | Scott, D., Rules and derived rules, in S. Stenlund (ed.), Logical Theory and Semantical Analysis, 1974, pp. 147-161. · Zbl 0296.02012 |
| [56] | Smullyan, R., First-Order Logic, Springer 1968. · Zbl 0172.28901 |
| [57] | Stouppa P.: A deep inference system for the modal logic S5. Studia Logica 85, 199-214 (2007) · Zbl 1162.03011 · doi:10.1007/s11225-007-9028-y |
| [58] | Suppes P., Introduction to Logic, Van Nostrand, Princeton 1957. · Zbl 0077.01105 |
| [59] | Surma, S. J., Wprowadzenie do metamatematyki T. I, Kraków 1965. |
| [60] | Suszko, R., W sprawie logiki bez aksjomatów, Kwartalnik Filozoficzny 17(3/4):199- 205, 1948. |
| [61] | Suszko, R., O analitycznych aksjomatach i logicznych regułach wnioskowania, Poznańskie Towarzystwo Przyjaciół Nauk, Prace Komisji Filozoficznej, 7/5, 1949. |
| [62] | Suszko R.: Formalna teoria wartości logicznych. Studia Logica 6, 145-320 (1957) · Zbl 0173.00402 · doi:10.1007/BF02547932 |
| [63] | Tait, W. W., Normal Derivability in Classical Logic, in The Sintax and Semantics of Infinitary Languages, LNM 72, 1968, pp. 204-236. · Zbl 0206.00502 |
| [64] | Wansing, H., Displaying Modal Logics, Kluwer Academic Publishers, Dordrecht 1999. · Zbl 0964.03020 |
| [65] | Wansing, H., Sequent Systems for Modal Logics, in D. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, vol IV, Reidel Publishing Company, Dordrecht 2002, pp. 89-133. |
| [66] | Wiśniewski A.: Socratic Proofs. Journal of Philosophical Logic 33(3), 299-326 (2004) · Zbl 1048.03009 · doi:10.1023/B:LOGI.0000031374.60945.6e |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
