Related categories

2686 found
Order:
1 — 50 / 2686
  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   1 citation  
  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 the Fixed Point Lemma.T. Parent - manuscript
    This paper argues that the Fixed Point Lemma implies that contradiction is derivable within primitive recursive arithmetic (PRA). Since PRA is consistent, this is regarded as a paradox to be resolved. The argument is inspired by the v-Curry paradox, but we utilize only a syntactic notion of derivability, not a semantic notion such as validity. The new paradox could be blocked by excluding certain formulae from the scope of the Fixed Point Lemma, but this would effectively concede that the unrestricted (...)
    Remove from this list   Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  8. Contradiction From a Coded Proof Predicate (Very Tentative Draft, Do Not Cite).T. Parent - manuscript
  9. 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  
  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. One-Pass Tableaux for Computation Tree Logic.Rajeev Gore - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  12. 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  
  13. A Cut-Free Sequent Calculus for Bi-Intuitionistic Logic.Rajeev Gore - manuscript
  14. Proof Theory and Meaning: On Second Order Logic.Greg Restall - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  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 - manuscript
    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. 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  
  20. 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  
  21. 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  
  22. 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  
  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. 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  
  27. 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  
  28. An Abductive Question-Answer System for the Minimal Logic of Formal Inconsistency $$\mathsf {mbC}$$ mbC.Szymon Chlebowski, Andrzej Gajda & Mariusz Urbański - forthcoming - Studia Logica:1-31.
    The aim in this paper is to define an Abductive Question-Answer System for the minimal logic of formal inconsistency \. As a proof-theoretical basis we employ the Socratic proofs method. The system produces abductive hypotheses; these are answers to abductive questions concerning derivability of formulas from sets of formulas. We integrated the generation of and the evaluation of hypotheses via constraints of consistency and significance being imposed on the system rules.
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  29. 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  
  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. Denotational Semantics for Languages of Epistemic Grounding Based on Prawitz’s Theory of Grounds.Antonio Piccolomini D’Aragona - forthcoming - Studia Logica:1-49.
    We outline a class of term-languages for epistemic grounding inspired by Prawitz’s theory of grounds. We show how denotation functions can be defined over these languages, relating terms to proof-objects built up of constructive functions. We discuss certain properties that the languages may enjoy both individually and with respect to their expansions. Finally, we provide a ground-theoretic version of Prawitz’s completeness conjecture, and adapt to our framework a refutation of this conjecture due to Piecha and Schroeder-Heister.
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  33. Proofs, Grounds and Empty Functions: Epistemic Compulsion in Prawitz’s Semantics.Antonio Piccolomini D’Aragona - forthcoming - Journal of Philosophical Logic:1-33.
    Prawitz has recently developed a theory of epistemic grounding that differs in many respects from his earlier semantics of arguments and proofs. An innovative approach to inferences yields a new conception of the intertwinement of the notions of valid inference and proof. We aim at singling out three reasons that may have led Prawitz to the ground-theoretic turn, i.e.: a better order in the explanation of the relation between valid inferences and proofs; a notion of valid inference based on which (...)
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  34. 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   3 citations  
  35. Nonclassical Truth with Classical Strength. A Proof-Theoretic Analysis of Compositional Truth Over Hype.Martin Fischer, Carlo Nicolai & Pablo Dopico - forthcoming - Review of Symbolic Logic:1-24.
    Questions concerning the proof-theoretic strength of classical versus nonclassical theories of truth have received some attention recently. A particularly convenient case study concerns classical and nonclassical axiomatizations of fixed-point semantics. It is known that nonclassical axiomatizations in four- or three-valued logics are substantially weaker than their classical counterparts. In this paper we consider the addition of a suitable conditional to First-Degree Entailment—a logic recently studied by Hannes Leitgeb under the label HYPE. We show in particular that, by formulating the theory (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  36. 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  
  37. 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  
  38. 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  
  39. 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  
  40. 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  
  41. 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  
  42. Tukey Order Among F Σ Ideals.Jialiang He, Michael Hrušák, Diego Rojas-Rebolledo & Sławomir Solecki - forthcoming - Journal of Symbolic Logic:1-15.
    We investigate the Tukey order in the class of Fσ ideals of subsets of ω. We show that no nontrivial Fσ ideal is Tukey below a Gδ ideal of compact sets. We introduce the notions of flat ideals and gradually flat ideals. We prove a dichotomy theorem for flat ideals isolating gradual flatness as the side of the dichotomy that is structurally good. We give diverse characterizations of gradual flatness among flat ideals using Tukey reductions and games. For example, we (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  43. 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   3 citations  
  44. 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  
  45. 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  
  46. On Inclusions Between Quantified Provability Logics.Taishi Kurahashi - forthcoming - Studia Logica:1-24.
    We investigate several consequences of inclusion relations between quantified provability logics. Moreover, we give a necessary and sufficient condition for the inclusion relation between quantified provability logics with respect to \ arithmetical interpretations.
    Remove from this list   Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  47. Normalisation and Subformula Property for a System of Classical Logic with Tarski’s Rule.Nils Kürbis - forthcoming - Archive for Mathematical Logic:1-25.
    This paper considers a formalisation of classical logic using general introduction rules and general elimination rules. It proposes a definition of ‘maximal formula’, ‘segment’ and ‘maximal segment’ suitable to the system, and gives reduction procedures for them. It is then shown that deductions in the system convert into normal form, i.e. deductions that contain neither maximal formulas nor maximal segments, and that deductions in normal form satisfy the subformula property. Tarski’s Rule is treated as a general introduction rule for implication. (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  48. Normalisation and Subformula Property for a System of Intuitionistic Logic with General Introduction and Elimination Rules.Nils Kürbis - forthcoming - Synthese.
    This paper studies a formalisation of intuitionistic logic by Negri and von Plato which has general introduction and elimination rules. The philosophical importance of the system is expounded. Definitions of `maximal formula', `segment' and `maximal segment' suitable to the system are formulated and corresponding reduction procedures for maximal formulas and permutative reduction procedures for maximal segments given. Alternatives to the main method used are also considered. It is shown that deductions in the system convert into normal form and that deductions (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  49. 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  
  50. 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  
1 — 50 / 2686