Results for '03F52'

7 found
Order:
  1.  34
    A Note on the Cut-Elimination Proof in “Truth Without Contra(di)Ction”.Andreas Fjellstad - 2020 - Review of Symbolic Logic 13 (4):882-886.
    This note shows that the permutation instructions presented by Zardini (2011) for eliminating cuts on universally quantified formulas in the sequent calculus for the noncontractive theory of truth IKTωare inadequate. To that purpose the note presents a derivation in the sequent calculus for IKTωending with an application of cut on a universally quantified formula which the permutation instructions cannot deal with. The counterexample is of the kind that leaves open the question whether cut can be shown to be eliminable in (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  2.  33
    Core Gödel.Neil Tennant - 2023 - Notre Dame Journal of Formal Logic 64 (1):15-59.
    This study examines how the Gödel phenomena are to be treated in core logic. We show in formal detail how one can use core logic in the metalanguage to prove Gödel’s incompleteness theorems for arithmetic even when classical logic is used for logical closure in the object language.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  3.  16
    Weihrauch Goes Brouwerian.Vasco Brattka & Guido Gherardi - 2020 - Journal of Symbolic Logic 85 (4):1614-1653.
    We prove that the Weihrauch lattice can be transformed into a Brouwer algebra by the consecutive application of two closure operators in the appropriate order: first completion and then parallelization. The closure operator of completion is a new closure operator that we introduce. It transforms any problem into a total problem on the completion of the respective types, where we allow any value outside of the original domain of the problem. This closure operator is of interest by itself, as it (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  17
    Affine logic for constructive mathematics.Michael Shulman - 2022 - Bulletin of Symbolic Logic 28 (3):327-386.
    We show that numerous distinctive concepts of constructive mathematics arise automatically from an “antithesis” translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically “constructivize” classical definitions, handling the resulting bookkeeping automatically.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  4
    Isomorphic formulae in classical propositional logic.Kosta Došen & Zoran Petrić - 2012 - Mathematical Logic Quarterly 58 (1):5-17.
    Isomorphism between formulae is defined with respect to categories formalizing equality of deductions in classical propositional logic and in the multiplicative fragment of classical linear propositional logic caught by proof nets. This equality is motivated by generality of deductions. Characterizations are given for pairs of isomorphic formulae, which lead to decision procedures for this isomorphism.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  6.  15
    On Zardini’s Rules for Multiplicative Quantification as the Source of Contra(di)Ctions.Uwe Petersen - 2023 - Review of Symbolic Logic 16 (4):1110-1119.
    Certain instances of contraction are provable in Zardini’s system $\mathbf {IK}^\omega $ which causes triviality once a truth predicate and suitable fixed points are available.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7.  15
    Complexity of the Infinitary Lambek Calculus with Kleene Star.Stepan Kuznetsov - 2021 - Review of Symbolic Logic 14 (4):946-972.
    We consider the Lambek calculus, or noncommutative multiplicative intuitionistic linear logic, extended with iteration, or Kleene star, axiomatised by means of an$\omega $-rule, and prove that the derivability problem in this calculus is$\Pi _1^0$-hard. This solves a problem left open by Buszkowski (2007), who obtained the same complexity bound for infinitary action logic, which additionally includes additive conjunction and disjunction. As a by-product, we prove that any context-free language without the empty word can be generated by a Lambek grammar with (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark