Related categories

2522 found
Order:
1 — 50 / 2522
  1. added 2020-06-03
    Uniform Interpolation and the Existence of Sequent Calculi.Rosalie Iemhoff - 2019 - Annals of Pure and Applied Logic 170 (11):102711.
  2. added 2020-05-26
    Natural Formalization: Deriving the Cantor-Bernstein Theorem in Zf.Wilfried Sieg & Patrick Walsh - forthcoming - Review of Symbolic Logic:1-44.
    Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3. added 2020-05-26
    Proof Theory of Paraconsistent Weak Kleene Logic.Francesco Paoli & Michele Pra Baldi - forthcoming - Studia Logica:1-24.
    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.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  4. added 2020-05-25
    Herzberger’s Limit Rule with Labelled Sequent Calculus.Andreas Fjellstad - forthcoming - Studia Logica:1-41.
    Inspired by recent work on proof theory for modal logic, this paper develops a cut-free labelled sequent calculus obtained by imitating Herzberger’s limit rule for revision sequences as a clause in a possible world semantics. With the help of two completeness theorems, one between the labelled sequent calculus and the corresponding possible world semantics, and one between the axiomatic theory of truth PosFS and a neighbourhood semantics, together with the proof of the equivalence between the two semantics, we show that (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  5. added 2020-05-25
    A Proof Theory for the Logic of Provability in True Arithmetic.Hirohiko Kushida - forthcoming - Studia Logica:1-19.
    In a classical 1976 paper, Solovay proved the arithmetical completeness of the modal logic GL; provability of a formula in GL coincides with provability of its arithmetical interpretations of it in Peano Arithmetic. In that paper, he also provided an axiomatic system GLS and proved arithmetical completeness for GLS; provability of a formula in GLS coincides with truth of its arithmetical interpretations in the standard model of arithmetic. Proof theory for GL has been studied intensively up to the present day. (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  6. added 2020-05-25
    Reasoning Continuously: A Formal Construction of Continuous Proofs.T. D. P. Brunet & E. Fisher - forthcoming - Studia Logica:1-16.
    We begin with the idea that lines of reasoning are continuous mental processes and develop a notion of continuity in proof. This requires abstracting the notion of a proof as a set of sentences ordered by provability. We can then distinguish between discrete steps of a proof and possibly continuous stages, defining indexing functions to pick these out. Proof stages can be associated with the application of continuously variable rules, connecting continuity in lines of reasoning with continuously variable reasons. Some (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  7. added 2020-05-25
    A Parametric, Resource-Bounded Generalization of Löb’s Theorem, and a Robust Cooperation Criterion for Open-Source Game Theory.Andrew Critch - 2019 - Journal of Symbolic Logic 84 (4):1368-1381.
    This article presents two theorems: a generalization of Löb’s Theorem that applies to formal proof systems operating with bounded computational resources, such as formal verification software or theorem provers, and a theorem on the robust cooperation of agents that employ proofs about one another’s source code as unexploitable criteria for cooperation. The latter illustrates a capacity for outperforming classical Nash equilibria and correlated equilibria, attaining mutually cooperative program equilibrium in the Prisoner’s Dilemma while remaining unexploitable, i.e., sometimes achieving the outcome, (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  8. added 2020-05-22
    Expander Construction in VNC1.Sam Buss, Valentine Kabanets, Antonina Kolokolova & Michal Koucký - 2020 - Annals of Pure and Applied Logic 171 (7):102796.
    We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [44], and show that this analysis can be formalized in the bounded arithmetic system VNC^1 (corresponding to the “NC^1 reasoning”). As a corollary, we prove the assumption made by Jeřábek [28] that a construction of certain bipartite expander graphs can be formalized in VNC^1 . This in turn implies that every proof in Gentzen's sequent calculus LK of a (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  9. added 2020-05-22
    Modal Extension of Ideal Paraconsistent Four-Valued Logic and its Subsystem.Norihiro Kamide & Yoni Zohar - 2020 - Annals of Pure and Applied Logic 171 (10):102830.
    This study aims to introduce a modal extension M4CC of Arieli, Avron, and Zamansky's ideal paraconsistent four-valued logic 4CC as a Gentzen-type sequent calculus and prove the Kripke-completeness and cut-elimination theorems for M4CC. The logic M4CC is also shown to be decidable and embeddable into the normal modal logic S4. Furthermore, a subsystem of M4CC, which has some characteristic properties that do not hold for M4CC, is introduced and the Kripke-completeness and cut-elimination theorems for this subsystem are proved. This subsystem (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  10. added 2020-05-19
    Motivated Proofs: What They Are, Why They Matter and How to Write Them.Rebecca Lea Morris - 2020 - Review of Symbolic Logic 13 (1):23-46.
    Mathematicians judge proofs to possess, or lack, a variety of different qualities, including, for example, explanatory power, depth, purity, beauty and fit. Philosophers of mathematical practice have begun to investigate the nature of such qualities. However, mathematicians frequently draw attention to another desirable proof quality: being motivated. Intuitively, motivated proofs contain no "puzzling" steps, but they have received little further analysis. In this paper, I begin a philosophical investigation into motivated proofs. I suggest that a proof is motivated if and (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  11. added 2020-05-16
    Essential Structure of Proofs as a Measure of Complexity.Jaime Ramos, João Rasga & Cristina Sernadas - 2020 - Logica Universalis 14 (2):209-242.
    The essential structure of proofs is proposed as the basis for a measure of complexity of formulas in FOL. The motivating idea was the recognition that distinct theorems can have the same derivation modulo some non essential details. Hence the difficulty in proving them is identical and so their complexity should be the same. We propose a notion of complexity of formulas capturing this property. With this purpose, we introduce the notions of schema calculus, schema derivation and description complexity of (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  12. added 2020-05-15
    Plans and Planning in Mathematical Proofs.Yacin Hamami & Rebecca Morris - forthcoming - Review of Symbolic Logic.
    In practice, mathematical proofs are most often the result of careful planning by the agents who produced them. As a consequence, each mathematical proof inherits a plan in virtue of the way it is produced, a plan which underlies its “architecture” or “unity”. This paper provides an account of plans and planning in the context of mathematical proofs. The approach adopted here consists in looking for these notions not in mathematical proofs themselves, but in the agents who produced them. The (...)
    Remove from this list  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  13. added 2020-05-15
    Herbrand's Theorem as Higher Order Recursion.Bahareh Afshari, Stefan Hetzl & Graham E. Leigh - 2020 - Annals of Pure and Applied Logic 171 (6):102792.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  14. added 2020-05-11
    The Large Structures of Grothendieck Founded on Finite-Order Arithmetic.Colin Mclarty - 2020 - Review of Symbolic Logic 13 (2):296-325.
    The large-structure tools of cohomology including toposes and derived categories stay close to arithmetic in practice, yet published foundations for them go beyond ZFC in logical strength. We reduce the gap by founding all the theorems of Grothendieck’s SGA, plus derived categories, at the level of Finite-Order Arithmetic, far below ZFC. This is the weakest possible foundation for the large-structure tools because one elementary topos of sets with infinity is already this strong.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  15. added 2020-05-11
    A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism.José Espírito Santo & Gilda Ferreira - 2020 - Studia Logica 108 (3):477-507.
    We study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity. As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  16. added 2020-05-11
    Gentzen’s 1935 Consistency Proof and the Interpretation of its Implication.Yuta Takahashi - 2018 - Proceedings of the XXIII World Congress of Philosophy 55:73-78.
    In this paper, I will argue from a historical perspective that Gentzen’s 1935 consistency proof of 1st order Peano Arithmetic PA principally aimed to give a finitist interpretation of implication and this aspect of the 1935 proof emerged as the attempt to cope with the non-finiteness in BHK-interpretation of implication. My argument consists of two parts. First, I will explain that the fundamental idea of the 1935 proof is to show the soundness of PA on some finitist interpretation and Gentzen (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  17. added 2020-05-11
    On the Classification of Natural Deduction Calculi.Andrzej Indrzejczak - 2018 - Proceedings of the XXIII World Congress of Philosophy 19:17-21.
    In 1934 Jaśkowski and Gentzen independently published their groundbreaking works on Natural Deduction. The aim of this paper is to provide some criteria for division of the diversity of existing systems on some natural subcategories and to show that despite the differences all these systems are descendants of original systems of Jaśkowski and Gentzen. Three criteria are discussed:The kind of items which are building-blocks of the proof.The format of proof.The kind of rules.The first leads to the division of ND into (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  18. added 2020-05-06
    Completeness and Cut-Elimination for First-Order Ideal Paraconsistent Four-Valued Logic.Norihiro Kamide & Yoni Zohar - 2020 - Studia Logica 108 (3):549-571.
    In this study, we prove the completeness and cut-elimination theorems for a first-order extension F4CC of Arieli, Avron, and Zamansky’s ideal paraconsistent four-valued logic known as 4CC. These theorems are proved using Schütte’s method, which can simultaneously prove completeness and cut-elimination.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  19. added 2020-04-19
    Kripke-Completeness and Cut-elimination Theorems for Intuitionistic Paradefinite Logics With and Without Quasi-Explosion.Norihiro Kamide - forthcoming - Journal of Philosophical Logic:1-28.
    Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems for (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  20. added 2020-04-10
    Grounding Rules and (Hyper-)Isomorphic Formulas.Francesca Poggiolesi - 2020 - Australasian Journal of Logic 17 (1):70.
    An oft-defended claim of a close relationship between Gentzen inference rules and the meaning of the connectives they introduce and eliminate has given rise to a whole domain called proof-theoretic semantics, see Schroeder- Heister ; Prawitz. A branch of proof-theoretic semantics, mainly developed by Dosen ; Dosen and Petric, isolates in a precise mathematical manner formulas that have the same meaning. These isomorphic formulas are defined to be those that behave identically in inferences. The aim of this paper is to (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  21. added 2020-04-01
    Local Reflection, Definable Elements and 1-Provability.Evgeny Kolmakov - forthcoming - Archive for Mathematical Logic:1-18.
    In this note we study several topics related to the schema of local reflection \\) and its partial and relativized variants. Firstly, we introduce the principle of uniform reflection with \-definable parameters, establish its relationship with relativized local reflection principles and corresponding versions of induction with definable parameters. Using this schema we give a new model-theoretic proof of the \-conservativity of uniform \-reflection over relativized local \-reflection. We also study the proof-theoretic strength of Feferman’s theorem, i.e., the assertion of 1-provability (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  22. added 2020-03-24
    Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems. 93413 Cham, Germany: Springer. pp. 202-218.
    This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  23. added 2020-03-24
    Cut-Free Calculi and Relational Semantics for Temporal STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In Francesco Calimeri, Nicola Leone & Marco Manna (eds.), Logics in Artificial Intelligence. Springer International Publishing. pp. 803 - 819.
    We present cut-free labelled sequent calculi for a central formalism in logics of agency: STIT logics with temporal operators. These include sequent systems for Ldm , Tstit and Xstit. All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi G3Ldm and G3Tstit are shown sound and complete relative to irreflexive temporal frames. Additionally, we extend current results by showing that also Xstit can be characterized through relational frames, omitting the use of BT+AC frames.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  24. added 2020-03-24
    From Display to Labelled Proofs for Tense Logics.Agata Ciabattoni, Tim Lyon & Revantha Ramanayake - 2018 - In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139.
    We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  25. added 2020-02-24
    Towards a More General Concept of Inference.Ivo Pezlar - 2014 - Logica Universalis 8 (1):61-81.
    The main objective of this paper is to sketch unifying conceptual and formal framework for inference that is able to explain various proof techniques without implicitly changing the underlying notion of inference rules. We base this framework upon the so-called two-dimensional, i.e., deduction to deduction, account of inference introduced by Tichý in his seminal work The Foundation’s of Frege’s Logic (1988). Consequently, it will be argued that sequent calculus provides suitable basis for such general concept of inference and therefore should (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  26. added 2020-02-12
    Basic Proof Theory.Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280-280.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   72 citations  
  27. added 2020-02-11
    Structural Proof Theory.Harold T. Hodes - 2006 - Philosophical Review 115 (2):255-258.
    Remove from this list   Direct download (6 more)  
     
    Export citation  
     
    Bookmark   56 citations  
  28. added 2020-02-11
    First Steps Into Metapredicativity in Explicit Mathematics.Andrea Cantini - 2002 - Bulletin of Symbolic Logic 8 (4):535-536.
  29. added 2020-02-09
    Deduction-Detachment Theorem and Gentzen-Style Deductive Systems.Sergey Babenyshev - 2018 - In Janusz Czelakowski (ed.), Don Pigozzi on Abstract Algebraic Logic, Universal Algebra, and Computer Science. Springer Verlag.
    Logical implication is an attempt to catch the essence of causeeffect relationships of the real world in the context of formal deductive systems. The Deduction-Detachment Theorem being, in its turn, a statement about essential logical properties of classical implication, was therefore of great interest for logicians. Although a statement about a Hilbert-style deductive system, DDT can be formulated by means of Gentzen-style rules, and as such seems to be a statement about the metatheoretical properties of Hilbert-style deductive systems. As is (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  30. added 2020-02-05
    Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic Via Nested Sequents.Tim Lyon, Alwen Tiu, Rajeev Gore & Ranald Clouston - 2020 - In Maribel Fernandez & Anca Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Dagstuhl, Germany: pp. 1-16.
    We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  31. added 2020-02-05
    Atomic Ontology.Andrew Parisi - 2020 - Synthese 197 (1):355-379.
    The aim of this article is to offer a method for determining the ontological commitments of a formalized theory. The second section shows that determining the consequence relation of a language model-theoretically entails that the ontology of a theory is tied very closely to the variables that feature in that theory. The third section develops an alternative way of determining the ontological commitments of a theory given a proof-theoretic account of the consequence relation for the language that theory is in. (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  32. added 2020-02-05
    Reinhard Kahle and Michael Rathjen : Gentzen’s Centenary. The Quest for Consistency: Springer, Berlin, Heidelberg Et Al., 2015, 561 Pp, Softcover $109.99, ISBN: 9783319101033. [REVIEW]David Binder - 2018 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 49 (3):475-479.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  33. added 2020-02-05
    The Strength of Countable Saturation.Benno van den Berg, Eyvind Briseid & Pavol Safarik - 2017 - Archive for Mathematical Logic 56 (5-6):699-711.
    In earlier work we introduced two systems for nonstandard analysis, one based on classical and one based on intuitionistic logic; these systems were conservative extensions of first-order Peano and Heyting arithmetic, respectively. In this paper we study how adding the principle of countable saturation to these systems affects their proof-theoretic strength. We will show that adding countable saturation to our intuitionistic system does not increase its proof-theoretic strength, while adding it to the classical system increases the strength from first- to (...)
    Remove from this list   Direct download (8 more)  
     
    Export citation  
     
    Bookmark  
  34. added 2020-02-05
    Anti-Realistic Notions of Truth.Luca Tranchini - 2012 - Topoi 31 (1):5-8.
    Validity, the central concept of the so-called ‘proof-theoretic semantics’ is described as correctly applying to the arguments that denote proofs. In terms of validity, I propose an anti-realist characterization of the notions of truth and correct assertion, at the core of which is the idea that valid arguments may fail to be recognized as such. The proposed account is compared with Dummett’s and Prawitz’s views on the matter.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  35. added 2020-02-03
    A Generalized Proof-Theoretic Approach to Logical Argumentation Based on Hypersequents.AnneMarie Borg, Christian Straßer & Ofer Arieli - forthcoming - Studia Logica:1-72.
    In this paper we introduce hypersequent-based frameworks for the modelling of defeasible reasoning by means of logic-based argumentation and the induced entailment relations. These structures are an extension of sequent-based argumentation frameworks, in which arguments and the attack relations among them are expressed not only by Gentzen-style sequents, but by more general expressions, called hypersequents. This generalization allows us to overcome some of the known weaknesses of logical argumentation frameworks and to prove several desirable properties of the entailments that are (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  36. added 2020-02-03
    Reasoning with Maximal Consistency by Argumentative Approaches.Ofer Arieli, AnneMarie Borg & Christian Straßer - 2018 - Journal of Logic and Computation 28 (7):1523--1563.
    Reasoning with the maximally consistent subsets of the premises is a well-known approach for handling contradictory information. In this paper we consider several variations of this kind of reasoning, for each one we introduce two complementary computational methods that are based on logical argumentation theory. The difference between the two approaches is in their ways of making consequences: one approach is of a declarative nature and is related to Dung-style semantics for abstract argumentation, while the other approach has a more (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  37. added 2020-02-03
    Towards the Proof-Theoretic Unification of Dung’s Argumentation Framework: An Adaptive Logic Approach.Christian Straßer & D. Seselja - 2010 - Journal of Logic and Computation 21 (2):133–156.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  38. added 2020-01-31
    Completeness of the primitive recursive $$omega $$-rule.Emanuele Frittaion - forthcoming - Archive for Mathematical Logic:1-17.
    Shoenfield’s completeness theorem states that every true first order arithmetical sentence has a recursive \-proof encodable by using recursive applications of the \-rule. For a suitable encoding of Gentzen style \-proofs, we show that Shoenfield’s completeness theorem applies to cut free \-proofs encodable by using primitive recursive applications of the \-rule. We also show that the set of codes of \-proofs, whether it is based on recursive or primitive recursive applications of the \-rule, is \ complete. The same \ completeness (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  39. added 2020-01-23
    Short Proofs for Slow Consistency.Anton Freund & Fedor Pakhomov - 2020 - Notre Dame Journal of Formal Logic 61 (1):31-49.
    Let Con↾x denote the finite consistency statement “there are no proofs of contradiction in T with ≤x symbols.” For a large class of natural theories T, Pudlák has shown that the lengths of the shortest proofs of Con↾n in the theory T itself are bounded by a polynomial in n. At the same time he conjectures that T does not have polynomial proofs of the finite consistency statements Con)↾n. In contrast, we show that Peano arithmetic has polynomial proofs of Con)↾n, (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  40. added 2020-01-14
    The Significance of the Curry-Howard Isomorphism.Zach Richard - 2019 - In Gabriele M. Mras, Paul Weingartner & Bernhard Ritter (eds.), Philosophy of Logic and Mathematics. Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin: De Gruyter. pp. 313-326.
    The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  41. added 2020-01-04
    Subminimal Logics in Light of Vakarelov’s Logic.Satoru Niki - forthcoming - Studia Logica:1-21.
    We investigate a subsystem of minimal logic related to D. Vakarelov’s logic \, using the framework of subminimal logics by A. Colacito, D. de Jongh and A. L. Vargas. In the course of it, the relationship between the two semantics in the respective frameworks is clarified. In addition, we introduce a sequent calculus for the investigated subsystem, and some proof-theoretic properties are established. Lastly, we formulate a new infinite class of subsystems of minimal logics.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42. added 2019-12-29
    The Power of Naive Truth.Hartry Field - manuscript
    While non-classical theories of truth that take truth to be transparent have some obvious advantages over any classical theory that evidently must take it as non-transparent, several authors have recently argued that there's also a big disadvantage of non-classical theories as compared to their “external” classical counterparts: proof-theoretic strength. While conceding the relevance of this, the paper argues that there is a natural way to beef up extant internal theories so as to remove their proof-theoretic disadvantage. It is suggested that (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  43. added 2019-12-29
    Subminimal Logics in Light of Vakarelov’s Logic.Satoru Niki - forthcoming - Studia Logica:1-21.
    We investigate a subsystem of minimal logic related to D. Vakarelov’s logic \, using the framework of subminimal logics by A. Colacito, D. de Jongh and A. L. Vargas. In the course of it, the relationship between the two semantics in the respective frameworks is clarified. In addition, we introduce a sequent calculus for the investigated subsystem, and some proof-theoretic properties are established. Lastly, we formulate a new infinite class of subsystems of minimal logics.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  44. added 2019-12-29
    On Deriving Nested Calculi for Intuitionistic Logics From Semantic Systems.Tim Lyon - 2020 - In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science. Cham: pp. 177-194.
    This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  45. added 2019-12-29
    Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic Via Linear Nested Sequents.Tim Lyon - 2020 - In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science. Cham: pp. 156-176.
    This paper employs the linear nested sequent framework to design a new cut-free calculus (LNIF) for intuitionistic fuzzy logic---the first-order Goedel logic characterized by linear relational frames with constant domains. Linear nested sequents---which are nested sequents restricted to linear structures---prove to be a well-suited proof-theoretic formalism for intuitionistic fuzzy logic. We show that the calculus LNIF possesses highly desirable proof-theoretic properties such as invertibility of all rules, admissibility of structural rules, and syntactic cut-elimination.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  46. added 2019-12-21
    Are the Open-Ended Rules for Negation Categorical?Constantin C. Brîncuș - forthcoming - Synthese:1-8.
    Vann McGee has recently argued that Belnap’s criteria constrain the formal rules of classical natural deduction to uniquely determine the semantic values of the propositional logical connectives and quantifiers if the rules are taken to be open-ended, i.e., if they are truth-preserving within any mathematically possible extension of the original language. The main assumption of his argument is that for any class of models there is a mathematically possible language in which there is a sentence true in just those models. (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  47. added 2019-12-21
    Translations Between Gentzen–Prawitz and Jaśkowski–Fitch Natural Deduction Proofs.Shawn Standefer - 2019 - Studia Logica 107 (6):1103-1134.
    Two common forms of natural deduction proof systems are found in the Gentzen–Prawitz and Jaśkowski–Fitch systems. In this paper, I provide translations between proofs in these systems, pointing out the ways in which the translations highlight the structural rules implicit in the systems. These translations work for classical, intuitionistic, and minimal logic. I then provide translations for classical S4 proofs.
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  48. added 2019-12-21
    The Fmla-Fmla Axiomatizations of the Exactly True and Non-falsity Logics and Some of Their Cousins.Yaroslav Shramko, Dmitry Zaitsev & Alexander Belikov - 2019 - Journal of Philosophical Logic 48 (5):787-808.
    In this paper we present a solution of the axiomatization problem for the Fmla-Fmla versions of the Pietz and Rivieccio exactly true logic and the non-falsity logic dual to it. To prove the completeness of the corresponding binary consequence systems we introduce a specific proof-theoretic formalism, which allows us to deal simultaneously with two consequence relations within one logical system. These relations are hierarchically organized, so that one of them is treated as the basic for the resulting logic, and the (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  49. added 2019-12-07
    A Note on Carnap’s Result and the Connectives.Tristan Haze - 2019 - Axiomathes 29 (3):285-288.
    Carnap’s result about classical proof-theories not ruling out non-normal valuations of propositional logic formulae has seen renewed philosophical interest in recent years. In this note I contribute some considerations which may be helpful in its philosophical assessment. I suggest a vantage point from which to see the way in which classical proof-theories do, at least to a considerable extent, encode the meanings of the connectives (not by determining a range of admissible valuations, but in their own way), and I demonstrate (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  50. added 2019-11-15
    Against the Unrestricted Applicability of Disjunction Elimination.Marcel Jahn - 2017 - Rerum Causae 9 (2):92-111.
    In this paper, I argue that the disjunction elimination rule presupposes the principle that a true disjunction contains at least one true disjunct. However, in some contexts such as supervaluationism or quantum logic, we have good reasons to reject this principle. Hence, disjunction elimination is restricted in at least one respect: it is not applicable to disjunctions for which this principle does not hold. The insight that disjunction elimination presupposes the principle that a true disjunction contains at least one true (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 2522