We show that every MALL proof-structure [9] satisfies the property of softness, originally a categorical notion introduced by Joyal. Furthermore, we show that the notion of hereditary softness precisely captures Girard’s algebraic restriction of the technical condition on proof-structures. Relying on this characterization, we prove a MALL+Mix sequentialization theorem by a proof-theoretical method, using Girard’s notion of jump. Our MALL+Mix correctness criterion subsumes the Danos/Fleury-Retoré criterion [6] for MLL+Mix.

We shall give a direct proof of the independence result of a Buchholz style-Hydra Game on labeled finite trees. We shall show that Takeuti-Arai's cut-elimination procedure of $(\Pi^{1}_{1}-CA) + BI$ and of the iterated inductive definition systems can be directly expressed by the reduction rules of Buchholz's Hydra Game. As a direct corollary the independence result of the Hydra Game follows.

We first note that Gentzen's proof-reduction for his consistency proof of PA can be directly interpreted as moves of Kirby-Paris' Hydra Game, which implies a direct independence proof of the game . Buchholz's Hydra Game for labeled hydras is known to be much stronger than PA. However, we show that the one-dimensional version of Buchholz's Game can be exactly identified to Kirby-Paris' Game , by a simple and natural interpretation . Jervell proposed another type of a combinatorial game, by abstracting (...) Gentzen's proof-reductions and showed that his game is independent of PA. We show that this Jervell's game is actually much stronger than PA, by showing that the critical ordinal of Jervell's game is φω = ϵ0) in the Veblen hierarchy of ordinals. (shrink)

We prove that the full completeness theorem for MLL+Mix holds by the simple interpretation via formulas as objects and proofs as Z-invariant morphisms in the *-autonomous category of topologized vector spaces. We do this by generalizing the recent work of Blute and Scott 101–142) where they used the semantical framework of dinatural transformation introduced by Girard–Scedrov–Scott , Logic from Computer Science, vol. 21, Springer, Berlin, 1992, pp. 217–241). By omitting the use of dinatural transformation, our semantics evidently allows the interpretation (...) of the cut-rule, while the original Blute–Scott's does not. Moreover, our interpretation for proofs is preserved automatically under the cut elimination procedure. In our semantics proofs themselves are characterized by the concrete algebraic notion “Z-invariance”, and our denotational semantics provides the full completeness. Our semantics is naturally extended to the full completeness semantics for CyLL+Mix owing to an elegant method of Blute–Scott 1413–1436) 101–142))). (shrink)

This paper presents a polarized phase semantics, with respect to which the linear fragment of second order polarized linear logic of Laurent [15] is complete. This is done by adding a topological structure to Girard's phase semantics [9]. The topological structure results naturally from the categorical construction developed by Hamano—Scott [12]. The polarity shifting operator ↓ (resp. ↑) is interpreted as an interior (resp. closure) operator in such a manner that positive (resp. negative) formulas correspond to open (resp. closed) (...) facts. By accommodating the exponentials of linear logic, our model is extended to the polarized fragment of the second order linear logic. Strong forms of completeness theorems are given to yield cut-eliminations for the both second order systems. As an application of our semantics, the first order conservativity of linear logic is studied over its polarized fragment of Laurent [16]. Using a counter model construction, the extension of this conservativity is shown to fail into the second order, whose solution is posed as an open problem in [16]. After this negative result, a second order conservativity theorem is proved for an eta expanded fragment of the second order linear logic, which fragment retains a focalized sequent property of [3]. (shrink)

In this paper, we present a categorical model for Multiplicative Additive Polarized Linear Logic , which is the linear fragment of Olivier Laurent’s Polarized Linear Logic. Our model is based on an adjunction between reflective/coreflective full subcategories / of an ambient *-autonomous category . Similar structures were first introduced by M. Barr in the late 1970’s in abstract duality theory and more recently in work on game semantics for linear logic. The paper has two goals: to discuss concrete models and (...) to present various completeness theorems.As concrete examples, we present a hypercoherence model, using Ehrhard’s hereditary/anti-hereditary objects, a Chu-space model, a double gluing model over our categorical framework, and a model based on iterated double gluing over a *-autonomous category.For the multiplicative fragment of. (shrink)

We prove a full completeness theorem for multiplicative–additive linear logic using a double gluing construction applied to Ehrhard’s *-autonomous category of hypercoherences. This is the first non-game-theoretic full completeness theorem for this fragment. Our main result is that every dinatural transformation between definable functors arises from the denotation of a cut-free proof. Our proof consists of three steps. We show:• Dinatural transformations on this category satisfy Joyal’s softness property for products and coproducts.• Softness, together with multiplicative full completeness, guarantees that (...) every dinatural transformation corresponds to a Girard proof-structure.• The proof-structure associated with any dinatural transformation is a proof-net, hence a denotation of a proof. This last step involves a detailed study of cycles in additive proof-structures.The second step is a completely general result, while the third step relies on the concrete structure of a double gluing construction over hypercoherences. (shrink)

Painless civilization is a term I coined in my Japanese book of the same title, which was published in 2003. Contemporary civilization aims to provide pleasure and comfort and eliminate pain and suffering as much as possible. This is especially evident in advanced countries. Contemporary civilization is moving toward a painless civilization. However, in a painless civilization, we are deprived of the joy of life, which is considered a fundamental source of meaning in life, and we are led toward the (...) situation of drowning in a sea of pleasure. This is a kind of dystopia, and we cannot find an easy way to escape from it. It is important to pay special attention to this aspect of contemporary civilization when we think about the future of our planet. (shrink)

In this paper, the concept of birth affirmation is clarified in both the psychological dimension and the philosophical dimension. In the psychological dimension, we propose two interpretations: 1) Possible world interpretation: Even if I could imagine a possible world in which my ideal was realized or my grave sufferings were resolved, I would never think, at the bottom of my heart, that it would have been better to have been born to that possible world. 2) Anti-antinatalistic interpretation: I would never (...) think, at the bottom of my heart, that it would have been better not to have been born. In the philosophical dimension, we propose the following interpretation: The comparison of betterness or worseness between the actual world and a possible world and between my having been born and my not having been born should be impossible. In the final part of this paper, the differences from other related concepts and frequently asked questions are discussed. (shrink)

One prominent feature of belief is that a belief cannot be formed at will. This paper argues that the best explanation of this fact is that belief formation is a process that takes aim at the truth. Taking aim at the truth is to be understood as causal responsiveness of the processes constituting belief formation to what facilitates achieving true beliefs. The requirement for this responsiveness precludes the possibility of belief formation responding to intentions in a way that would count (...) as forming a belief at will. (shrink)

In this paper, I make two arguments: 1) There is a solipsistic layer in meaning in life, which I call the “heart of meaning in life” (HML). The bearer of the heart of meaning in life is the solipsistic being. The heart of meaning in life cannot be compared with anything else whatsoever. 2) The heart of meaning in life can be dynamically incorporated into the affirmation of having been born into this world, which I call “birth affirmation.” There can (...) be two interpretations of birth affirmation, the anti-anti-natalistic interpretation and the possible world interpretation. Birth affirmation can be an alternative to anti-natalism, which is destined to be frustrated in this universe. (shrink)

Abstract -/- In 1998, the Council for Science and Technology established the Bioethics Committee and asked its members to examine the ethical and legal aspects of human cloning. The Committee concluded in 1999 that human cloning should be prohibited, and, based on the report, the government presented a bill for the regulation of human cloning in 2000. After a debate in the Diet, the original bill was slightly modified and issued on December 6, 2000. In this paper, I take a (...) closer look at this process and discuss some of the ethical problems that were debated. Also, I make a brief analysis of the concept “the sprout of human life.” Not only people who object to human cloning, but also many of those who seek to promote research on human cloning admit that a human embryo is the sprout of human life and, hence, it should be highly respected. I also discuss the function of the language of utilitarianism, the language of skepticism, and religious language appeared in the discussion of human cloning in Japan. (shrink)

Determining the relationship between the entire brain structure and individual differences is important in extending healthy life expectancy, which can be affected by brain atrophy. The entire brain structure has been gradually known to be correlated not only with age but also with individual differences, such as quality of life, general intelligence, and lifestyle. However, little attention has been paid to the relationship between the entire brain structure and personal traits. We herein focused on one personal trait, namely spiritual growth, (...) and examined its relationship with the entire brain structure using two neuroimaging-derived measures, namely the gray matter Brain Healthcare Quotient, a measure of GM volume, and the fractional anisotropy Brain Healthcare Quotient, a measure of white matter integrity, in 229 healthy participants. The results indicated no significant relationship between the GM-BHQ and spiritual growth, but there was a significant positive correlation between the FA-BHQ and spiritual growth after controlling for age, sex, and body mass index with partial correlation analysis. Furthermore, multiple regression analysis revealed a significant positive correlation between the FA-BHQ and spiritual growth after controlling for physical characteristics, such as age, sex, and BMI, as well as other variables related to lifestyle that were collected using the Health-Promoting Lifestyle Profile. These results support the idea that there is a relationship between the entire WM brain structure and spiritual growth. Further studies are required to clarify the causal relationship between the entire WM brain structure and spiritual growth with some interventions to improve spiritual growth. Such studies will help extend healthy life expectancy from a new perspective of personal trait. (shrink)

A tactile record and playback system will progress _tactileology_—a new cross-disciplinary field related to tactile sensations—as it will enhance its use in the instruction, archiving, and analysis of human manipulation. In this paper, we describe two key devices for achieving tactileology: a tactile sensor capturing human tactile sense (fingernail color sensor) and a robotic tactile sensor, both of which can detect not only normal force but also tangential force. This is beneficial because people manipulate objects and tools in various ways, (...) such as grasping, picking, and rubbing. The fingernail color sensor registers the three-dimensional (3D) force applied to a fingertip by detecting the fingernail color change caused by blood distribution under the fingernail, which can be observed with green illumination and a miniature camera. Since detecting this color change is more complicated than using a robotic sensor, the relationships between the image and 3D force are learned using a convolutional neural network (CNN). In the robotic sensor, the 3D force applied to a robotic finger transforms into a bright area using an illuminated acrylic core, a rubber robotic finger skin, and a miniature camera. We measure normal force and tangential force by the brightness and movement of the bright area, respectively. Using a force gauge or an electronic scale for measurement, we perform a series of evaluation experiments. The experimental results show that the precision of both the fingernail color sensor and the robotic tactile sensor are sufficient for our system. (shrink)

We introduce the Easton collapse and show that the two-stage iteration of Easton collapses gives a model in which the successor of a regular cardinal carries a strongly saturated filter. This allows one to get a model in which many successor cardinals carry saturated filters just by iterating Easton collapses.

Many cultures have had knowledge imposed from outside, whether by force or for reasons of power, to the detriment of their own endogenous knowledge and the wisdom developed throughout their history. Would Japan’s acquisition of Western knowledge have led but to the development of a lesser know-how, devoid of meaning or sense, or even of knowledge which it might be better to ignore? Far from benefiting from an endogenous development or a modernization respectful of beings and of their environment, the (...) developing countries that superficially adopt this unilateral knowledge undergo a type of ‘self-colonization’. Although concurring with biologist Keiko Nakamura’s theory that scientific attitudes must be studied from within, Masahiro Hamashita considers that knowledge from outside allows for more solid internal reflection. He thus advocates the development of an integrated, hybrid knowledge, where external knowledge is mixed with internal knowledge in a spontaneous, harmonious way, as was the case with the traditional knowledge that Japan acquired from China. (shrink)

Yanagita Kunio (1875-1962), one of the most representative of Japanese folklorists, sees the different aspects of forests as a composite whole comprising customs, legends and way of life of the inhabitants. Yanagita looks at this in detail, wishing to understand how the forest is related to the life and customs of the people living there, an attitude that could be called an understanding from within. Given the complexity of the issue of the earth’s ecology, Yanagita suggests adopting the same attitude.

A change of gaze behavior at a small mistake moment is a natural response that reveals our own mistakes and suggests an apology to others with whom we are working or interacting. In this paper we investigate how robot gaze behaviors at small mistake moments change the impressions of others. To prepare gaze behaviors for a robot, first, we identified by questionnaires how human gaze behaviors change in such situations and extracted three kinds: looking at the other, looking down, and (...) looking away. We prepared each gaze behavior, added a no-gaze behavior, and investigated how a robot’s gaze behavior at a small mistake moment changes the impressions of the interacting people in a simple cooperative task. Experiment results show that the ‘looking at the other’ gaze behavior outperforms the other gaze behaviors and indicates the degrees of perceived apologeticness and friendliness. Keywords: Communication robots; gaze; mistake; mitigation. (shrink)

We give an extender characterization of a very strong elementary embedding between transitive models of set theory, whose existence is known as the axiom I2. As an application, we show that the positive solution of a partition problem raised by Magidor would refute it.