Related categories

2609 found
Order:
1 — 50 / 2609
  1. Some Proof Theoretical Remarks on Quantification in Ordinary Language.Michele Abrusci & Christian Retoré - manuscript
    This paper surveys the common approach to quantification and generalised quantification in formal linguistics and philosophy of language. We point out how this general setting departs from empirical linguistic data, and give some hints for a different view based on proof theory, which on many aspects gets closer to the language itself. We stress the importance of Hilbert's oper- ator epsilon and tau for, respectively, existential and universal quantifications. Indeed, these operators help a lot to construct semantic representation close to (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  2. Computational Reverse Mathematics and Foundational Analysis.Benedict Eastaugh - manuscript
    Reverse mathematics studies which subsystems of second order arithmetic are equivalent to key theorems of ordinary, non-set-theoretic mathematics. The main philosophical application of reverse mathematics proposed thus far is foundational analysis, which explores the limits of different foundations for mathematics in a formally precise manner. This paper gives a detailed account of the motivations and methodology of foundational analysis, which have heretofore been largely left implicit in the practice. It then shows how this account can be fruitfully applied in the (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  3. 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  
  4. Harmony, Normality and Stability.Nils Kurbis - manuscript
    The paper begins with a conceptual discussion of Michael Dummett's proof-theoretic justification of deduction or proof-theoretic semantics, which is based on what we might call Gentzen's thesis: 'the introductions constitute, so to speak, the "definitions" of the symbols concerned, and the eliminations are in the end only consequences thereof, which could be expressed thus: In the elimination of a symbol, the formula in question, whose outer symbol it concerns, may only "be used as that which it means on the basis (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  5. A Decision Procedure for Herbrand Formulas Without Skolemization.Timm Lampert - manuscript
    This paper describes a decision procedure for disjunctions of conjunctions of anti-prenex normal forms of pure first-order logic (FOLDNFs) that do not contain V within the scope of quantifiers. The disjuncts of these FOLDNFs are equivalent to prenex normal forms whose quantifier-free parts are conjunctions of atomic and negated atomic formulae (= Herbrand formulae). In contrast to the usual algorithms for Herbrand formulae, neither skolemization nor unification algorithms with function symbols are applied. Instead, a procedure is described that rests on (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  6. Cut Elimination for Systems of Transparent Truth with Restricted Initial Sequents.Carlo Nicolai - manuscript
    The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, we (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  7. Contradiction From a Coded Proof Predicate.T. Parent - manuscript
    Assuming that Q (Robinson arithmetic) is consistent and Church's Thesis is true, a coded proof predicate enables the derivation of a contradiction. Since Q is presumed to be consistent, this is regarded as a paradox to be resolved. The reasoning is somewhat similar to the reasoning behind Liar paradox, although the present argument requires only a syntactic notion of derivability in place of a semantic notion such as truth. Conceivably, the proof-theoretic Liar could be blocked by leaving the proof predicate (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  8. Contradiction From the Fixed Point Lemma.T. Parent - manuscript
    Assuming that Q (Robinson arithmetic) is consistent and Church's Thesis is true, the Fixed Point Lemma enables the derivation of a contradiction, in a manner akin to the v-Curry paradox. The derivation could be blocked by excluding certain formulae from the scope of the Lemma, but this would effectively concede that the unrestricted Lemma is false. The resolution of the paradox thus remains an open question.
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  9. Aristotle's Theory of the Assertoric Syllogism.Stephen Read - manuscript
    Although the theory of the assertoric syllogism was Aristotle's great invention, one which dominated logical theory for the succeeding two millenia, accounts of the syllogism evolved and changed over that time. Indeed, in the twentieth century, doctrines were attributed to Aristotle which lost sight of what Aristotle intended. One of these mistaken doctrines was the very form of the syllogism: that a syllogism consists of three propositions containing three terms arranged in four figures. Yet another was that a syllogism is (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  10. On the Notion of Validity for the Bilateral Classical Logic.Ukyo Suzuki & Yoriyuki Yamagata - manuscript
    This paper considers Rumfitt’s bilateral classical logic (BCL), which is proposed to counter Dummett’s challenge to classical logic. First, agreeing with several authors, we argue that Rumfitt’s notion of harmony, used to justify logical rules by a purely proof theoretical manner, is not sufficient to justify coordination rules in BCL purely proof-theoretically. For the central part of this paper, we propose a notion of proof-theoretical validity similar to Prawitz for BCL and proves that BCL is sound and complete respect to (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  11. Classical Modal Display Logic in the Calculus of Structures and Minimal Cut-Free Deep Inference Calculi for S.Rajeev Gore - manuscript
    Remove from this list  
     
    Export citation  
     
    Bookmark   2 citations  
  12. A Cut-Free Sequent Calculus for Bi-Intuitionistic Logic.Rajeev Gore - manuscript
  13. One-Pass Tableaux for Computation Tree Logic.Rajeev Gore - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  14. Proof Theory and Meaning: On Second Order Logic.Greg Restall - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  15. On Cut Elimination for Subsystems of Second-Order Number Theory.William Tait - manuscript
    To appear in the Proceedings of Logic Colloquium 2006. (32 pages).
    Remove from this list  
     
    Export citation  
     
    Bookmark  
  16. Proof Theory and Meaning: On Second Order Logic.Author unknown -
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  17. Natural Deduction and Semantic Models of Justification Logic in the Proof Assistant Coq.Jesús Mauricio Andrade Guzmán & Francisco Hernández Quiroz - forthcoming - Logic Journal of the IGPL.
    The purpose of this paper is to present a formalization of the language, semantics and axiomatization of justification logic in Coq. We present proofs in a natural deduction style derived from the axiomatic approach of justification logic. Additionally, we present possible world semantics in Coq based on Fitting models to formalize the semantic satisfaction of formulas. As an important result, with this implementation, it is possible to give a proof of soundness for $\mathsf{L}\mathsf{P}$ with respect to Fitting models.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  18. Proof Systems for 3-Valued Logics Based on Gödel’s Implication.Arnon Avron - forthcoming - Logic Journal of the IGPL.
    The logic $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ was introduced in Robles and Mendéz as a paraconsistent logic which is based on Gödel’s 3-valued matrix, except that Kleene–Łukasiewicz’s negation is added to the language and is used as the main negation connective. We show that $G3^{<}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ is exactly the intersection of $G3^{\{1\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$ and $G3^{\{1,0.5\}}_{{{}^{\scriptsize{-}}}\!\!\textrm{L}}$, the two truth-preserving 3-valued logics which are based on the same truth tables. We then construct a Hilbert-type system which has for $\to $ as its sole rule of inference, and is (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  19. Quasi-Canonical Systems and Their Semantics.Arnon Avron - forthcoming - Synthese:1-19.
    A canonical Gentzen-type system is a system in which every rule has the subformula property, it introduces exactly one occurrence of a connective, and it imposes no restrictions on the contexts of its applications. A larger class of Gentzen-type systems which is also extensively in use is that of quasi-canonical systems. In such systems a special role is given to a unary connective \ of the language. Accordingly, each application of a logical rule in such systems introduces either a formula (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  20. What is the Meaning of Proofs?Sara Ayhan - forthcoming - Journal of Philosophical Logic:1-21.
    The origins of proof-theoretic semantics lie in the question of what constitutes the meaning of the logical connectives and its response: the rules of inference that govern the use of the connective. However, what if we go a step further and ask about the meaning of a proof as a whole? In this paper we address this question and lay out a framework to distinguish sense and denotation of proofs. Two questions are central here. First of all, if we have (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  21. How Much Propositional Logic Suffices for Rosser’s Essential Undecidability Theorem?Guillermo Badia, Petr Cintula, Petr Hajek & Andrew Tedder - forthcoming - Review of Symbolic Logic:1-18.
    In this paper we explore the following question: how weak can a logic be for Rosser's essential undecidability result to be provable for a weak arithmetical theory? It is well known that Robinson's Q is essentially undecidable in intuitionistic logic, and P. Hajek proved it in the fuzzy logic BL for Grzegorczyk's variant of Q which interprets the arithmetic operations as non-total non-functional relations. We present a proof of essential undecidability in a much weaker substructural logic and for a much (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  22. NL Λ as the Logic of Scope and Movement.Chris Barker - forthcoming - Journal of Logic, Language and Information:1-21.
    Lambek elegantly characterized part of natural language. As is well-known, his substructural logic L, and its non-associative version NL, handle basic function/argument composition well, but not scope taking and syntactic displacement—at least, not in their full generality. In previous work, I propose \, which is NL supplemented with a single structural inference rule.ion closely resembles the traditional linguistic rule of quantifier raising, and characterizes both semantic scope taking and syntactic displacement. Due to the unconventional form of the abstraction inference, there (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  23. On Bivalent Semantics and Natural Deduction for Some Infectious Logics.Alex Belikov - forthcoming - Logic Journal of the IGPL.
    In this work, we propose a variant of so-called informational semantics, a technique elaborated by Voishvillo, for two infectious logics, Deutsch’s ${\mathbf{S}_{\mathbf{fde}}}$ and Szmuc’s $\mathbf{dS}_{\mathbf{fde}}$. We show how the machinery of informational semantics can be effectively used to analyse truth and falsity conditions of disjunction and conjunction. Using this technique, it is possible to claim that disjunction and conjunction can be rightfully regarded as such, a claim which was disputed in the recent literature. Both ${\mathbf{S}_{\mathbf{fde}}}$ and $\mathbf{dS}_{\mathbf{fde}}$ are formalized in (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  24. The Subformula Property of Natural Deduction Derivations and Analytic Cuts.Mirjana Borisavljević - forthcoming - Logic Journal of the IGPL.
    In derivations of a sequent system, $\mathcal{L}\mathcal{J}$, and a natural deduction system, $\mathcal{N}\mathcal{J}$, the trails of formulae and the subformula property based on these trails will be defined. The derivations of $\mathcal{N}\mathcal{J}$ and $\mathcal{L}\mathcal{J}$ will be connected by the map $g$, and it will be proved the following: an $\mathcal{N}\mathcal{J}$-derivation is normal $\Longleftrightarrow $ it has the subformula property based on trails $\Longleftrightarrow $ its $g$-image in $\mathcal{L}\mathcal{J}$ is without maximum cuts $\Longrightarrow $ that $g$-image has the subformula property based (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  25. Simplified Gentzenizations for Contraction-Less Logics.Ross T. Brady - forthcoming - Logique Et Analyse.
    Remove from this list  
     
    Export citation  
     
    Bookmark   3 citations  
  26. 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  
  27. Cut-Free Completeness for Modular Hypersequent Calculi for Modal Logics K, T, and D.Samara Burns & Richard Zach - forthcoming - Review of Symbolic Logic:1-20.
    We investigate a recent proposal for modal hypersequent calculi. The interpretation of relational hypersequents incorporates an accessibility relation along the hypersequent. These systems give the same interpretation of hypersequents as Lellman's linear nested sequents, but were developed independently by Restall for S5 and extended to other normal modal logics by Parisi. The resulting systems obey Došen's principle: the modal rules are the same across different modal logics. Different modal systems only differ in the presence or absence of external structural rules. (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  28. The Logic of Orthomodular Posets of Finite Height.Ivan Chajda & Helmut Länger - forthcoming - Logic Journal of the IGPL.
    Orthomodular posets form an algebraic formalization of the logic of quantum mechanics. A central question is how to introduce implication in such a logic. We give a positive answer whenever the orthomodular poset in question is of finite height. The crucial advantage of our solution is that the corresponding algebra, called implication orthomodular poset, i.e. a poset equipped with a binary operator of implication, corresponds to the original orthomodular poset and that its implication operator is everywhere defined. We present here (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  29. From Many-Valued Consequence to Many-Valued Connectives.Emmanuel Chemla & Paul Egré - forthcoming - Synthese:1-38.
    Given a consequence relation in many-valued logic, what connectives can be defined? For instance, does there always exist a conditional operator internalizing the consequence relation, and which form should it take? In this paper, we pose this question in a multi-premise multi-conclusion setting for the class of so-called intersective mixed consequence relations, which extends the class of Tarskian relations. Using computer-aided methods, we answer extensively for 3-valued and 4-valued logics, focusing not only on conditional operators, but also on what we (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  30. Calculizing Classical Inferential Erotetic Logic.Moritz Cordes - forthcoming - Review of Symbolic Logic:1-22.
    This paper contributes to the calculization of evocation and erotetic implication as defined by Inferential Erotetic Logic (IEL). There is a straightforward approach to calculizing (propositional) erotetic implication which cannot be applied to evocation. First-order evocation is proven to be uncalculizable, i.e. there is no proof system, say FOE, such that for all X, Q: X evokes Q iff there is an FOE-proof for the evocation of Q by X. These results suggest a critique of the represented approaches to calculizing (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  31. ST, LP and Tolerant Metainferences.Bogdan Dicher & Francesco Paoli - forthcoming - In C. Bașkent & Thomas Ferguson (eds.), Graham Priest on dialetheism and paraconsistency. Springer.
  32. Proof-Theoretic Pluralism.Filippo Ferrari & Eugenio Orlandelli - forthcoming - Synthese:1-25.
    Starting from a proof-theoretic perspective, where meaning is determined by the inference rules governing logical operators, in this paper we primarily aim at developing a proof-theoretic alternative to the model-theoretic meaning-invariant logical pluralism discussed in Beall and Restall. We will also outline how this framework can be easily extended to include a form of meaning-variant logical pluralism. In this respect, the framework developed in this paper—which we label two-level proof-theoretic pluralism—is much broader in scope than the one discussed in Beall (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  33. The Power of Naive Truth.Hartry Field - forthcoming - Review of Symbolic Logic:1-34.
    Nonclassical theories of truth that take truth to be transparent have some obvious advantages over any classical theory of truth. But several authors have recently argued that there’s also a big disadvantage of nonclassical 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 the resulting internal theories are (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  34. A Poly-Connexive Logic.Nissim Francez - forthcoming - Logic and Logical Philosophy:1.
    The paper introduces a variant of connexive logic in which connexivity is extended from the interaction of negation with implication to the interaction of negation also with conjunction and disjunction. The logic is presented by two deductively equivalent methods: an axiomatic one and a natural-deduction one. Both are shown to be complete for a four-valued model theory.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  35. Proof Compression and NP Versus PSPACE II.Lew Gordeev & Edward Hermann Haeusler - forthcoming - Bulletin of the Section of Logic.
    We upgrade [3] to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on [2]. Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suffices to show that every valid purely implicational formula ρ has a proof whose weight and time complexity of the provability involved are both polynomial in the weight of (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  36. Postponement of Reduction Ad Absurdum and Glivenko’s Theorem, Revisited.Giulio Guerrieri & Alberto Naibo - forthcoming - Studia Logica:1-36.
    We study how to postpone the application of the reductio ad absurdum rule (RAA) in classical natural deduction. This technique is connected with two normalization strategies for classical logic, due to Prawitz and Seldin, respectively. We introduce a variant of Seldin’s strategy for the postponement of RAA, which induces a negative translation from classical to intuitionistic and minimal logic. Through this translation, Glivenko’s theorem from classical to intuitionistic and minimal logic is proven.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  37. Plans and Planning in Mathematical Proofs.Yacin Hamami & Rebecca Lea Morris - forthcoming - Review of Symbolic Logic:1-40.
    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   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  38. Epistemic Multilateral Logic.Luca Incurvati & Julian J. Schlöder - forthcoming - Review of Symbolic Logic:1-44.
    We present epistemic multilateral logic, a general logical framework for reasoning involving epistemic modality. Standard bilateral systems use propositional formulae marked with signs for assertion and rejection. Epistemic multilateral logic extends standard bilateral systems with a sign for the speech act of weak assertion (Incurvati and Schlöder 2019) and an operator for epistemic modality. We prove that epistemic multilateral logic is sound and complete with respect to the modal logic S5 modulo an appropriate translation. The logical framework developed provides the (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  39. A novel approach to equality.Andrzej Indrzejczak - forthcoming - Synthese:1-26.
    A new type of formalization of classical first-order logic with equality is introduced on the basis of the sequent calculus. It serves to justify the claim that equality is a logical constant characterised by well-behaved rules satisfying properties usually regarded as essential. The main feature of this approach is the application of sequents built not only from formulae but also from terms. Two variants of sequent calculus are examined, a structural and a logical one. The former is defined in accordance (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  40. Free Logics Are Cut-Free.Andrzej Indrzejczak - forthcoming - Studia Logica:1-28.
    The paper presents a uniform proof-theoretic treatment of several kinds of free logic, including the logics of existence and definedness applied in constructive mathematics and computer science, and called here quasi-free logics. All free and quasi-free logics considered are formalised in the framework of sequent calculus, the latter for the first time. It is shown that in all cases remarkable simplifications of the starting systems are possible due to the special rule dealing with identity and existence predicate. Cut elimination is (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  41. Modal and Intuitionistic Variants of Extended Belnap–Dunn Logic with Classical Negation.Norihiro Kamide - forthcoming - Journal of Logic, Language and Information:1-41.
    In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42. Proof-Theoretic Uniform Boundedness and Bounded Collection Principles and Countable Heine–Borel Compactness.Ulrich Kohlenbach - forthcoming - Archive for Mathematical Logic.
    In this note we show that proof-theoretic uniform boundedness or bounded collection principles which allow one to formalize certain instances of countable Heine–Borel compactness in proofs using abstract metric structures must be carefully distinguished from an unrestricted use of countable Heine–Borel compactness.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  43. Mīmāṃsā deontic reasoning using specificity: a proof theoretic approach.Björn Lellmann, Francesca Gulisano & Agata Ciabattoni - forthcoming - Artificial Intelligence and Law:1-44.
    Over the course of more than two millennia the philosophical school of Mīmāṃsā has thoroughly analyzed normative statements. In this paper we approach a formalization of the deontic system which is applied but never explicitly discussed in Mīmāṃsā to resolve conflicts between deontic statements by giving preference to the more specific ones. We first extend with prohibitions and recommendations the non-normal deontic logic extracted in Ciabattoni et al. from Mīmāṃsā texts, obtaining a multimodal dyadic version of the deontic logic \. (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  44. Binary Kripke Semantics for a Strong Logic for Naive Truth.Ben Middleton - forthcoming - Review of Symbolic Logic:1-25.
    I show that the logic $\textsf {TJK}^{d+}$, one of the strongest logics currently known to support the naive theory of truth, is obtained from the Kripke semantics for constant domain intuitionistic logic by dropping the requirement that the accessibility relation is reflexive and only allowing reflexive worlds to serve as counterexamples to logical consequence. In addition, I provide a simplified natural deduction system for $\textsf {TJK}^{d+}$, in which a restricted form of conditional proof is used to establish conditionals.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  45. Natural Deduction and Normal Form for Intuitionistic Linear Logic.S. Negri - forthcoming - Archive for Mathematical Logic.
    Remove from this list  
     
    Export citation  
     
    Bookmark   1 citation  
  46. Proof-Theoretic Analysis of the Logics of Agency: The Deliberative STIT.S. Negri & E. Pavlović - forthcoming - Studia Logica:1-35.
    A sequent calculus methodology for systems of agency based on branching-time frames with agents and choices is proposed, starting with a complete and cut-free system for multi-agent deliberative STIT; the methodology allows a transparent justification of the rules, good structural properties, analyticity, direct completeness and decidability proofs.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  47. A Note on the Sequent Calculi G3[Mic]=.F. Parlamento & F. Previale - forthcoming - Review of Symbolic Logic:1-18.
  48. The Elimination of Atomic Cuts and the Semishortening Property for Gentzen’s Sequent Calculus with Equality.F. Parlamento & F. Previale - forthcoming - Review of Symbolic Logic:1-32.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  49. An Ecumenical Notion of Entailment.Elaine Pimentel, Luiz Carlos Pereira & Valeria de Paiva - forthcoming - Synthese:1-23.
    Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  50. On the Importance of Being Analytic. The Paradigmatic Case of the Logic of Proofs.Francesca Poggiolesi - forthcoming - Logique Et Analyse.
1 — 50 / 2609