Related categories

2728 found
Order:
1 — 50 / 2728
  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 -
    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   3 citations  
  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   2 citations  
  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. The Premise Paradox.T. Parent - manuscript
    This paper argues that if our talk of “premises” is not handled carefully, our system of logic will be unsound. This is so, even if a “premise” is defined in nonsemantic terms, viz., as a sentence that is underived in the context of a proof. As a preliminary, I first explain that in a classical formal system, expressions must be seen as linguistic types rather than tokens. [Otherwise, ‘this very term = this very term’ is a false sentence that is (...)
    Remove from this list  
     
    Export citation  
     
    Bookmark   1 citation  
  8. Montague's Paradox Without Necessitation.T. Parent - manuscript
    Some such as Dean (2014) suggest that Montague's paradox requires the necessitation rule, and that the use of the rule in such a context is contentious. But here, I show that the paradox arises independently of the necessitation rule. A derivation of the paradox is given in modal system T without deploying necessitation; a necessitation-free derivation is also formulated in a significantly weaker system.
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  9. 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  
  10. One-Pass Tableaux for Computation Tree Logic.Rajeev Gore - manuscript
    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
    Remove from this list  
     
    Export citation  
     
    Bookmark   6 citations  
  13. Proof Theory and Meaning: On Second Order Logic.Greg Restall - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  14. 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  
  15. Proof Theory and Meaning: On Second Order Logic.Author unknown - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  16. Epistemic Modals in Hypothetical Reasoning.Maria Aloni, Luca Incurvati & Julian J. Schlöder - forthcoming - Erkenntnis:1-31.
    Data involving epistemic modals suggest that some classically valid argument forms, such as reductio, are invalid in natural language reasoning as they lead to modal collapses. We adduce further data showing that the classical argument forms governing the existential quantifier are similarly defective, as they lead to a de re–de dicto collapse. We observe a similar problem for disjunction. But if the classical argument forms for negation, disjunction and existential quantification are invalid, what are the correct forms that govern the (...)
    Remove from this list   Direct download (5 more)  
    Translate
     
     
    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. Epsilon Theorems in Intermediate Logics.Matthias Baaz & Richard Zach - forthcoming - Journal of Symbolic Logic:1-40.
    Any intermediate propositional logic (i.e., a logic including intuitionistic logic and contained in classical logic) can be extended to a calculus with epsilon- and tau-operators and critical formulas. For classical logic, this results in Hilbert’s ε-calculus. The first and second ε-theorems for classical logic establish conservativity of the ε-calculus over its classical base logic. It is well known that the second ε-theorem fails for the intuitionistic ε-calculus, as prenexation is impossible. The paper investigates the effect of adding critical ε- and (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  20. 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  
  21. 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  
  22. Peirce’s Triadic Logic and Its (Overlooked) Connexive Expansion.Alex Belikov - forthcoming - Logic and Logical Philosophy:1.
    In this paper, we present two variants of Peirce’s Triadic Logic within a language containing only conjunction, disjunction, and negation. The peculiarity of our systems is that conjunction and disjunction are interpreted by means of Peirce’s mysterious binary operations Ψ and Φ from his ‘Logical Notebook’. We show that semantic conditions that can be extracted from the definitions of Ψ and Φ agree (in some sense) with the traditional view on the semantic conditions of conjunction and disjunction. Thus, we support (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  23. 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  
  24. Simplified Gentzenizations for Contraction-Less Logics.Ross T. Brady - forthcoming - Logique Et Analyse.
    Remove from this list  
     
    Export citation  
     
    Bookmark   3 citations  
  25. Transmission of Verification.Ethan Brauer & Neil Tennant - forthcoming - Review of Symbolic Logic:1-16.
    This paper clarifies, revises, and extends the account of the transmission of truthmakers by core proofs that was set out in chap. 9 of Tennant. Brauer provided two kinds of example making clear the need for this. Unlike Brouwer’s counterexamples to excluded middle, the examples of Brauer that we are dealing with here establish the need for appeals to excluded middle when applying, to the problem of truthmaker-transmission, the already classical metalinguistic theory of model-relative evaluations.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  26. Single-Assumption Systems in Proof-Theoretic Semantics.Leonardo Ceragioli - forthcoming - Journal of Philosophical Logic:1-36.
    Proof-theoretic semantics is an inferentialist theory of meaning, usually developed in a multiple-assumption and single-conclusion framework. In that framework, this theory seems unable to justify classical logic, so some authors have proposed a multiple-conclusion reformulation to accomplish this goal. In the first part of this paper, the debate originated by this proposal is briefly exposed and used to defend the diverging opinion that proof-theoretic semantics should always endorse a single-assumption and single-conclusion framework. In order to adopt this approach some of (...)
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  27. Higher-level Inferences in the Strong-Kleene Setting: A Proof-theoretic Approach.Pablo Cobreros, Elio La Rosa & Luca Tranchini - forthcoming - Journal of Philosophical Logic:1-36.
    Building on early work by Girard and using closely related techniques from the proof theory of many-valued logics, we propose a sequent calculus capturing a hierarchy of notions of satisfaction based on the Strong Kleene matrices introduced by Barrio et al. and others. The calculus allows one to establish and generalize in a very natural manner several recent results, such as the coincidence of some of these notions with their classical counterparts, and the possibility of expressing some notions of satisfaction (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   2 citations  
  28. 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   3 citations  
  29. ST, LP and Tolerant Metainferences.Bogdan Dicher & Francesco Paoli - forthcoming - In C. Bașkent & Thomas Ferguson (eds.), Graham Priest on dialetheism and paraconsistency. Springer.
  30. Calculi of Epistemic Grounding Based on Prawitz’s Theory of Grounds.Antonio Piccolomini D’Aragona - forthcoming - Studia Logica:1-59.
    We define a class of formal systems inspired by Prawitz’s theory of grounds. The latter is a semantics that aims at accounting for epistemic grounding, namely, at explaining why and how deductively valid inferences have the power to epistemically compel to accept the conclusion. Validity is defined in terms of typed objects, called grounds, that reify evidence for given judgments. An inference is valid when a function exists from grounds for the premises to grounds for the conclusion. Grounds are described (...)
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  31. A Substructural Gentzen Calculus for Orthomodular Quantum Logic.Davide Fazio, Antonio Ledda, Francesco Paoli & Gavin St John - forthcoming - Review of Symbolic Logic:1-22.
    We introduce a sequent system which is Gentzen algebraisable with orthomodular lattices as equivalent algebraic semantics, and therefore can be viewed as a calculus for orthomodular quantum logic. Its sequents are pairs of non-associative structures, formed via a structural connective whose algebraic interpretation is the Sasaki product on the left-hand side and its De Morgan dual on the right-hand side. It is a substructural calculus, because some of the standard structural sequent rules are restricted—by lifting all such restrictions, one recovers (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  32. Correction to: Cut-free Sequent Calculus and Natural Deduction for the Tetravalent Modal Logic.Martín Figallo - forthcoming - Studia Logica:1-1.
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  33. Metainferential Reasoning on Strong Kleene Models.Andreas Fjellstad - forthcoming - Journal of Philosophical Logic:1-18.
    Barrio et al., 93–120, 2020) and Pailos, 249–268, 2020) develop an approach to define various metainferential hierarchies on strong Kleene models by transferring the idea of distinct standards for premises and conclusions from inferences to metainferences. In particular, they focus on a hierarchy named the \-hierarchy where the inferential logic at the bottom of the hierarchy is the non-transitive logic ST but where each subsequent metainferential logic ‘says’ about the former logic that it is transitive. While Barrio et al. suggests (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  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. Metainferences From a Proof-Theoretic Perspective, and a Hierarchy of Validity Predicates.Rea Golan - forthcoming - Journal of Philosophical Logic 1:1-31.
    I explore, from a proof-theoretic perspective, the hierarchy of classical and paraconsistent logics introduced by Barrio, Pailos and Szmuc in. First, I provide sequent rules and axioms for all the logics in the hierarchy, for all inferential levels, and establish soundness and completeness results. Second, I show how to extend those systems with a corresponding hierarchy of validity predicates, each one of which is meant to capture “validity” at a different inferential level. Then, I point out two potential philosophical implications (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  36. A Simple Sequent System for Minimally Inconsisteny LP.Rea Golan - forthcoming - Review of Symbolic Logic:1-16.
    Minimally inconsistent LP (MiLP) is a nonmonotonic paraconsistent logic based on Graham Priest's logic of paradox (LP). Unlike LP, MiLP purports to recover, in consistent situations, all of classical reasoning. The present paper conducts a proof-theoretic analysis of MiLP. I highlight certain properties of this logic, introduce a simple sequent system for it, and establish soundness and completeness results. In addition, I show how to use my proof system in response to a criticism of this logic put forward by JC (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  37. 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  
  38. 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   2 citations  
  39. On Cut-Elimination Arguments for Axiomatic Theories of Truth.Daichi Hayashi - forthcoming - Studia Logica:1-34.
    As is mentioned in Leigh :845-865, 2015), it is an open problem whether for several axiomatic theories of truth, including Friedman–Sheard theory \ and Kripke–Feferman theory \ :690-716, 1976), there exist cut-elimination arguments that give the upper bounds of their proof-theoretic strengths. In this paper, we give complete cut-elimination results for several well-known axiomatic theories of truth. In particular, we treat the systems \, and \ \\) of Friedman and Sheard’s theories and \.
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  40. Meta-Inferences and Supervaluationism.Luca Incurvati & Julian J. Schlöder - forthcoming - Journal of Philosophical Logic:1-34.
    Many classically valid meta-inferences fail in a standard supervaluationist framework. This allegedly prevents supervaluationism from offering an account of good deductive reasoning. We provide a proof system for supervaluationist logic which includes supervaluationistically acceptable versions of the classical meta-inferences. The proof system emerges naturally by thinking of truth as licensing assertion, falsity as licensing negative assertion and lack of truth-value as licensing rejection and weak assertion. Moreover, the proof system respects well-known criteria for the admissibility of inference rules. Thus, supervaluationists (...)
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  41. Embedding Friendly First-Order Paradefinite and Connexive Logics.Norihiro Kamide - forthcoming - Journal of Philosophical Logic:1-48.
    First-order intuitionistic and classical Nelson–Wansing and Arieli–Avron–Zamansky logics, which are regarded as paradefinite and connexive logics, are investigated based on Gentzen-style sequent calculi. The cut-elimination and completeness theorems for these logics are proved uniformly via theorems for embedding these logics into first-order intuitionistic and classical logics. The modified Craig interpolation theorems for these logics are also proved via the same embedding theorems. Furthermore, a theorem for embedding first-order classical Arieli–Avron–Zamansky logic into first-order intuitionistic Arieli–Avron–Zamansky logic is proved using a modified (...)
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  42. Mathematical Incompleteness Results in First-Order Peano Arithmetic: A Revisionist View of the Early History.Saul A. Kripke - forthcoming - History and Philosophy of Logic:1-8.
    In the Handbook of Mathematical Logic, the Paris-Harrington variant of Ramsey's theorem is celebrated as the first result of a long ‘search’ for a purely mathematical incompleteness result in first-order Peano arithmetic. This paper questions the existence of any such search and the status of the Paris-Harrington result as the first mathematical incompleteness result. In fact, I argue that Gentzen gave the first such result, and that it was restated by Goodstein in a number-theoretic form.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  43. A Proof of Gamma.Saul A. Kripke - forthcoming - In Katalin Bimbó (ed.), Relevance Logics and other Tools for Reasoning. Essays in Honor of J. Michael Dunn. London: College Publications. pp. 261-265.
    This paper is dedicated to the memory of Mike Dunn. His untimely death is a loss not only to logic, computer science, and philosophy, but to all of us who knew and loved him. The paper gives an argument for closure under γ in standard systems of relevance logic (first proved by Meyer and Dunn 1969). For definiteness, I chose the example of R. The proof also applies to E and to the quantified systems RQ and EQ. The argument uses (...)
    Remove from this list   Direct download  
     
    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   2 citations  
  46. A Marriage of Brouwer’s Intuitionism and Hilbert’s Finitism I: Arithmetic.Takako Nemoto & Sato Kentaro - forthcoming - Journal of Symbolic Logic:1-61.
    We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: fan theorem for decidable fans but arbitrary bars; continuity principle (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  47. A Modal View on Resource-Bounded Propositional Logics.Pere Pardo - forthcoming - Studia Logica:1-46.
    Classical propositional logic plays a prominent role in industrial applications, and yet the complexity of this logic is presumed to be non-feasible. Tractable systems such as depth-bounded boolean logics approximate classical logic and can be seen as a model for resource-bounded agents whose reasoning style is nonetheless classical. In this paper we first study a hierarchy of tractable logics that is not defined by depth. Then we extend it into a modal logic where modalities make explicit the assumptions discharged in (...)
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  48. A Note on the Sequent Calculi G3[Mic]=.F. Parlamento & F. Previale - forthcoming - Review of Symbolic Logic:1-18.
  49. 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   2 citations  
  50. Dialogue Games for Minimal Logic.Alexandra Pavlova - forthcoming - Logic and Logical Philosophy:1.
    In this paper, we define a class of dialogue games for Johansson’s minimal logic and prove that it corresponds to the validity of minimal logic. Many authors have stated similar results for intuitionistic and classical logic either with or without actually proving the correspondence. Rahman, Clerbout and Keiff [17] have already specified dialogues for minimal logic; however, they transformed it into Fitch-style natural deduction only. We propose a different specification for minimal logic with the proof of correspondence between the existence (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 2728