7 found
Order:
  1. Corrigendum to “Strong Normalization Proof with CPS-Translation for Second Order Classical Natural Deduction”.Koji Nakazawa & Makoto Tatsuta - 2003 - Journal of Symbolic Logic 68 (4):1415-1416.
    This paper points out an error of Parigot's proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.
    Direct download (12 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2. Uniqueness of Normal Proofs of Minimal Formulas.Makoto Tatsuta - 1993 - Journal of Symbolic Logic 58 (3):789-799.
    A minimal formula is a formula which is minimal in provable formulas with respect to the substitution relation. This paper shows the following: (1) A β-normal proof of a minimal formula of depth 2 is unique in NJ. (2) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NJ. (3) There exists a minimal formula of depth 3 whose βη-normal proof is not unique in NK.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  3.  7
    A Simple Proof of Second-Order Strong Normalization with Permutative Conversions.Makoto Tatsuta & Grigori Mints - 2005 - Annals of Pure and Applied Logic 136 (1-2):134-155.
    A simple and complete proof of strong normalization for first- and second-order intuitionistic natural deduction including disjunction, first-order existence and permutative conversions is given. The paper follows the Tait–Girard approach via computability predicates and saturated sets. Strong normalization is first established for a set of conversions of a new kind, then deduced for the standard conversions. Difficulties arising for disjunction are resolved using a new logic where disjunction is restricted to atomic formulas.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  4.  18
    Inhabitation of Polymorphic and Existential Types.Makoto Tatsuta, Ken-Etsu Fujita, Ryu Hasegawa & Hiroshi Nakano - 2010 - Annals of Pure and Applied Logic 161 (11):1390-1399.
    This paper shows that the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable, where the inhabitation problem asks whether there exists some term that belongs to a given type. In order to do that, this paper proves the decidability of the provability in the logical system defined from the second-order natural deduction by removing implication and disjunction. This is proved by showing the quantifier elimination theorem and reducing the problem to the provability in (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  7
    Strong Normalization of Classical Natural Deduction with Disjunctions.Koji Nakazawa & Makoto Tatsuta - 2008 - Annals of Pure and Applied Logic 153 (1-3):21-37.
    This paper proves the strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. Using them, this paper also proves the strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves that natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6.  8
    The Function\ Lfloor a/M\ Rfloor in Sharply Bounded Arithmetic.Mitsuru Tada & Makoto Tatsuta - 1997 - Archive for Mathematical Logic 37 (1):51-57.
  7.  4
    The Function [Mathematical Formula] in Sharply Bounded Arithmetic.Mitsuru Tada & Makoto Tatsuta - 1997 - Archive for Mathematical Logic 1.
    Direct download  
     
    Export citation  
     
    Bookmark