Results for 'Proof theory'

1000+ found
Order:
See also
  1.  90
    Basic Proof Theory.A. S. Troelstra - 2000 - Cambridge University Press.
    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   139 citations  
  2.  75
    Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - Cambridge University Press.
    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   99 citations  
  3.  2
    Proof Theory.Gaisi Takeuti - 1975 - Elsevier.
  4.  1
    Proof Theory.K. Schütte - 1977 - Springer Verlag.
  5. 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   13 citations  
  6. Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
     
    Export citation  
     
    Bookmark   146 citations  
  7.  32
    Proof Theory and Logical Complexity. [REVIEW]Helmut Pfeifer - 1991 - Annals of Pure and Applied Logic 53 (4):197.
    Direct download  
     
    Export citation  
     
    Bookmark   39 citations  
  8.  61
    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  
  9. Structural Proof Theory[REVIEW]Harold T. Hodes - 2006 - Philosophical Review 115 (2):255-258.
  10.  14
    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)  
    Translate
     
     
    Export citation  
     
    Bookmark   7 citations  
  11.  21
    Basic Proof Theory.Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280-280.
  12. 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 (2 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  13.  35
    Proof Theory of Modal Logic.Heinrich Wansing (ed.) - 1996 - Dordrecht, Netherland: 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  
  14.  38
    Handbook of Proof Theory.Samuel R. Buss (ed.) - 1998 - 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   31 citations  
  15.  27
    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 (10 more)  
     
    Export citation  
     
    Bookmark   25 citations  
  16.  63
    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.
  17.  16
    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   35 citations  
  18.  4
    On the Proof Theory of Infinitary Modal Logic.Matteo Tesi - forthcoming - Studia Logica:1-32.
    The article deals with infinitary modal logic. We first discuss the difficulties related to the development of a satisfactory proof theory and then we show how to overcome these problems by introducing a labelled sequent calculus which is sound and complete with respect to Kripke semantics. We establish the structural properties of the system, namely admissibility of the structural rules and of the cut rule. Finally, we show how to embed common knowledge in the infinitary calculus and we (...)
    Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  19.  37
    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   3 citations  
  20.  38
    Proof Theory and Logical Complexity.Helmut Pfeifer & Jean-Yves Girard - 1989 - Journal of Symbolic Logic 54 (4):1493.
  21.  40
    Proof Theory.Wilfried Sieg - unknown
  22.  34
    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  
  23.  14
    On the Proof Theory of Type Two Functionals Based on Primitive Recursive Operations.David Steiner & Thomas Strahm - 2006 - Mathematical Logic Quarterly 52 (3):237-252.
    This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of the (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  24.  27
    Proof Theory of Paraconsistent Quantum Logic.Norihiro Kamide - 2018 - Journal of Philosophical Logic 47 (2):301-324.
    Paraconsistent quantum logic, a hybrid of minimal quantum logic and paraconsistent four-valued logic, is introduced as Gentzen-type sequent calculi, and the cut-elimination theorems for these calculi are proved. This logic is shown to be decidable through the use of these calculi. A first-order extension of this logic is also shown to be decidable. The relationship between minimal quantum logic and paraconsistent four-valued logic is clarified, and a survey of existing Gentzen-type sequent calculi for these logics and their close relatives is (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  25.  1
    Proof Theory and Intuitionistic Systems.Bruno Scarpellini - 1971 - New York: Springer Verlag.
  26.  26
    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   2 citations  
  27.  13
    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  
  28.  19
    Algebraic Proof Theory: Hypersequents and Hypercompletions.Agata Ciabattoni, Nikolaos Galatos & Kazushige Terui - 2017 - Annals of Pure and Applied Logic 168 (3):693-737.
  29.  93
    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   6 citations  
  30.  10
    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  
  31. Proof Theory and Meaning.B. G. Sundholm - unknown
    Translate
     
     
    Export citation  
     
    Bookmark   20 citations  
  32.  27
    Proof Theory and Ordinal Analysis.W. Pohlers - 1991 - Archive for Mathematical Logic 30 (5-6):311-376.
    In the first part we show why ordinals and ordinal notations are naturally connected with proof theoretical research. We introduce the program of ordinal analysis. The second part gives examples of applications of ordinal analysis.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  33.  43
    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   1 citation  
  34.  1
    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   6 citations  
  35.  21
    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   5 citations  
  36. 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   3 citations  
  37.  41
    Semantics and Proof Theory of the Epsilon Calculus.Richard Zach - 2017 - In Sujata Ghosh & Sanjiva Prasad (eds.), Logic and Its Applications. ICLA 2017. Berlin, Heidelberg: Springer. pp. 27-47.
    The epsilon operator is a term-forming operator which replaces quantifiers in ordinary predicate logic. The application of this undervalued formalism has been hampered by the absence of well-behaved proof systems on the one hand, and accessible presentations of its theory on the other. One significant early result for the original axiomatic proof system for the epsilon-calculus is the first epsilon theorem, for which a proof is sketched. The system itself is discussed, also relative to possible semantic (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  38.  1
    Hybrid Logic and its Proof-Theory.Torben Braüner - 2010 - Dordrecht and New York: Springer.
    This is the first book-length treatment of hybrid logic and its proof-theory. Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a model. This is useful for many applications, for example when reasoning about time one often wants to formulate a series of statements about what happens at specific times. There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  39.  25
    Structural Proof Theory for First-Order Weak Kleene Logics.Andreas Fjellstad - 2020 - Journal of Applied Non-Classical Logics 30 (3):272-289.
    This paper presents a sound and complete five-sided sequent calculus for first-order weak Kleene valuations which permits not only elegant representations of four logics definable on first-order weak Kleene valuations, but also admissibility of five cut rules by proof analysis.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  40.  27
    Proof Theory: A Selection of Papers From the Leeds Proof Theory Programme 1990.Peter Aczel, Harold Simmons & Stanley S. Wainer (eds.) - 1992 - 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  
  41. Logical Consequence, Proof Theory, and Model Theory.Stewart Shapiro - 2005 - In Oxford Handbook of Philosophy of Mathematics and Logic. Oxford University Press. pp. 651--670.
    This chapter provides broad coverage of the notion of logical consequence, exploring its modal, semantic, and epistemic aspects. It develops the contrast between proof-theoretic notion of consequence, in terms of deduction, and a model-theoretic approach, in terms of truth-conditions. The main purpose is to relate the formal, technical work in logic to the philosophical concepts that underlie reasoning.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   47 citations  
  42.  44
    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   5 citations  
  43.  40
    Proof Theory and Semantics for a Theory of Definite Descriptions.Nils Kürbis - 2021 - In Anupam Das & Sara Negri (eds.), TABLEAUX 2021, LNAI 12842.
    This paper presents a sequent calculus and a dual domain semantics for a theory of definite descriptions in which these expressions are formalised in the context of complete sentences by a binary quantifier I. I forms a formula from two formulas. Ix[F, G] means ‘The F is G’. This approach has the advantage of incorporating scope distinctions directly into the notation. Cut elimination is proved for a system of classical positive free logic with I and it is shown to (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  44.  67
    Proof Theory of Epistemic Logic of Programs.Paolo Maffezioli & Alberto Naibo - 2014 - Logic and Logical Philosophy 23 (3):301--328.
    A combination of epistemic logic and dynamic logic of programs is presented. Although rich enough to formalize some simple game-theoretic scenarios, its axiomatization is problematic as it leads to the paradoxical conclusion that agents are omniscient. A cut-free labelled Gentzen-style proof system is then introduced where knowledge and action, as well as their combinations, are formulated as rules of inference, rather than axioms. This provides a logical framework for reasoning about games in a modular and systematic way, and to (...)
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  45.  27
    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 (7 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  46.  52
    Proof Theory and Constructive Mathematics.Anne S. Troelstra - 1977 - In Jon Barwise & H. Jerome Keisler (eds.), Handbook of Mathematical Logic. North-Holland Pub. Co.. pp. 973--1052.
  47. Truth Values and Proof Theory.Greg Restall - 2009 - Studia Logica 92 (2):241-264.
    I present an account of truth values for classical logic, intuitionistic logic, and the modal logic S5, in which truth values are not a fundamental category from which the logic is defined, but rather, an idealisation of more fundamental logical features in the proof theory for each system. The result is not a new set of semantic structures, but a new understanding of how the existing semantic structures may be understood in terms of a more fundamental notion of (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   18 citations  
  48.  24
    Proof Theories for Some Prioritized Consequence Relations.Liza Verhoeven - 2003 - Logique Et Analyse 183 (184):325-344.
  49.  35
    Proof Theories for Semilattice Logics.Steve Giambrone & Alasdaire Urquhart - 1987 - Mathematical Logic Quarterly 33 (5):433-439.
  50.  68
    A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
    The lambdaPi-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the lambdaPi-calculus and prove the cut-elimination theorem. The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 1000