Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
  1. Home
  2. Books
  3. Proof Analysis
  • Cited by 77
Publisher:
Cambridge University Press
Online publication date:
October 2011
Print publication year:
2011
Online ISBN:
9781139003513
DOI:
https://doi.org/10.1017/CBO9781139003513
Subjects:
Mathematics, Logic, Categories and Sets, Logic, Philosophy
Information

Book description

This book continues from where the authors' previous book, Structural Proof Theory, ended. It presents an extension of the methods of analysis of proofs in pure logic to elementary axiomatic systems and to what is known as philosophical logic. A self-contained brief introduction to the proof theory of pure logic is included that serves both the mathematically and philosophically oriented reader. The method is built up gradually, with examples drawn from theories of order, lattice theory and elementary geometry. The aim is, in each of the examples, to help the reader grasp the combinatorial behaviour of an axiom system, which typically leads to decidability results. The last part presents, as an application and extension of all that precedes it, a proof-theoretical approach to the Kripke semantics of modal and related logics, with a great number of new results, providing essential reading for mathematical and philosophical logicians.

Reviews

"...provide a substantial contribution to the development of proof theory in mathematics.... The book covers a lot of useful material in a concise, efficient and very clearly structured manner. The chapters are written with a palpable intention to show how vast the applicability of the methods is. The results are uniform, general and require a high-level preparation in many different fields. This book can be seen as the stimulating continuation of the authors’ introductory book Structural Proof Theory..."
--F. Poggiolesi, Institut d'Histoire et Philosophie des Sciences, Paris, France, History and Philosophy of Logic

Refine List

Actions for selected content:

Select all | Deselect all
  • View selected items
  • Export citations
  • Download PDF (zip)
  • Save to Kindle
  • Save to Dropbox
  • Save to Google Drive

Save Search

You can save your searches here and later view and run them again in "My saved searches".

Please provide a title, maximum of 40 characters.
Cancel
×

Contents

Contents
References
Bibliography
Avron, A. (1984) On modal systems having arithmetical interpretations. The Journal of Symbolic Logic, vol. 49, pp. 935–942.
Basin, D., S., Matthews, and L., Viganó (1998) Natural deduction for non-classical logics. Studia Logica, vol. 60, pp. 119–160.
van Benthem, J. (1984) Correspondence theory. In D., Gabbay and F., Guenther (eds.) Handbook of Philosophical Logic, vol. 2, pp. 167–247, Kluwer, Dordrecht.
Bernays, P. (1945) Review of Ketonen (1944). The Journal of Symbolic Logic, vol. 10, pp. 127–130.
Bezem, M. and D., Hendriks (2008) On the mechanization of the proof of Hessenberg's theorem in coherent logic. Journal of Automated Reasoning, vol. 40, pp. 61–85.
Blackburn, P. (2000) Representation, reasoning, and relational structures: a hybrid logic manifesto. Logic Journal of the IGPL, vol. 8, pp. 339–365.
Blackburn, P., M., de Rijke, and Y., Venema (2001) Modal Logic. Cambridge University Press.
Blass, A. (1988) Topoi and computation. Bulletin of the European Association for Theoretical Computer Science, vol. 36, pp. 57–65.
Borga, M. (1983) On some proof theoretical properties of the modal logic GL. Studia Logica, vol. 4, pp. 453–459.
Braüner, T. (2000) A cut-free Gentzen formulation of the modal logic S5. Logic Journal of the IGPL, vol. 8, pp. 629–643.
Brouwer, L. (1924) Intuitionistische Zerlegung mathematischer Grundbegriffe. As reprinted in Brouwer'sCollected Works, vol. 1, pp. 275–280, North-Holland, Amsterdam, 1980.
Brouwer, L. (1927) Virtuelle Ordnung und unerweiterbare Ordnung. As reprinted in Brouwer'sCollected Works, vol. 1, pp. 406–408.
Brouwer, L. (1950) Remarques sur la notions d'ordre. As reprinted in Brouwer'sCollected Works, vol. 1, pp. 499–500.
Bull, R. and K., Segerberg (1984) Basic modal logic. In D., Gabbay and F., Guenther (eds.) Handbook of Philosophical Logic, vol. 2, pp. 1–88, Kluwer, Dordrecht. Second edition 2001.
Burris, S. (1995) Polynomial time uniform word problems. Mathematical Logic Quarterly, vol. 41, pp. 173–182.
Buss, S. (1995) On Herbrand's theorem. In D., Leivant (ed.) Logical and Computational Complexity (LNCS 960), pp. 195–209, Springer, Berlin.
Castellini, C. and A., Smaill (2002) A systematic presentation of quantified modal logics. Logic Journal of the IGPL, vol. 10, pp. 571–599.
Cederqvist, J., T., Coquand, and S., Negri (1998) The Hahn-Banach theorem in type theory. In G., Sambin and J., Smith (eds.) Twenty-Five Years of Constructive Type Theory, pp. 39–50, Oxford University Press.
Chagrov, A. and M., Zakharyaschev (1997) Modal Logic. Oxford University Press.
Copeland, B. J. (2002) The genesis of possible worlds semantics. Journal of Philosophical Logic, vol. 31, pp. 99–137.
Coste, M., H., Lombardi, and M.-F., Roy (2001) Dynamical method in algebra: effective Nullstellensätze. Annals of Pure and Applied Logic, vol. 111, pp. 203–256.
Curry, H. B. (1952) The elimination theorem when modality is present. The Journal of Symbolic Logic, vol. 17, pp. 249–265.
van Dalen, D. and R., Statman (1978) Equality in the presence of apartness. In J., Hintikkaet al. (eds.) Essays in Mathematical and Philosophical Logic, pp. 95–116, D. Reidel, Dordrecht.
Degtyarev, A. and A., Voronkov (2001) Equality reasoning in sequent-based calculi. In A., Robinson and A., Voronkov (eds.)Handbook of Automated Reasoning, vol. 1, pp. 611–706, Elsevier, Amsterdam.
Dragalin, A. (1988) Mathematical Intuitionism: Introduction to Proof Theory. American Mathematical Society, Providence, RI.
Dummett, M. (1959) A propositional calculus with a denumerable matrix. The Journal of Symbolic Logic, vol. 24, pp. 97–106.
Dummett, M. and E., Lemmon (1959) Modal logics between S4 and S5. Zeitschrift für Mathematische Logik und Grundlagen derMathematik, vol. 5, pp. 250–264.
Dunn, J. M. and G., Restall (2002) Relevance logic. In D., Gabbay and F., Guenthner (eds.) Handbook of Philosophical Logic, vol. 6, pp. 1–128, Kluwer, Dordrecht.
Dyckhoff, R. (1988) Implementing a simple proof assistant. In J., Derrick and H. A., Lewis (eds.) Workshop on Programming for Logic Teaching, pp. 49–59. Proceedings 23/1988, University of Leeds: Centre for Theoretical Computer Science. Mimeograph.
Dyckhoff, R. and S., Negri (2005) Proof analysis in intermediate propositional logics. Ms.
Dyckhoff, R. and S., Negri (2006) Decision methods for linearly ordered Heyting algebras. Archive for Mathematical Logic, vol. 45, pp. 411–422.
Ehrenfeucht, A. (1959) Decidability of the theory of linear ordering relation. Notices of the American Mathematical Society, vol. 6, pp. 268–269.
Fitch, F. (1966) Tree proofs in modal logic. The Journal of Symbolic Logic, vol. 31, p. 152.
Fitting, M. (1983) Proof Methods for Modal and Intuitionistic Logics. D. Reidel, Dordrecht.
Fitting, M. (1999) A simple propositional S5 tableau system. Annals of Pure and Applied Logic, vol. 96, pp. 107–115.
Fitting, M. and R. L., Mendelsohn (1998) First-OrderModal Logic. Synthese Library vol. 277. Kluwer, Dordrecht.
Freese, R., J., Ježek, and J., Nation (1995) Free Lattices. American Mathematical Society, Providence, RI.
Gabbay, D. (1996) Labelled Deductive Systems. Oxford University Press.
Gentzen, G. (1934–1935) Untersuchungen über das logische Schließen. Mathematische Zeitschrift, vol. 39, pp. 176–210 and 405–431.
Gentzen, G. (1938) Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, vol. 4, pp. 19–44.
Gentzen, G. (1969) The Collected Papers of Gerhard Gentzen. Ed. M., Szabo, North-Holland, Amsterdam.
Gentzen, G. (2008) The normalization of derivations. The Bulletin of Symbolic Logic, vol. 14, pp. 245–257.
Girard, J.-Y. (1987) Proof Theory and Logical Complexity, vol. 1. Bibliopolis, Naples.
Gödel, K. (1933) Eine Interpretation des intuitionistischen Aussagenkalküls. Ergebnisse eines mathematischen Kolloquiums, vol. 4, pp. 39–40. English tr. in Gödel's Collected Works (1986), vol. 1, pp. 300–303.
Goldblatt, R. (2005) Mathematical modal logic: a view of its evolution. In D., Gabbay and J., Woods (eds.) Handbook of the History of Logic, vol. 7, pp. 1–98, Elsevier, Amsterdam.
Goré, R. (1998) Tableau methods for modal and temporal logis. In M., D'Agostinoet al. (eds.) Handbook of Tableau Methods, Kluwer, Dordrecht.
Goré, R. and R., Ramanayake (2008) Valentini's cut-elimination for provability logic resolved. In C., Areces and R., Goldblatt (eds.) Advances in Modal Logic, vol. 7, pp. 67–96, College Publications, London.
Hallett, M. and U., Majer (ed.) (2004) David Hilbert's Lectures on the Foundations of Geometry1891–1902. Springer, Berlin.
Hakli, R. and S., Negri (2011a) Does the deduction theorem fail for modal logic? Synthese, in press.
Hakli, R. and S., Negri (2011b) Reasoning about collectively accepted group beliefs. Journal of Philosophical Logic, vol. 40, pp. 531–555.
Heyting, A. (1927) Zur intuitionistischen Axiomatik der projektiven Geometrie. Mathematische Annalen, vol. 98, pp. 491–538.
Heyting, A. (1956) Intuitionism, an Introduction, North-Holland, Amsterdam.
Hilbert, D. (1899) Grundlagen der Geometrie. Teubner, Leipzig.
Janisczak, A. (1953) Undecidability of some simple formalized theories. Fundamenta Mathematicae, vol. 40, pp. 131–139.
Jankov, V. A. (1968) The calculus of the weak ‘law of excluded middle’. Mathematics of the USSR: Izvestija, vol. 2, pp. 997–1004.
Joachimski, F. and R., Matthes (2003) Short proofs of normalization for the simply typed λ-calculus, permutative conversions and Gödel's T. Archive for Mathematical Logic, vol. 42, pp. 59–87.
Johnstone, Peter T. (1977) Topos Theory. LMS Monograph no. 10. Academic Press, London.
Kanger, S. (1957) Provability in Logic. Almqvist & Wiksell, Stockholm.
Kanger, S. (1963) A simplified proof method for elementary logic. In P., Braffort and D., Hirshberg (eds.) Computer Programming and Formal Systems, pp. 87–94, North-Holland, Amsterdam.
Ketonen, O. (1943) ‘Luonnollisen päättelyn’ kalkyylista (On the calculus of ‘natural deduction’, in Finnish). Ajatus (Yearbook of the Finnish Philosophical Society), vol. 12, pp. 128–140.
Ketonen, O. (1944) Untersuchungen zum Prädikatenkalkül. Ann. Acad. Sci. Fenn., Ser. A.I. 23.
Kleene, S. (1952) Introduction to Metamathematics. North-Holland, Amsterdam.
Kohlenbach, U. (2008) Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer, Berlin.
Kreisel, G. (1954) Review of Janisczak (1953). Mathematical Reviews, vol. 15, pp. 669–670.
Kripke, S. (1959) A completeness theorem in modal logic. The Journal of Symbolic Logic, vol. 24, pp. 1–14.
Kripke, S. (1963a) Semantical analysis of modal logic I. Normal modal propositional calculi. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, vol. 9, pp. 67–96.
Kripke, S. (1963b) Semantical considerations on modal logic. Acta Philosophica Fennica, vol. 16, pp. 83–94.
Kripke, S. (1965) Semantical Analysis of Intuitionistic Logic I. In M., Dummett and J., Crossley (eds.) Formal Systems and Recursive Functions, pp. 92–130, North-Holland, Amsterdam.
Kushida, H. and M., Okada (2003) A proof-theoretic study of the correspondence of classical logic and modal logic. The Journal of Symbolic Logic, vol. 68, pp. 1403–1414.
Läuchli, H. and J., Leonard (1966) On the elementary theory of linear order. Fundamenta Mathematicae, vol. 59, pp. 109–116.
Leivant, D. (1981) On the proof theory of the modal logic for arithmetic provability. The Journal of Symbolic Logic, vol. 46, pp. 531–538.
Lopez-Escobar, L. (1999) Standardizing the N-systems of Gentzen. In X., Caicedo and C., Montenegro (eds.) Models, Algebras and Proofs, pp. 411–434, Dekker, New York.
McKinsey, J. and A., Tarski (1948) Some theorems about the sentential calculi of Lewis and Heyting. The Journal of Symbolic Logic, vol. 13, pp. 1–15.
Mac Lane, S. and I., Moerdijk (1992) Sheaves in Geometry and Logic. Springer, New York.
Maksimova, L. (1979) Interpolation properties of superintuitionistic logics. Studia Logica, vol. 38, pp. 419–428.
Mares, E. (2004) Relevant logic: A Philosophical Interpretation. Cambridge University Press.
Massacci, F. (2000) Single step tableaux for modal logics: methodology, computations, algorithms. Journal of Automated Reasoning, vol. 24, pp. 319–364.
Meinander, A. (2010) A solution of the uniform word problem for ortholattices. Mathematical Structures in Computer Science, vol. 20, pp. 625–638.
Mints, G. (1970) Cut-free calculi of type S5. Translation of Russian original in A., Slisenko (ed.) Studies in Constructive Mathematics andMathematical Logic, vol. 8, pt II, pp. 79–82, n.p., Leningrad.
Mints, G. (1997) Indexed systems of sequents and cut-elimination. Journal of Philosophical Logic, vol. 26, pp. 671–696.
Moen, A. (2003) A normal form for Gödel Löb sequent calculus, manuscript. Abstract published in The Bulletin of Symbolic Logic, vol. 10 (2004), p. 266.
Mostowski, A. (1965) Thirty Years of Foundational Studies. The Philosophical Society of Finland, Helsinki.
Negri, S. (1999) Sequent calculus proof theory of intuitionistic apartness and order relations. Archive for Mathematical Logic, vol. 38, pp. 521–547.
Negri, S. (2003) Contraction-free sequent calculi for geometric theories, with an application to Barr's theorem. Archive for Mathematical Logic, vol. 42, pp. 389–401.
Negri, S. (2005a) Proof analysis in modal logic. Journal of Philosophical Logic, vol. 34, pp. 507–544.
Negri, S. (2005b) Permutability of rules for linear lattices. Journal of Universal Computer Science, vol. 11, pp. 1986–1995.
Negri, S. (2008) Proof analysis in non-classical logics. In C., DimitracopoulosL., NewelskiD., Normann, and J., Steel (eds.) Logic Colloquium '05, ASL Lecture Notes in Logic, vol. 28, pp. 107–128, Cambridge University Press.
Negri, S. (2009) Kripke completeness revisited. In G., Primiero and S., Rahman (eds.) Acts of Knowledge – History, Philosophy and Logic, pp. 247–282, College Publications, London.
Negri, S. and J., von Plato (1998) Cut elimination in the presence of axioms. The Bulletin of Symbolic Logic, vol. 4, pp. 418–435.
Negri, S. and J., von Plato (2001) Structural Proof Theory. Cambridge University Press.
Negri, S. and J., von Plato (2002) Permutability of rules in lattice theory. Algebra Universalis, vol. 48, pp. 473–477.
Negri, S. and J., von Plato (2004) Proof systems for lattice theory. Mathematical Structures in Computer Science, vol. 14, pp. 507–526.
Negri, S. and J., von Plato (2005) The duality of classical and constructive notions and proofs. In L., Crosilla and P., Schuster (eds.) From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, pp. 149–161, Oxford University Press.
Negri, S., J., von Plato, and Th., Coquand (2004) Proof-theoretic analysis of order relations. Archive for Mathematical Logic, vol. 43, pp. 297–309.
Nerode, A. (1991) Some lectures on modal logic. In F., Bauer (ed.) Logic, Algebra, and Computation, NATO ASI Series, Springer, New York.
Ohlbach, H. (1993) Translation methods for non-classical logics – an overview. Bulletin of the IGPL, vol. 1, pp. 69–91.
Ohnishi, M. and K., Matsumoto (1957) Gentzen method in modal calculi. Osaka Mathematical Journal, vol. 9, pp. 113–130.
Palmgren, E. (2002) An intuitionistic axiomatization of real closed fields. Mathematical Logic Quarterly, vol. 48, pp. 297–299.
von Plato, J. (1995) The axioms of constructive geometry. Annals of Pure and Applied Logic, vol. 76, pp. 169–200.
von Plato, J. (1996) Organization and development of a constructive axiomatization. In S., Berardi and M., Coppo (eds.) Types for Proofs and Programs (LNCS 1158), pp. 288–296, Springer, Berlin.
von Plato, J. (1997) Formalization of Hilbert's geometry of incidence and parallelism. Synthese, vol. 110, pp. 127–141.
von Plato, J. (2001a) Natural deduction with general elimination rules. Archive for Mathematical Logic, vol. 40, pp. 541–567.
von Plato, J. (2001b) A proof of Gentzen's Hauptsatz without multicut. Archive for Mathematical Logic, vol. 40, pp. 9–18.
von Plato, J. (2001c) Positive lattices. In P., Schusteret al. (eds.) Reuniting the Antipodes, pp. 185–197, Kluwer, Dordrecht.
von Plato, J. (2004) Ein Leben, ein Werk – Gedanken über das wissenschaftliche Schaffen des finnischen Logikers Oiva Ketonen. In R., Seising (ed.) Form, Zahl, Ordnung: Studien zur Wissenschafts- und Technikgeschichte, pp. 427–435, Franz Steiner Verlag, Stuttgart.
von Plato, J. (2005) Normal derivability in modal logic. Mathematical Logic Quarterly, vol. 51, pp. 632–638.
von Plato, J. (2007) In the shadows of the Löwenheim-Skolem theorem: early combinatorial analyses of mathematical proofs. The Bulletin of Symbolic Logic, vol. 13, pp. 189–225.
von Plato, J. (2008) Gentzen's proof of normalization for intuitionistic natural deduction. The Bulletin of Symbolic Logic, vol. 14, pp. 240–244.
von Plato, J. (2009) Gentzen's logic. In D., Gabbay and J., Woods (eds.) Handbook of the History of Logic, vol. 5: Logic from Russell to Church, pp. 667–721, Elsevier, Amsterdam.
von Plato, J. (2010) Combinatorial analysis of proofs in projective and affine geometry. Annals of Pure and Applied Logic, vol. 162, no. 2, pp. 144–161.
Pohlers, W. (2009) Proof Theory: The First Step into Impredicativity. Springer, Berlin.
Popkorn, S. [Harold Simmons] (1994) First Steps in Modal Logic. Cambridge University Press.
Prawitz, D. (1965) Natural Deduction: A Proof-Theoretical Study. Almqvist & Wicksell, Stockholm.
Prawitz, D. (1971) Ideas and results in proof theory. In J., Fenstad (ed.) Proceedings of the Second Scandinavian Logic Symposium, pp. 235–308, North-Holland, Amsterdam.
Read, S. (2008) Harmony and Modality. In C., DégremontL., Kieff, and H., Rückert (eds.) Dialogues, Logics and Other Strong Things: Essays in Honour of Shahid Rahman, pp. 285–303, College Publications, London.
Restall, G. (2000) An Introduction to Substructural Logics. Routledge.
Restall, G. (2008) Proofnets for S5: sequents and circuits for modal logic. In C., DimitracopoulosL., NewelskiD., Normann, and J., Steel (eds.) Logic Colloquium '05, ASL Lecture Notes in Logic, vol. 28, pp. 151–172, Cambridge University Press.
Sambin, G. and S., Valentini (1982) The modal logic of provability: the sequential approach. Journal of Philosophical Logic, vol. 11, pp. 311–342.
Sasaki, K. (2002) A cut-free sequent system for the smallest interpretability logic. Studia Logica, vol. 70, pp. 353–372.
Sato, M. (1980) A cut-free Gentzen-type system for the modal logic S5. The Journal of Symbolic Logic, vol. 45, pp. 67–84.
Schmidt, R. and U., Hustadt (2003) A principle for incorporating axioms into the first-order translation ofmodal formulae. Lecture Notes in Artificial Intelligence, vol. 2741, pp. 412–426.
Schroeder-Heister, P. (1984) A natural extension of natural deduction. The Journal of Symbolic Logic, vol. 49, pp. 1284–1300.
Scott, D. (1968) Extending the topological interpretation to intuitionistic analysis. Compositio Mathematica, vol. 20, pp. 194–210.
Shvarts, G. (1989) Gentzen style systems for K45 and K45D. In A. R., Meyer and M. A., Taitslin (eds.) Logic at Botik '89 (LNCS 363), pp. 245–256, Springer, Berlin.
Skolem, T. (1920) Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze, nebst einem Theoreme über dichte Mengen. As reprinted in Skolem 1970, pp. 103–136.
Skolem, T. (1970) Selected Papers in Logic. Ed. J., Fenstad, University of Oslo Press, Oslo.
Smorynski, C. (1973) Elementary intuitionistic theories. The Journal of Symbolic Logic, vol. 38, pp. 102–134.
Solovay, R. (1976) Provability interpretations of modal logic. Israel Journal of Mathematics, vol. 25, pp. 287–304.
Stouppa, P. (2007) A deep inference system for the modal logic S5. Studia Logica, vol. 85, pp. 199–214.
Szpilrajn, E. (1930) Sur l'extension de l'ordre partiel. Fundamenta Mathematicae, vol. 16, pp. 386–389.
Takeuti, G. (1987) Proof Theory. North-Holland, Amsterdam.
Tarski, A. (1949) On essential undecidability. The Journal of Symbolic Logic, vol. 14, pp. 75–76.
Tennant, N. (1992) Autologic. Edinburgh University Press.
Troelstra, A. and D., van Dalen (1988) Constructivism inMathematics, vol. 1. North-Holland, Amsterdam.
Troelstra, A. and H., Schwichtenberg (1996) Basic Proof Theory. Cambridge University Press. Second edition 2000.
Valentini, S. (1983) The modal logic of provability: cut-elimination. Journal of Philosophical Logic, vol. 12, pp. 471–476.
Vickers, S. (1989)Topology via Logic. Cambridge University Press.
Viganó, L. (2000) Labelled Non-Classical Logics. Kluwer, Dordrecht.
Wang, H. (1960) Towards mechanical mathematics. IBM Journal of Research and Development, vol. 4, pp. 2–22.
Wansing, H. (1994) Sequent calculi for normal modal propositional logics. Journal of Logic and Computation, vol. 4, pp. 125–142.
Wansing, H. (ed.) (1996) Proof Theory of Modal Logic. Kluwer, Dordrecht.
Wansing, H. (2002) Sequent systems for modal logics. In D., Gabbay and F., Guenther (eds.) Handbook of Philosophical Logic, 2nd edn, vol. 8, pp. 61–145, Kluwer, Dordrecht.

Metrics

Altmetric attention score

Full text views

Total number of HTML views: 0
Total number of PDF views: 0 *
Loading metrics...

Book summary page views

Total views: 0 *
Loading metrics...

* Views captured on Cambridge Core between #date#. This data will be updated every 24 hours.

Usage data cannot currently be displayed.