Order:
See also
  1. Consistency proof of a fragment of pv with substitution in bounded arithmetic.Yoriyuki Yamagata - 2018 - Journal of Symbolic Logic 83 (3):1063-1090.
    This paper presents proof that Buss's S22 can prove the consistency of a fragment of Cook and Urquhart's PV from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic S12. Our proof relies on the notion of "computation" of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved and either (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  2. Strong normalization of a symmetric lambda calculus for second-order classical logic.Yoriyuki Yamagata - 2002 - Archive for Mathematical Logic 41 (1):91-99.
    We extend Barbanera and Berardi's symmetric lambda calculus to second-order classical propositional logic and prove its strong normalization.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  3.  4
    A sequent calculus for Limit Computable Mathematics.Stefano Berardi & Yoriyuki Yamagata - 2008 - Annals of Pure and Applied Logic 153 (1-3):111-126.
    We introduce an implication-free fragment image of ω-arithmetic, having Exchange rule for sequents dropped. Exchange rule for formulas is, instead, an admissible rule in image. Our main result is that cut-free proofs of image are isomorphic with recursive winning strategies of a set of games called “1-backtracking games” in [S. Berardi, Th. Coquand, S. Hayashi, Games with 1-backtracking, Games for Logic and Programming Languages, Edinburgh, April 2005].We also show that image is a sound and complete formal system for the implication-free (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations