See also
  1.  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 (5 more)  
    Export citation  
    Bookmark   2 citations  
  2.  84
    Consistency Proof of a Fragment of Pv with Substitution in Bounded Arithmetic.Yoriyuki Yamagata - 2018 - Journal of Symbolic Logic 83 (3):1063-1090.
    Direct download (3 more)  
    Export citation  
  3. Strong Normalization of a Symmetric Lambda Calculus for Second-Order Classical Logic.Yoriyuki Yamagata - 2002 - Archive for Mathematical Logic 41 (1):91-99.