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 (...) affirmative. The first to prove this was E. P. Martin by a semantical method. In this paper, we give the first proof of Martin's theorem based on the theory of simply typed λ-calculus. This proof is obtained as a corollary to the main theorem of this paper, shown without using Martin's Theorem, that any closed hereditary right-maximal linear (HRML) λ-term of type α → α is βη-reducible to λ x.x. Here the HRML λ-terms correspond, via the Curry-Howard isomorphism, to the P-W proofs in natural deduction style. (shrink)

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 (...) reduction rule which simplifies of (( ) ) into an atomic type. (shrink)

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 (...) another -term that has the type as its principal type-scheme. The clearness of the algorithm is due to the characterization theorem of principal type-assignment figures. The algorithm is applicable to BCIW--terms as well. Thus a uniform proof is presented for the converse principal type-scheme theorem for general -terms and BCIW--terms. (shrink)

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 (...) M + is introduced. It is shown that a formula α is provable in P - W if and only if α is a type of some λ-term in this class. Hence these λ-terms represent proof figures in the Natural Deduction version of P - W. Errol Martin (1982) proved that no formula with form α → α is provable in P - W without using the axiom I. We show that a β-normal form λ-term M in the class is η reducible to λ x.x if the translated BB'I-combinator M + contains I. Using this theorem and Martin's result, we prove that a λ-term in the class is βη-reducible to λ x.x if the λ-term has a type α → α. Hence the structure of proofs of α → α in P - W is determined. (shrink)

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 (...) $M^+$ is introduced. It is shown that a formula $\alpha$ is provable in $P - W$ if and only if $\alpha$ is a type of some $\lambda$-term in this class. Hence these $\lambda$-terms represent proof figures in the Natural Deduction version of $P - W$. Errol Martin (1982) proved that no formula with form $\alpha \rightarrow \alpha$ is provable in $P - W$ without using the axiom $I$. We show that a $\beta$-normal form $\lambda$-term $M$ in the class is $\eta$ reducible to $\lambda x.x$ if the translated $BB'I$-combinator $M^+$ contains $I$. Using this theorem and Martin's result, we prove that a $\lambda$-term in the class is $\beta\eta$-reducible to $\lambda x.x$ if the $\lambda$-term has a type $\alpha \rightarrow \alpha$. Hence the structure of proofs of $\alpha \rightarrow \alpha$ in $P - W$ is determined. (shrink)

The mental fatigue elicited by working and studying consumed mental resources, thereby eliciting a declined performance and an increased mental stress. The long-term continuous work and study, which is typical for modern workers and students, can increase mental fatigue and health risks. Previous studies reported that the natural environment has a restorative of mental resources and reducing stress. However, it is difficult for urban workers and students to take sufficient breaks in real natural environment. We conducted an experiment to examine (...) whether brief and indirect exposure to the natural environment elicits a restorative of attention and reducing stress. Twenty-five undergraduate and graduate students from the university of modern city participated in the experiment. The experiment involved measuring the changes in the task performance of the participants and the subjective mental workload, while the attention restoration was indexed from physiological response over time. The participants had two types of resting periods in the middle of the task, i.e., by looking at a blank display or by watching a nature video having scenes of, e.g., a forest, small waterfall, and rustling leaves. The results indicate that the natural environment indirectly depicted through the nature videos does not affect the task performance and the subjective mental workload but decreases the SCL. The results of the physiological response suggest that having rest periods depicting the natural environment, even if indirectly and briefly, can restore the directed attention for the task. This experiment revealed a useful method of resting for urban workers and students to restore their attention to a task. (shrink)

In his paper, ìRight Weakening and Right Contraction in LK î, Hirokawa investigates the properties of the structural rules of contraction and weak- ening as they appear in a certain sequent calculus formulation of Örst order classical logic. In what follows we explore the notion of correspondence, in particular with reference to the structural rules in the succedent, and in doing so critically examine the sensitivity of Hirokawaís results to the formulation of the calculus, both with respect to the (...) formulations of the rules governing the connectives present and to the choice of the connectives themselves. (shrink)

We study a multiple-succedent sequent calculus with both of the structural rules Left Weakening and Left Contraction but neither of their counterparts on the right, for possible application to the treatment of multiplicative disjunction against the background of intuitionistic logic. We find that, as Hirokawa dramatically showed in a 1996 paper with respect to the rules for implication, the rules for this connective render derivable some new structural rules, even though, unlike the rules for implication, these rules are what (...) we call ipsilateral: applying such a rule does not make any formula change sides—from the left to the right of the sequent separator or vice versa. Some possibilities for a semantic characterization of the resulting logic are also explored. The paper concludes with three open questions. (shrink)