6 found
Sort by:
  1. Sachio Hirokawa, Yuichi Komori & Misao Nagayama (2000). A Lambda Proof of the P-W Theorem. Journal of Symbolic Logic 65 (4):1841-1849.
    The logical system P-W is an implicational non-commutative intuitionistic logic defined by axiom schemes B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a with the rules of modus ponens and substitution. The P-W problem is a problem asking whether α = β holds if α → β and β → α are both provable in P-W. The answer is (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  2. Sachio Hirokawa (1996). The Proofs of Α→Α in P - W. Journal of Symbolic Logic 61 (1):195-211.
    The syntactic structure of the system of pure implicational relevant logic P - W is investigated. This system is defined by the axioms B = (b → c) → (a → b) → a → c, B' = (a → b) → (b → c) → a → c, I = a → a, and the rules of substitution and modus ponens. A class of λ-terms, the closed hereditary right-maximal linear λ-terms, and a translation of such λ-terms M to BB'I-combinators (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  3. Sachio Hirokawa (1996). The Proofs of $Alpha Rightarrow Alpha$ in $P - W$. Journal of Symbolic Logic 61 (1):195-211.
    The syntactic structure of the system of pure implicational relevant logic $P - W$ is investigated. This system is defined by the axioms $B = (b \rightarrow c) \rightarrow (a \rightarrow b) \rightarrow a \rightarrow c, B' = (a \rightarrow b) \rightarrow (b \rightarrow c) \rightarrow a \rightarrow c, I = a \rightarrow a$, and the rules of substitution and modus ponens. A class of $\lambda$-terms, the closed hereditary right-maximal linear $\lambda$-terms, and a translation of such $\lambda$-terms $M$ to $BB'I$-combinators (...)
    Direct download  
     
    My bibliography  
     
    Export citation  
  4. Sachio Hirokawa, Yuichi Komori & Izumi Takeuti (1996). A Reduction Rule for Peirce Formula. Studia Logica 56 (3):419 - 426.
    A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a -calculus with a new constant P (()). It is shown that all terms with the same type are equivalent with respect to -reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for P-reduction. Weak normalization is shown for P-reduction with another (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  5. Yuichi Komori & Sachio Hirokawa (1993). The Number of Proofs for a BCK-Formula. Journal of Symbolic Logic 58 (2):626-628.
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  6. Sachio Hirokawa (1992). The Converse Principal Type-Scheme Theorem in Lambda Calculus. Studia Logica 51 (1):83 - 95.
    A principal type-scheme of a -term is the most general type-scheme for the term. The converse principal type-scheme theorem (J.R. Hindley, The principal typescheme of an object in combinatory logic, Trans. Amer. Math. Soc. 146 (1969) 29–60) states that every type-scheme of a combinatory term is a principal type-scheme of some combinatory term.This paper shows a simple proof for the theorem in -calculus, by constructing an algorithm which transforms a type assignment to a -term into a principal type assignment to (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation