Results for 'proof theory'

1000+ found
Order:
See also
  1. Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
    This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   160 citations  
  2.  12
    Proof theory.Gaisi Takeuti - 1976 - New York, N.Y., U.S.A.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
    This comprehensive monograph is a cornerstone in the area of mathematical logic and related fields. Focusing on Gentzen-type proof theory, the book presents a detailed overview of creative works by the author and other 20th-century logicians that includes applications of proof theory to logic as well as other areas of mathematics. 1975 edition.
    Direct download  
     
    Export citation  
     
    Bookmark   127 citations  
  3.  6
    Proof theory.K. Schütte - 1977 - New York: Springer Verlag.
  4.  13
    Proof theory: sequent calculi and related formalisms.Katalin Bimbó - 2015 - Boca Raton: CRC Press, Taylor & Francis Group.
    Sequent calculi constitute an interesting and important category of proof systems. They are much less known than axiomatic systems or natural deduction systems are, and they are much less known than they should be. Sequent calculi were designed as a theoretical framework for investigations of logical consequence, and they live up to the expectations completely as an abundant source of meta-logical results. The goal of this book is to provide a fairly comprehensive view of sequent calculi -- including a (...)
    Direct download  
     
    Export citation  
     
    Bookmark   9 citations  
  5.  40
    Proof theory of modal logic.Heinrich Wansing (ed.) - 1996 - Boston: Kluwer Academic Publishers.
    Proof Theory of Modal Logic is devoted to a thorough study of proof systems for modal logics, that is, logics of necessity, possibility, knowledge, belief, time, computations etc. It contains many new technical results and presentations of novel proof procedures. The volume is of immense importance for the interdisciplinary fields of logic, knowledge representation, and automated deduction.
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  6. Proof Theory of Finite-valued Logics.Richard Zach - 1993 - Dissertation, Technische Universität Wien
    The proof theory of many-valued systems has not been investigated to an extent comparable to the work done on axiomatizatbility of many-valued logics. Proof theory requires appropriate formalisms, such as sequent calculus, natural deduction, and tableaux for classical (and intuitionistic) logic. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   17 citations  
  7.  98
    Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.
    Structural proof theory is a branch of logic that studies the general structure and properties of logical and mathematical proofs. This book is both a concise introduction to the central results and methods of structural proof theory, and a work of research that will be of interest to specialists. The book is designed to be used by students of philosophy, mathematics and computer science. The book contains a wealth of results on proof-theoretical systems, including extensions (...)
    Direct download  
     
    Export citation  
     
    Bookmark   119 citations  
  8.  35
    Proof theory: a selection of papers from the Leeds Proof Theory Programme, 1990.Peter Aczel, Harold Simmons & Stanley S. Wainer (eds.) - 1992 - New York: Cambridge University Press.
    This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.
    Direct download  
     
    Export citation  
     
    Bookmark  
  9.  7
    Proof theory and intuitionistic systems.Bruno Scarpellini - 1971 - New York,: Springer Verlag.
  10.  55
    Handbook of proof theory.Samuel R. Buss (ed.) - 1998 - New York: Elsevier.
    This volume contains articles covering a broad spectrum of proof theory, with an emphasis on its mathematical aspects. The articles should not only be interesting to specialists of proof theory, but should also be accessible to a diverse audience, including logicians, mathematicians, computer scientists and philosophers. Many of the central topics of proof theory have been included in a self-contained expository of articles, covered in great detail and depth. The chapters are arranged so that (...)
    Direct download  
     
    Export citation  
     
    Bookmark   33 citations  
  11.  75
    PROOF THEORY. Gödel and the metamathematical tradition.Jeremy Avigad - 2010 - In Kurt Gödel, Solomon Feferman, Charles Parsons & Stephen G. Simpson (eds.), Kurt Gödel: essays for his centennial. Association for Symbolic Logic.
    At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  12.  21
    Goal-directed proof theory.Dov M. Gabbay - 2000 - Boston: Kluwer Academic. Edited by Nicola Olivetti.
    Goal Directed Proof Theory presents a uniform and coherent methodology for automated deduction in non-classical logics, the relevance of which to computer science is now widely acknowledged. The methodology is based on goal-directed provability. It is a generalization of the logic programming style of deduction, and it is particularly favourable for proof search. The methodology is applied for the first time in a uniform way to a wide range of non-classical systems, covering intuitionistic, intermediate, modal and substructural (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  13.  30
    Proof theory for theories of ordinals—I: recursively Mahlo ordinals.Toshiyasu Arai - 2003 - Annals of Pure and Applied Logic 122 (1-3):1-85.
    This paper deals with a proof theory for a theory T22 of recursively Mahlo ordinals in the form of Π2-reflecting on Π2-reflecting ordinals using a subsystem Od of the system O of ordinal diagrams in Arai 353). This paper is the first published one in which a proof-theoretic analysis à la Gentzen–Takeuti of recursively large ordinals is expounded.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  14.  26
    Proof theory for theories of ordinals II: Π3-reflection.Toshiyasu Arai - 2004 - Annals of Pure and Applied Logic 129 (1-3):39-92.
    This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   12 citations  
  15.  32
    Proof theory of classical and intuitionistic logic.Jan von Plato - 2011 - In Leila Haaparanta (ed.), The development of modern logic. New York: Oxford University Press.
    This chapter focuses on the development of Gerhard Gentzen's structural proof theory and its connections with intuitionism. The latter is important in proof theory for several reasons. First, the methods of Hilbert's old proof theory were limited to the “finitistic” ones. These methods proved to be insufficient, and they were extended by infinitistic principles that were still intuitionistically meaningful. It is a general tendency in proof theory to try to use weak principles. (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  16.  28
    Proof theory of reflection.Michael Rathjen - 1994 - Annals of Pure and Applied Logic 68 (2):181-224.
    The paper contains proof-theoretic investigation on extensions of Kripke-Platek set theory, KP, which accommodate first-order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Пn reflection rules. This leads to consistency proofs for the theories KP+Пn reflection using a small amount of arithmetic and the well-foundedness of a certain ordinal system with respect to primitive decending sequences. Regarding future work, we intend to avail ourselves of (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   37 citations  
  17.  70
    Proof Theory for Reasoning with Euler Diagrams: A Logic Translation and Normalization.Ryo Takemura - 2013 - Studia Logica 101 (1):157-191.
    Proof-theoretical notions and techniques, developed on the basis of sentential/symbolic representations of formal proofs, are applied to Euler diagrams. A translation of an Euler diagrammatic system into a natural deduction system is given, and the soundness and faithfulness of the translation are proved. Some consequences of the translation are discussed in view of the notion of free ride, which is mainly discussed in the literature of cognitive science as an account of inferential efficacy of diagrams. The translation enables us (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  18.  73
    Proof theory and constructive mathematics.Anne S. Troelstra - 1977 - In Jon Barwise (ed.), Handbook of mathematical logic. New York: North-Holland. pp. 973--1052.
  19.  55
    Proof Theory for Positive Logic with Weak Negation.Marta Bílková & Almudena Colacito - 2020 - Studia Logica 108 (4):649-686.
    Proof-theoretic methods are developed for subsystems of Johansson’s logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  20.  6
    Proof theory and formal grammars: applications of normalization.Hans-Jörg Tiede - 2003 - In Benedikt Löwe, Thoralf Räsch & Wolfgang Malzkorn (eds.), Foundations of the Formal Sciences II. Kluwer Academic Publishers. pp. 235--256.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  21.  37
    Intuitionism and proof theory.A. Kino, John Myhill & Richard Eugene Vesley (eds.) - 1970 - Amsterdam,: North-Holland Pub. Co..
    Our first aim is to make the study of informal notions of proof plausible. Put differently, since the raison d'étre of anything like existing proof theory seems to rest on such notions, the aim is nothing else but to make a case for proof theory; ...
    Direct download  
     
    Export citation  
     
    Bookmark   8 citations  
  22.  35
    Proof theory of weak compactness.Toshiyasu Arai - 2013 - Journal of Mathematical Logic 13 (1):1350003.
    We show that the existence of a weakly compact cardinal over the Zermelo–Fraenkel's set theory ZF is proof-theoretically reducible to iterations of Mostowski collapsings and Mahlo operations.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  23.  23
    Proof theory and computer programming.Ruy J. G. B. de Queiroz & Thomas S. E. Maibaum - 1990 - Mathematical Logic Quarterly 36 (5):389-414.
  24.  34
    Proof theory and computer programming.Ruy J. G. B. de Queiroz & Thomas S. E. Maibaum - 1990 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 36 (5):389-414.
  25. Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
     
    Export citation  
     
    Bookmark   166 citations  
  26. Proof theory in philosophy of mathematics.Andrew Arana - 2010 - Philosophy Compass 5 (4):336-347.
    A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  27. Stoic Sequent Logic and Proof Theory.Susanne Bobzien - 2019 - History and Philosophy of Logic 40 (3):234-265.
    This paper contends that Stoic logic (i.e. Stoic analysis) deserves more attention from contemporary logicians. It sets out how, compared with contemporary propositional calculi, Stoic analysis is closest to methods of backward proof search for Gentzen-inspired substructural sequent logics, as they have been developed in logic programming and structural proof theory, and produces its proof search calculus in tree form. It shows how multiple similarities to Gentzen sequent systems combine with intriguing dissimilarities that may enrich contemporary (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  28.  34
    Proof Theory of Paraconsistent Weak Kleene Logic.Francesco Paoli & Michele Pra Baldi - 2020 - Studia Logica 108 (4):779-802.
    Paraconsistent Weak Kleene Logic is the 3-valued propositional logic defined on the weak Kleene tables and with two designated values. Most of the existing proof systems for PWK are characterised by the presence of linguistic restrictions on some of their rules. This feature can be seen as a shortcoming. We provide a cut-free calculus for PWK that is devoid of such provisos. Moreover, we introduce a Priest-style tableaux calculus for PWK.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  29.  4
    Proof Theory.Jeremy Avigad - 2012 - In Sven Ove Hansson & Vincent F. Hendricks (eds.), Introduction to Formal Philosophy. Cham: Springer. pp. 177-190.
    Proof theory began in the 1920s as a part of Hilbert’s program, which aimed to secure the foundations of mathematics by modeling infinitary mathematics with formal axiomatic systems and proving those systems consistent using restricted, finitary means. The program thus viewed mathematics as a system of reasoning with precise linguistic norms, governed by rules that can be described and studied in concrete terms. Today such a viewpoint has applications in mathematics, computer science, and the philosophy of mathematics.
    Direct download  
     
    Export citation  
     
    Bookmark  
  30.  15
    Combinators, 2-terms and proof theory.Sören Stenlund - 1972 - Dordrecht,: D. Reidel.
    The main aim of Schonfinkel's paper was methodological: to reduce the primitive logical notions to as few and definite notions as possible. ...
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  31.  14
    Proof theory for theories of ordinals II:< i> Π_< sub> 3-reflection.Toshiyasu Arai - 2004 - Annals of Pure and Applied Logic 129 (1):39-92.
  32.  78
    An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs.Paolo Mancosu, Sergio Galvan & Richard Zach - 2021 - Oxford: Oxford University Press. Edited by Sergio Galvan & Richard Zach.
    An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details of proofs worked out and examples and exercises to aid the reader's understanding. It also serves as a companion to reading the original pathbreaking articles by Gerhard Gentzen. The first half covers topics in structural proof theory, including the Gödel-Gentzen translation of classical into intuitionistic logic, natural deduction and the normalization theorems, the sequent calculus, including cut-elimination and mid-sequent theorems, (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  33. Proof Theory for Modal Logic.Sara Negri - 2011 - Philosophy Compass 6 (8):523-538.
    The axiomatic presentation of modal systems and the standard formulations of natural deduction and sequent calculus for modal logic are reviewed, together with the difficulties that emerge with these approaches. Generalizations of standard proof systems are then presented. These include, among others, display calculi, hypersequents, and labelled systems, with the latter surveyed from a closer perspective.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   21 citations  
  34.  50
    Proof Theory.Wilfried Sieg - unknown
  35. Proof Theory For Finitely Valid Sentences.J. Degen - 2001 - Reports on Mathematical Logic:47-59.
    We investigate infinitary sequent calculi which generate the finitely valid sentences of first-order logic, of simple type theory and of transitive closure logic, respectively.
     
    Export citation  
     
    Bookmark  
  36.  43
    Proof theory in the abstract.J. M. E. Hyland - 2002 - Annals of Pure and Applied Logic 114 (1-3):43-78.
    Categorical proof theory is an approach to understanding the structure of proofs. We illustrate the idea first by analyzing G0̈del's Dialectica interpretation and the Diller-Nahm variant in categorical terms. Then we consider the problematic question of the structure of classical proofs. We show how double negation translations apply in the case of the Dialectica interpretations. Finally we formulate a proposal as to how to give a more faithful analysis of proofs in the sequent calculus.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  37.  18
    Lifting proof theory to the countable ordinals: Zermelo-Fraenkel set theory.Toshiyasu Arai - 2014 - Journal of Symbolic Logic 79 (2):325-354.
  38.  54
    Proof Theory for Functional Modal Logic.Shawn Standefer - 2018 - Studia Logica 106 (1):49-84.
    We present some proof-theoretic results for the normal modal logic whose characteristic axiom is \. We present a sequent system for this logic and a hypersequent system for its first-order form and show that these are equivalent to Hilbert-style axiomatizations. We show that the question of validity for these logics reduces to that of classical tautologyhood and first-order logical truth, respectively. We close by proving equivalences with a Fitch-style proof system for revision theory.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  39.  87
    Algebraic proof theory for substructural logics: cut-elimination and completions.Agata Ciabattoni, Nikolaos Galatos & Kazushige Terui - 2012 - Annals of Pure and Applied Logic 163 (3):266-290.
  40.  61
    Proof theory for admissible rules.Rosalie Iemhoff & George Metcalfe - 2009 - Annals of Pure and Applied Logic 159 (1-2):171-186.
    Admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In this paper, a Gentzen-style framework is introduced for analytic proof systems that derive admissible rules of non-classical logics. While Gentzen systems for derivability treat sequents as basic objects, for admissibility, the basic objects are sequent rules. Proof systems are defined here for admissible rules of classes of modal logics, including K4, S4, and GL, and also Intuitionistic Logic IPC. (...)
    Direct download (9 more)  
     
    Export citation  
     
    Bookmark   27 citations  
  41.  54
    General Proof Theory: Introduction.Thomas Piecha & Peter Schroeder-Heister - 2019 - Studia Logica 107 (1):1-5.
    This special issue on general proof theory collects papers resulting from the conference on general proof theory held in November 2015 in Tübingen.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  42. Proof theory of iterated inductive definitions revisited.W. Buchholz - forthcoming - Archive for Mathematical Logic.
     
    Export citation  
     
    Bookmark   1 citation  
  43. Takeuti's proof theory in the context of the Kyoto School.Andrew Arana - 2019 - Jahrbuch Für Philosophie Das Tetsugaku-Ronso 46:1-17.
    Gaisi Takeuti (1926–2017) is one of the most distinguished logicians in proof theory after Hilbert and Gentzen. He extensively extended Hilbert's program in the sense that he formulated Gentzen's sequent calculus, conjectured that cut-elimination holds for it (Takeuti's conjecture), and obtained several stunning results in the 1950–60s towards the solution of his conjecture. Though he has been known chiefly as a great mathematician, he wrote many papers in English and Japanese where he expressed his philosophical thoughts. In particular, (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  44.  51
    Proof theory for quantified monotone modal logics.Sara Negri & Eugenio Orlandelli - 2019 - Logic Journal of the IGPL 27 (4):478-506.
    This paper provides a proof-theoretic study of quantified non-normal modal logics. It introduces labelled sequent calculi based on neighbourhood semantics for the first-order extension, with both varying and constant domains, of monotone NNML, and studies the role of the Barcan formulas in these calculi. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown that each of the calculi (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  45.  20
    Proof Theory of First Order Abduction: Sequent Calculus and Structural Rules.Seyed Ahmad Mirsanei - 2021 - Eighth Annual Conference of Iranian Association for Logic (Ial).
    The logical formalism of abductive reasoning is still an open discussion and various theories have been presented about it. Abduction is a type of non-monotonic and defeasible reasonings, and the logic containing such a reasoning is one of the types of non-nonmonotonic and defeasible logics, such as inductive logic. Abduction is a kind of natural reasoning and it is a solution to the problems having this form "the phenomenon of φ cannot be explained by the theory of Θ" and (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  46.  45
    Proof Theory and Logical Complexity.Helmut Pfeifer & Jean-Yves Girard - 1989 - Journal of Symbolic Logic 54 (4):1493.
  47.  21
    Proof Theory for Fuzzy Logics.George Metcalfe, Nicola Olivetti & Dov M. Gabbay - 2008 - Dordrecht, Netherland: Springer.
    Fuzzy logics are many-valued logics that are well suited to reasoning in the context of vagueness. They provide the basis for the wider field of Fuzzy Logic, encompassing diverse areas such as fuzzy control, fuzzy databases, and fuzzy mathematics. This book provides an accessible and up-to-date introduction to this fast-growing and increasingly popular area. It focuses in particular on the development and applications of "proof-theoretic" presentations of fuzzy logics; the result of more than ten years of intensive work by (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  48.  39
    Pure proof theory aims, methods and results.Wolfram Pohlers - 1996 - Bulletin of Symbolic Logic 2 (2):159-188.
    Apologies. The purpose of the following talk is to give an overview of the present state of aims, methods and results in Pure Proof Theory. Shortage of time forces me to concentrate on my very personal views. This entails that I will emphasize the work which I know best, i.e., work that has been done in the triangle Stanford, Munich and Münster. I am of course well aware that there are as important results coming from outside this triangle (...)
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  49. Proof theory and set theory.Gaisi Takeuti - 1985 - Synthese 62 (2):255 - 263.
    The foundations of mathematics are divided into proof theory and set theory. Proof theory tries to justify the world of infinite mind from the standpoint of finite mind. Set theory tries to know more and more of the world of the infinite mind. The development of two subjects are discussed including a new proof of the accessibility of ordinal diagrams. Finally the world of large cardinals appears when we go slightly beyond girard's categorical (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  50.  91
    Proof theory in the USSR 1925–1969.Grigori Mints - 1991 - Journal of Symbolic Logic 56 (2):385-424.
    We present a survey of proof theory in the USSR beginning with the paper by Kolmogorov [1925] and ending (mostly) in 1969; the last two sections deal with work done by A. A. Markov and N. A. Shanin in the early seventies, providing a kind of effective interpretation of negative arithmetic formulas. The material is arranged in chronological order and subdivided according to topics of investigation. The exposition is more detailed when the work is little known in the (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   6 citations  
1 — 50 / 1000