Switch to: References

Add citations

You must login to add citations.
  1. 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.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • The existential fragment of second-order propositional intuitionistic logic is undecidable.Ken-Etsu Fujita, Aleksy Schubert, Paweł Urzyczyn & Konrad Zdanowski - 2024 - Journal of Applied Non-Classical Logics 34 (1):55-74.
    The provability problem in intuitionistic propositional second-order logic with existential quantifier and implication (∃,→) is proved to be undecidable in presence of free type variables (constants). This contrasts with the result that inutitionistic propositional second-order logic with existential quantifier, conjunction and negation is decidable.
    Download  
     
    Export citation  
     
    Bookmark  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations