Related categories

2792 found
Order:
1 — 50 / 2792
  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 citations  
  4. A Fundamental Non-Classical Logic.Wesley Holliday - manuscript
    We give a proof-theoretic as well as a semantic characterization of a logic in the signature with conjunction, disjunction, negation, and the universal and existential quantifiers that we suggest has a certain fundamental status. We present a Fitch-style natural deduction system for the logic that contains only the introduction and elimination rules for the logical constants. From this starting point, if one adds the rule that Fitch called Reiteration, one obtains a proof system for intuitionistic logic in the given signature; (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  5. 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  
  6. 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  
  7. 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  
  8. 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  
  9. Montague's Paradox Without Necessitation.T. Parent -
    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  
  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
    Remove from this list  
     
    Export citation  
     
    Bookmark   6 citations  
  13. One-Pass Tableaux for Computation Tree Logic.Rajeev Gore - manuscript
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  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)  
     
    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. Wellfoundedness proof with the maximal distinguished set.Toshiyasu Arai - forthcoming - Archive for Mathematical Logic:1-25.
    In Arai it is shown that an ordinal \\) is an upper bound for the proof-theoretic ordinal of a set theory \\). In this paper we show that a second order arithmetic \ proves the wellfoundedness up to \\) for each N. It is easy to interpret \ in \\).
    Remove from this list   Direct download (3 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   3 citations  
  22. 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   1 citation  
  23. Simplified Gentzenizations for Contraction-Less Logics.Ross T. Brady - forthcoming - Logique Et Analyse.
    Remove from this list  
     
    Export citation  
     
    Bookmark   3 citations  
  24. 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  
  25. 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)  
     
    Export citation  
     
    Bookmark   5 citations  
  26. 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  
  27. Coordination and Harmony in Bilateral Logic.Pedro del Valle-Inclan & Julian J. Schloeder - forthcoming - Mind.
    Ian Rumfitt (2000) developed a bilateralist account of logic in which the meaning of the connectives is given by conditions on asserted and rejected sentences. An additional set of inference rules, the coordination principles, determines the interaction of assertion and rejection. Fernando Ferreira (2008) found this account defective, as Rumfitt must state the coordination principles for arbitrary complex sentences. Rumfitt (2008) has a reply, but we argue that the problem runs deeper than he acknowledges and is in fact related to (...)
    Remove from this list   Direct download  
     
    Export citation  
     
    Bookmark  
  28. 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  
  29. Inferential Constants.Camillo Fiore, Federico Pailos & Mariela Rubin - forthcoming - Journal of Philosophical Logic: 1 - 26.
    A metainference is usually understood as a pair consisting of a collection of inferences, called premises, and a single inference, called conclusion. In the last few years, much attention has been paid to the study of metainferences—and, in particular, to the question of what are the valid metainferences of a given logic. So far, however, this study has been done in quite a poor language. Our usual sequent calculi have no way to represent, e.g. negations, disjunctions or conjunctions of inferences. (...)
    Remove from this list   Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  30. 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)  
     
    Export citation  
     
    Bookmark   2 citations  
  31. 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   3 citations  
  32. 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  
  33. An Argument From Proof Theory Against Implicit Conventionalism.Rea Golan - forthcoming - Philosophical Quarterly.
    Conventionalism about logic is the view that logical principles hold in virtue of some linguistic conventions. According to explicit conventionalism, these conventions have to be stipulated explicitly. Explicit conventionalism is subject to a famous criticism by Quine, who accused it of leading to an infinite regress. In response to the criticism, several authors have suggested reconstructing conventionalism as implicit in our linguistic behaviour. In this paper, drawing on a distinction from proof theory between derivable and admissible rules, I argue that (...)
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  34. 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   4 citations  
  35. On the Metainferential Solution to the Semantic Paradoxes.Rea Golan - forthcoming - Journal of Philosophical Logic:1-24.
    Substructural solutions to the semantic paradoxes have been broadly discussed in recent years. In particular, according to the non-transitive solution, we have to give up the metarule of Cut, whose role is to guarantee that the consequence relation is transitive. This concession—giving up a meta rule—allows us to maintain the entire consequence relation of classical logic. The non-transitive solution has been generalized in recent works into a hierarchy of logics where classicality is maintained at more and more metainferential levels. All (...)
    Remove from this list   Direct download (4 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   2 citations  
  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   3 citations  
  38. 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)  
     
    Export citation  
     
    Bookmark   1 citation  
  39. Fregean Description Theory in Proof-Theoretical Setting.Andrzej Indrzejczak - forthcoming - Logic and Logical Philosophy:1.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  40. Two-Sided Sequent Calculi for FDE-Like Four-Valued Logics.Barteld Kooi & Allard Tamminga - forthcoming - Journal of Philosophical Logic:1-24.
    We present a method that generates two-sided sequent calculi for four-valued logics like "first degree entailment" (FDE). (We say that a logic is FDE-like if it has finitely many operators of finite arity, including negation, and if all of its operators are truth-functional over the four truth-values 'none', 'false', 'true', and 'both', where 'true' and 'both' are designated.) First, we show that for every n-ary operator * every truth table entry f*(x1,...,xn) = y can be characterized in terms of a (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  41. Proof Systems for Exact Entailment.Johannes Korbmacher - forthcoming - Review of Symbolic Logic:1-37.
    We present a series of proof systems for exact entailment (i.e. relevant truthmaker preservation from premises to conclusion) and prove soundness and completeness. Using the proof systems, we observe that exact entailment is not only hyperintensional in the sense of Cresswell but also in the sense recently proposed by Odintsov and Wansing.
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  42. The Turing Degrees and Keisler’s Order.M. Malliaris & S. Shelah - forthcoming - Journal of Symbolic Logic:1-11.
  43. The Axiom of Choice is False Intuitionistically.Charles Mccarty, Stewart Shapiro & Ansten Klev - forthcoming - Bulletin of Symbolic Logic:1-26.
  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   3 citations  
  46. A Note on the Sequent Calculi G3[Mic]=.F. Parlamento & F. Previale - forthcoming - Review of Symbolic Logic:1-18.
  47. 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  
  48. The First-Order Logic of CZF is Intuitionistic First-Order Logic.Robert Passmann - forthcoming - Journal of Symbolic Logic:1-23.
    We prove that the first-order logic of CZF is intuitionistic first-order logic. To do so, we introduce a new model of transfinite computation (Set Register Machines) and combine the resulting notion of realisability with Beth semantics. On the way, we also show that the propositional admissible rules of CZF are exactly those of intuitionistic propositional logic.
    Remove from this list   Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  49. 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  
  50. Neutral Free Logic: Motivation, Proof Theory and Models.Edi Pavlović & Norbert Gratzl - forthcoming - Journal of Philosophical Logic:1-36.
    Free logics are a family of first-order logics which came about as a result of examining the existence assumptions of classical logic. What those assumptions are varies, but the central ones are that the domain of interpretation is not empty, every name denotes exactly one object in the domain and the quantifiers have existential import. Free logics reject the claim that names need to denote in. Positive free logic concedes that some atomic formulas containing non-denoting names are true, negative free (...)
    Remove from this list   Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
1 — 50 / 2792