This paper shows that the inhabitation problem in the lambda calculus with negation, product, polymorphic, and existential types is decidable, where the inhabitation problem asks whether there exists some term that belongs to a given type. In order to do that, this paper proves the decidability of the provability in the logical system defined from the second-order natural deduction by removing implication and disjunction. This is proved by showing the quantifier elimination theorem and reducing the problem to the provability in (...) propositional logic. The magic formulas are used for quantifier elimination such that they replace quantifiers. As a byproduct, this paper also shows the second-order witness theorem which states that a quantifier followed by negation can be replaced by a witness obtained only from the formula. As a corollary of the main results, this paper also shows Glivenko’s theorem, Double Negation Shift, and conservativity for antecedent-empty sequents between the logical system and its classical version. (shrink)

I examine the tension between biopolitics and necropolitics through three themes that I have perceived and that are related to my life in Japan. First, I examine the transformation of hospitals and medical care, particularly for the elderly, through my experience of sharing the end of my mother’s life. Modern medicine has made great achievements in treating diseases that used to be fatal, but it has become institutionalized in the context of Big Pharma interests, with no insight into the natural (...) ageing and death of human beings. Second, I discuss how the ecological worldview on parasitism and symbiosis has been distorted by industrial logic, drawing on the work of my esteemed friend and parasitologist Professor Koichiro Fujita, who passed away in 2021. Finally, with regard to the Covid-19 pandemic, I would argue that it is not a sudden phenomenon triggered by a new virus, but in a sense a disaster that has been prepared for decades and must be seen as a war using bioengineering and epidemiology as weapons, rather than tanks and bombs. (shrink)

dai 1-kan. Ningen, kyōiku ga umarekawaru tame -- dai 2-kan. Ningen to no deai, kyōiku to no deai -- dai 3 kan. Ningenrashiku naru tedate -- dai 4-kan. Jinrui no kibō, osanago -- dai 5-kan. Shishū, ushinawareta kisetsu o motomete -- dai 6-kan. Aru mazushiki shōgai no kiroku -- [7] Kyōiku to kyōikugaku.

We provide a natural extension of the intuitionistic natural deduction system NJ with at most two consequences, which we call a binary conclusion natural deduction system. The classical natural deduction system NK is defined as NJ together with the law of the excluded middle or the double negation principle. However, in contrast to NK, the new BCN system has no such classical rule, but has two kinds of rules managing two consequences. One is to eliminate one consequence and the other (...) is to introduce another consequence. Except on this point, BCN proofs are derived in exactly the same way as those in NJ. It is shown that with respect to the propositional fragment of NK, the BCN system is sound and sufficiently complete to prove classical propositional theorems. Moreover, as a corollary we obtain a general form of Glivenko's theorem and disjunction property for one of the two consequences. We also show the normalization theorem for BCN. Finally, we study some extensions of BCN to classical predicate logic. (shrink)

There is an intimate connection between proofs of the natural deduction systems and typed lambda calculus. It is well-known that in simply typed lambda calculus, the notion of formulae-as-types makes it possible to find fine structure of the implicational fragment of intuitionistic logic, i.e., relevant logic, BCK-logic and linear logic. In this paper, we investigate three classical substructural logics (GL, GLc, GLw) of Gentzen's sequent calculus consisting of implication and negation, which contain some of the right structural rules. In terms (...) of Parigot's -calculus with proper restrictions, we introduce a proof term assignment to these classical substructural logics. According to these notions, we can classify the -terms into four categories. It is proved that well-typed GLx--terms correspond to GLx proofs, and that a GLx--term has a principal type if stratified where x is nil, c, w or cw. Moreover, we investigate embeddings of classical substructural logics into the corresponding intuitionistic substructural logics. It is proved that the Gödel-style translations of GLx--terms are embeddings preserving substructural logics. As by-products, it is obtained that an inhabitation problem is decidable and well-typed GLx--terms are strongly normalizable. (shrink)

A proof is given for the theorem that at least one bound state exists in a one-dimensional attractive potential however weak it may be. The proof is constructive in that it provides a method to explicitly solve the eigenvalue problem for the eigenvalues as well as the eigenfunctions. The method is well suited to precise numerical calculations.

It has been reported as a robust effect that people are likely to select a matching case in the Wason selection task. For example, they usually select the 5 case, in the Wason selection task with the conditional "if an E, then a not-5". This was explained by the matching bias account that people are likely to regard a matching case as relevant to the truth of the conditional (Evans, 1998). However, because a positive concept usually constructs a smaller set (...) than its negative one does (a rarity assumption), it is more effective to get information on the truth of the conditional in a positive set than in a negative set. Thus the optimal data selection account can also explain the effect. The set size of Q and matching by introducing negation were manipulated independently in four experiments. From the results it was inferred that the so-called matching bias was an amalgam of two different cognitive components-relevance judgement by matching and optimal data selection. (shrink)

In this paper, we study the relationship among classical logic, intuitionistic logic, and quantum logic . These logics are related in an interesting way and are not far apart from each other, as is widely believed. The results in this paper show how they are related with each other through a dual intuitionistic logic . Our study is completely syntactical.

Sehen und Sagen sind untrennbar. Diese Untrennbarkeit ist ein wesentlicher, aber bisher nicht so beachteter Streitpunkt der Fichtes WL. Das Sagen ist für Fichte wesentlich. Dies ist deutlich, wenn man darauf achtet, dass es in enger Beziehung zu dem Sehen steht.

『日本唯物論史』などで知られるわが国の唯物論哲学の開拓者・永田廣志の生涯をまとめ、その理論活動の意義を解明。哲学研究者と在野の郷土史家との共同研究が生み出した成果。本邦初公開の貴重な資料や秘蔵写真も多 数紹介。.

The present work, which was inspired by Kripke and McCarthy, is about a non-classical predicate logic system containing a truth predicate symbol. In this system, each sentence A is referred to not by a Gödel number but by its quotation name 'A'.

Minami–Sakai :883–898, 2016) investigated the cofinal types of the Katětov and the Katětov–Blass orders on the family of all \ ideals. In this paper we discuss these orders on analytic P-ideals and Borel ideals. We prove the following:The family of all analytic P-ideals has the largest element with respect to the Katětov and the Katětov–Blass orders.The family of all Borel ideals is countably upward directed with respect to the Katětov and the Katětov–Blass orders. In the course of the proof of (...) the latter result, we also prove that for any analytic ideal \ there is a Borel ideal \ with \. (shrink)

We investigate how weak square principles are denied by Chang’s Conjecture and its generalizations. Among other things we prove that Chang’s Conjecture does not imply the failure of \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\square_{\omega_1, 2}}$$\end{document}, i.e. Chang’s Conjecture is consistent with \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\square_{\omega_1, 2}}$$\end{document}.

Using simple stochastic models, we discuss how cooperative breeders, especially wasps and bees, can improve their productivity by reducing foraging work. In a harsh environment, where foraging is the main cause of mortality, such breeders achieve greater productivity by reducing their foraging effort below full capacity, and they may thrive by adopting cooperative breeding. This could prevent the population extinction of cooperative breeders under conditions where a population of lone breeders cannot be maintained.

Nisbett et al. claim that East Asians are likely to use holistic thought to solve problems, whereas Westerners use analytic thought more, and discuss the differences in the frame of the individualism/collectivism distinction. The holistic versus analytic distinction has been the greatest point of interest of dual process theories, which imply that human thinking has two sub processes. We apply a revised dual process model that proposes meme-acquired goals in both systems to explain cultural differences in thought. According to this, (...) gene-installed goals are universal across cultures, whereas meme-acquired goals depend upon culture. To introduce a dual process model means that we discuss adaptation both in terms of culture and natural selection. Hence, we propose an interactive view that supports an adaptive relation between mind and culture. (shrink)

dai 1-kan. Hōgaku no kiso riron -- dai 2-kan. Gendai hōgaku no taikei. Kōhō, shakaihō -- dai 3-kan. Gendai hōgaku no taikei. Shihō, gaikokuhō.

Yama (2001) argued that the matching bias effect was an amalgam of a genuine matching effect and a set size effect. However, Evans (2002) pointed out some problems with Yama's argument. One was on the matching index used in Yama (2001). The others concerned a gap between Yama's (2001) interpretation of matching bias and Evans' (1998) recent discussions that had placed emphasis on the problem of implicit negation. I reply to these claims taking Oaksford (2002) into consideration. Further, I propose (...) a framework connecting context, goal, utility, and relevance, and including a hierarchical structure of goals. I argue that theories of reasoning can be developed and extended with the framework. (shrink)

This paper presents a new method that improves robustness of real-coded Genetic Algorithm (GA) for function optimization. It is reported that most of crossover operators for real-coded GA have sampling bias, which prevents to find the optimum when it is near the boundary of search space. They like to search the center of search space much more than the other. Therefore, they will not work on functions that have their optima near the boundary of the search space. Although several methods (...) have been proposed to relax this sampling bias, they could not cancel whole bias. In this paper, we propose a new method, Toroidal Search Space Conversion (TSC), to remove this sampling bias. TSC converts bounded search space into toroidal one without any parameter. Experimental results show that a GA with TSC has higher performance to find the optimum near the boundary of search space and the GA has more robustness concerning the relative position of the optimum. (shrink)

新しい社会科学の構築へ。来たるべき社会の基礎となる社会科学的方法論の課題を、第一線で活躍する十二名が「思想学」の観点から論じる。自由思想、啓蒙思想から神学、経済学まで多彩な視座より先哲の歩みを分析し、 思想研究の未来を探る充実の書。.

The mitogenic action of cytokines such as epidermal growth factor (EGF)d̊ or platelet dericed growth factor (PDGF) involves the stimulation of a signal cascade controlled by a small G protein called Ras. Mutations of Ras can cause its constitutive activation and, as a consequence, bypass the regulation of cell growth by cytokines. Both growth factor‐induced and oncogenic activation of Ras involve the conversion of Ras from the GDP‐bound (D‐Ras) to the GTP‐bound (T‐Ras) forms. T‐Ras activates a network of protein kinases (...) including c‐Mos, c‐Raf‐1 and MAP kinase. Eventually the activation of MAP kinase leads to the activation of the elongation factor 4E and several transcription factors such as c‐Jun, c‐Myc and c‐Fos. There are several modulators of Ras activity, such as the GTPase activating proteins (GAP1 and NF1), which stimulate the coversion of T‐Ras to D‐Ras. A series of small NF1 fragments, which bind T‐Ras, as well as truncated forms or derivatives of c‐Raf‐1, c‐Jun and c‐Myc, are capable of blocking the T‐Ras‐activated mitogenesis in a competitive manner. These agents offer a unique opportunity to control the proliferation of T‐Ras‐associated tumors, which represent more than 30% of total human carcinomas. (shrink)