Order:
  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 (...)
    Download  
     
    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.
    Download  
     
    Export citation  
     
    Bookmark  
  3. 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 (...)
    Download  
     
    Export citation  
     
    Bookmark