This paper presents proof that Buss's S22 can prove the consistency of a fragment of Cook and Urquhart's PV from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic S12. Our proof relies on the notion of "computation" of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved and either (...) its left- or right-hand side is computed, then there is a corresponding computation for its right- or left-hand side, respectively. By carefully computing the bound of the size of the computation, the proof of this theorem inside a bounded arithmetic is obtained, from which the consistency of the system is readily proven. This result apparently implies the separation of bounded arithmetic because Buss and Ignjatović stated that it is not possible to prove the consistency of a fragment of PV without induction but with substitution in Buss's S12. However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours. On the other hand, the system that we have considered is strictly equational, which is a property on which our proof relies. (shrink)

We extend Barbanera and Berardi's symmetric lambda calculus [2] to second-order classical propositional logic and prove its strong normalization.

We introduce an implication-free fragment image of ω-arithmetic, having Exchange rule for sequents dropped. Exchange rule for formulas is, instead, an admissible rule in image. Our main result is that cut-free proofs of image are isomorphic with recursive winning strategies of a set of games called “1-backtracking games” in [S. Berardi, Th. Coquand, S. Hayashi, Games with 1-backtracking, Games for Logic and Programming Languages, Edinburgh, April 2005].We also show that image is a sound and complete formal system for the implication-free (...) fragment of LCM , Seventh International Conference on Typed Lambda Calculi and Applications, in: Lecture Notes in Computer Science, vol. 3461, 2005, pp. 11–22. Invited paper]). A simple syntactical description of this fragment was still missing. No sound and complete formal system is known for LCM itself. (shrink)

This paper considers Rumfitt’s bilateral classical logic (BCL), which is proposed to counter Dummett’s challenge to classical logic. First, agreeing with several authors, we argue that Rumfitt’s notion of harmony, used to justify logical rules by a purely proof theoretical manner, is not sufficient to justify coordination rules in BCL purely proof-theoretically. For the central part of this paper, we propose a notion of proof-theoretical validity similar to Prawitz for BCL and proves that BCL is sound and complete respect to (...) this notion of validity. The major difficulty in defining validity for BCL is that validity of positive +A appears to depend on negative −A, and vice versa. Thus, the straightforward inductive definition does not work because of this circular dependance. However, Knaster-Tarski’s fixed point theorem can resolve this circularity. Finally, we discuss the philosophical relevance of our work, in particular, the impact of the use of fixed point theorem and the issue of decidability. (shrink)

Researchers typically use the “big five” traits as a standard way to describe personality. Evaluation of personality is generally conducted using self-report questionnaires that require participants to respond to a large number of test items. To minimize the burden on participants, this paper proposes an alternative method of estimating multidimensional personality traits from only a single word. We constructed a system that can convert a sound-symbolic word that intuitively expresses personality traits into information expressed by 50 personality-related adjective pairs. This (...) system can obtain information equivalent to the adjective scales using only a single word instead of asking many direct questions. To achieve this, we focused on SSWs in Japanese that have the association between linguistic sounds and meanings and express diverse and complex aspects of personality traits. We evaluated the prediction accuracy of the system and found that the multiple correlation coefficients for 48 personality-related adjective pairs exceeded 0.75, indicating that the model could explain more than half of the variations in the data. In addition, we conducted an evaluation experiment in which participants rated the appropriateness of the system output using a seven-point scale. The average score for 50 personality-related adjective pairs was 1.25. Thus, we believe that this system can contribute to the field of personality computing, particularly in terms of personality evaluation and communication. (shrink)

誕生から今日まで、文芸・演劇が芸術に占める位置ばどう変わっているのか?古今東西の具体的な動きに即しつつ、類型論的・理論的パースペクティブを示す。.

Detection of genuine altruists could be a solution to the problem of subtle cheating. Brown et al. (Evol Psychol 1:42–69, 2003) found that humans could detect altruists using nonverbal cues. However, their experiments can be improved upon in several ways, and further investigation is needed to determine whether altruist-detection abilities are human universals. In our experiment, we used video clips of natural conversations as the stimulus. We asked a sample of Japanese undergraduates to rate their own level of altruism and (...) then to estimate the videotaped targets’ altruism using the same scale. The perceivers were able to estimate the targets’ altruism levels accurately. Perceivers’ altruism score did not affect their ability to discriminate between altruists and non-altruists. Perceivers’ impressions of the altruist and non-altruist targets were also found to be different. Coding of nonverbal behavior of the targets revealed that altruists exhibited more “felt smiles” than non-altruists, which also supports the results of the previous study. (shrink)

ναξ and βασιλες are the two most important titles applied to the top stratum of Homeric aristocracy., usually translated as ′lord′ or ′master′, and βασιλες, usually translated as ′king′, often apply to the same individuals, and can at times appear to be very close in meaning, allowing translators to render ναξ as ′king′ and βασιλες as ′lord′. There are, however, significant differences between the two. As Lexikon des friihgriechischen Epos now conveniently summarizes for us, avat; can be divine or human, (...) can be a master of a state, of gods, of men, of animals, or of his household, and can be used as an address in the vocative, whereas fiaoiXevs is only applied to humans in Homer, often in a political context, and is never used in the vocative. (shrink)

Phoenix's speech in Book 9 of the Iliad is generally considered prophetic of what happens to Achilles later in the story. Many scholars have argued that Achilles is punished by Zeus through τη which causes the death of Patroclus, just as anyone who spurns the Litai in the allegory of Phoenix will be punished by Ate sent by Zeus. The Meleager episode is also regarded as reflecting almost exactly what happens later: the Achaeans have difficulty in the battle due to (...) Achilles' withdrawal, just as the Aetolians have when Meleager refuses to fight. Achilles, like Meleager, receives a set of three supplications to go back to the battle, and, just as Meleager loses his prize because he rejects the supplications, Achilles loses Patroclus because he does not listen to the pleas of the Embassy. This seems to be, in outline, the present orthodoxy. (shrink)

When making decisions, people tend to overweigh the impact of losses compared to gains, a phenomenon known as loss aversion. A moderate amount of LA may be adaptive as it is necessary for protecting oneself from danger. However, excessive LA may leave people few opportunities and ultimately lead to suboptimal outcomes. Despite frequent reports of elevated LA in specific populations such as patients with depression, little is known about what psychological characteristics are associated with the tendency of LA. Based on (...) the neurobiological studies of LA, we hypothesized that positive psychological wellbeing may be negatively associated with people's tendency of LA. In the present study, we set out to test this hypothesis in a sample of young adults. We evaluated LA using a decision-making task in which subjects were asked to decide whether to accept or reject a series of coin-toss gambles. Our results revealed that individuals with more advanced personal growth as assessed by the Ryff's Psychological Well-being Inventory showed reduced LA. To our knowledge, this is the first report demonstrating an association between positive psychological wellbeing and LA. These findings suggest that personal growth might be employed as interventional targets for correcting excessive LA in vulnerable populations. (shrink)

ναξ and βασιλες are the two most important titles applied to the top stratum of Homeric aristocracy., usually translated as ′lord′ or ′master′, and βασιλες, usually translated as ′king′, often apply to the same individuals, and can at times appear to be very close in meaning, allowing translators to render ναξ as ′king′ and βασιλες as ′lord′. There are, however, significant differences between the two. As Lexikon des friihgriechischen Epos now conveniently summarizes for us, avat; can be divine or human, (...) can be a master of a state, of gods, of men, of animals, or of his household, and can be used as an address in the vocative, whereas fiaoiXevs is only applied to humans in Homer, often in a political context, and is never used in the vocative. (shrink)

Cet article a pour but de développer le théme qui a été lamcé dans mon article précédent :"Le corps comme événement" , où l'on a considéré le corps comme centre des sensations. Le corps comme lieu des désaccords et discords est en même temps lieu des événements et de la naissance des sensations. À propos de l'oevre d'art, on dit parfois le style de l'artiste, de l'ecole et du temps. Cela est possible, parce que l'oeuvre d'art, elle a aussi un (...) corps. Or la création de l'oeuvre par l'artiste est un événement et notre rencontre avec l'oeuvre l'est aussi. À ce moment, non seulement les relations entre l'artiste et l'ouvre, et l'ouvre et nous, mias celle-même entre nous et l'artiste est réciproque. Cette r6eacute;ciprocité est le plus important des indices de l'événement. (shrink)

Phoenix's speech in Book 9 of the Iliad is generally considered prophetic of what happens to Achilles later in the story. Many scholars have argued that Achilles is punished by Zeus through τη which causes the death of Patroclus, just as anyone who spurns the Litai in the allegory of Phoenix will be punished by Ate sent by Zeus. The Meleager episode is also regarded as reflecting almost exactly what happens later: the Achaeans have difficulty in the battle due to (...) Achilles' withdrawal, just as the Aetolians have when Meleager refuses to fight. Achilles, like Meleager, receives a set of three supplications to go back to the battle, and, just as Meleager loses his prize because he rejects the supplications, Achilles loses Patroclus because he does not listen to the pleas of the Embassy. This seems to be, in outline, the present orthodoxy. (shrink)