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 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)

History of philosophical thought of Vietnam up to XX century.

On the Yin-yang, Chinese philosophy, and oral tradition in Mongolia.

The aim of this paper is to give a characterisation of religion and the Religious Spirit, basing itself on the Platonic assumption that there are Forms, salient jewels of simplicity and affinity, to be dug out from the soil of vague experience and cut clear from the confusedly shifting patterns of usage, which will give us conceptual mastery over the changeable detail in a given sector. It will further be Platonic in that it will not seek to discount the deep (...) gulfs between the species into which religion qua genus divides itself, i.e. its theistic, polytheistic and atheistic subvarieties, taking it to be of the essence of a true genus to extend itself over mutually exclusive species, only being what it is by including in its sense the alternatives which are thus mutually exclusive. And my treatment will be Platonic, thirdly, in that it will endeavour to delimit the Religious Spirit by, on the one hand, setting it over against what it excludes, all purely this-world talk and life which is quite irreligious, and by, on the other hand, opposing it to forms of talk and life which fall short of it in various ways or which deviate from it variously, thereby likewise contributing to our understanding of what it is. The practice of Plato, which could study the deviations from his ideal city in order to confirm his notion of its structure and excellence, and which also paired every ideal pattern with its opposite— piety with impiety, justice with self-interested tyranny, etc.—is plainly one to be followed: Plato, as we know from a citation from his contemporary Hermodorus in one of the Aristotelian commentators, always set beside the ‘in itself’ of the pure Form the deviant and the wholly negative which were nonetheless part of its sense. Religion will therefore stand before us as a target that it is possible to fall short of or miss altogether as well as to hit squarely, and we shall try by a series of glancing darts to end by hitting it squarely. (shrink)

On Islamic teachings, written by an army officer and educationist from Pakistan.

Ancient treatise on Sankhya philosophy; Sanskrit text with English and Oriya translation and interpretation.

On study and teaching of aesthetics in Vietnam.

Dictionary of Nyaya terminology ; English and Sanskrit interpretation.