Kripke completeness of some infinitary predicate modal logics is presented. More precisely, we prove that if a normal modal logic above is -persistent and universal, the infinitary and predicate extension of with BF and BF is Kripke complete, where BF and BF denote the formulas pi pi and x x, respectively. The results include the completeness of extensions of standard modal logics such as , and its extensions by the schemata T, B, 4, 5, D, and their combinations. The proof (...) is obtained by extending the correspondence between the representation of modal algebras and the completeness of propositional modal logic to infinite. (shrink)

Predicate modal logics based on Kwith non-compact extra axioms are discussed and a sufficient condition for the model existence theorem is presented. We deal with various axioms in a general way by an algebraic method, instead of discussing concrete non-compact axioms one by one.

We give an extension of the Jónsson‐Tarski representation theorem for both normal and non‐normal modal algebras so that it preserves countably many infinite meets and joins. In order to extend the Jónsson‐Tarski representation to non‐normal modal algebras we consider neighborhood frames instead of Kripke frames just as Došen's duality theorem for modal algebras, and to deal with infinite meets and joins, we make use of Q‐filters, which were introduced by Rasiowa and Sikorski, instead of prime filters. By means of the (...) extended representation theorem, we show that every predicate modal logic, whether it is normal or non‐normal, has a model defined on a neighborhood frame with constant domains, and we give a completeness theorem for some predicate modal logics with respect to classes of neighborhood frames with constant domains. Similarly, we show a model existence theorem and a completeness theorem for infinitary modal logics which allow conjunctions of countably many formulas. (shrink)

In this article, a cut-free system TLMω1 for infinitary propositional modal logic is proposed which is complete with respect to the class of all Kripke frames.The system TLMω1 is a kind of Gentzen style sequent calculus, but a sequent of TLMω1 is defined as a finite tree of sequents in a standard sense. We prove the cut-elimination theorem for TLMω1 via its Kripke completeness.

Objectives: To analyse the decision making for end of life care for patients with cancer at a teaching hospital in Japan at two periods 10 years apart.Design and setting: Retrospective study conducted in a 550 bed community teaching hospital in Okinawa, Japan.Patients: There were 124 terminally ill cancer patients admitted either in 1989 and 1999 for end of life care with sufficient data to permit analysis.Main measurements: Basic demographic data, notification to the patient that he or she had cancer, patient (...) involvement in do not resuscitate orders, and various medical interventions which were performed in the month prior to the patient’s death were evaluated.Results: In 1989 none of the patients were notified of their diagnosis; in 1999 five patients were informed . Of the 113 patients with a written DNR order, none were involved in consenting to the DNR order. In the month before death, patients in both groups received non-palliative treatments such as feeding tube placements , total parenteral nutrition , and intravenous albumin infusion . Morphine use increased significantly in 1999 compared with the 1989 group.Conclusions: The majority of patients dying of cancer were still not informed of their diagnosis and were seldom involved in DNR decision making at a teaching hospital in Japan. There was no change in the number of potentially futile interventions that were performed but morphine use increased. Modern ethical education is urgently needed in Japanese medical practice to improve decision making process in the end of life care. (shrink)

It is known that for any subdirectly irreducible finite Heyting algebra A and any Heyting algebra, B, A is embeddable into a quotient algebra of B, if and only if Jankov's formula ${\rm{\chi A}}$ A for A is refuted in B. In this paper, we present an infinitary extension of the above theorem given by Jankov. More precisely, for any cardinal number ${\rm{\kappa }}$, we present Jankov's theorem for homomorphisms preserving infinite meets and joins, a class of subdirectly irreducible complete (...) ${\rm{\kappa }}$ - Heyting algebras and ${\rm{\kappa }}$ - infinitary logic, where a ${\rm{\kappa }}$ -Heyting algebra is a Heyting algebra A with ${\rm{\# A}} \le {\rm{\kappa }}$ and ${\rm{\kappa }}$ - infinitary logic is the infinitary logic such that for any set ${\rm{\Theta }}$ of formulas with ${\rm{\# \Theta }} \le {\rm{\kappa }}$ ⌈ Θ and ‷ Θ are well defined formulas. (shrink)

Little is known about health of the growing subpopulation of the working poor in Japan. We aimed to evaluate health status and healthcare utilization in relation to income among Japanese working adults. We conducted a one-month prospective cohort study using a health diary in working adults from a nationally representative random sample in Japan. Based on the government criterion, the working poor group was defined as earning an equivalent annual income of less than 1.48 million Japanese-yen. For health status, we (...) measured symptomatic episodes and health-related quality of life (HRQOL). For healthcare utilization, we measured frequencies of visits to a physician or pharmacy, and use of complementary and alternative medicine (CAM). We constructed multiple linear regression models for these measures adjusted for age, gender, and co-morbidity, using annual equivalent income as a 4-level categorical variable. (shrink)

The one-variable fragment of a first-order logic may be viewed as an “S5-like” modal logic, where the universal and existential quantifiers are replaced by box and diamond modalities, respectively. Axiomatizations of these modal logics have been obtained for special cases—notably, the modal counterparts $\mathrm {S5}$ and $\mathrm {MIPC}$ of the one-variable fragments of first-order classical logic and first-order intuitionistic logic, respectively—but a general approach, extending beyond first-order intermediate logics, has been lacking. To this end, a sufficient criterion is given in (...) this paper for the one-variable fragment of a semantically defined first-order logic—spanning families of intermediate, substructural, many-valued, and modal logics—to admit a certain natural axiomatization. More precisely, an axiomatization is obtained for the one-variable fragment of any first-order logic based on a variety of algebraic structures with a lattice reduct that has the superamalgamation property, using a generalized version of a functional representation theorem for monadic Heyting algebras due to Bezhanishvili and Harding. An alternative proof-theoretic strategy for obtaining such axiomatization results is also developed for first-order substructural logics that have a cut-free sequent calculus and admit a certain interpolation property. (shrink)

In the midst of globalization, English is regarded as an international language, or Lingua Franca, but learning it as a second language (L2) remains still difficult to speakers of other languages. This is true especially for the speakers of languages distantly related to English such as Japanese. In this sense, exploring neural basis for translation between the first language (L1) and L2 is of great interest. There have been relatively many previous researches revealing brain activation patterns during translations between L1 (...) and English as L2. These studies, which focused on language translation with close or moderate linguistic distance (LD), have suggested that the Broca area (BA 44/45) and the dorsolateral prefrontal cortex (DLPFC; BA 46) may play an important role on translation. However, the neural mechanism of language translation between Japanese and English, having large LD, has not been clarified. Thus, we used functional near infrared spectroscopy (fNIRS) to investigate the brain activation patterns during word translation between Japanese and English. We also assessed the effects of translation directions and word familiarity. All participants’ first language was Japanese and they were learning English. Their English proficiency was advanced or elementary. We selected English and Japanese words as stimuli based on the familiarity for Japanese people. Our results showed that the brain activation patterns during word translation largely differed depending on their English proficiency. The advanced group elicited greater activation on the left prefrontal cortex around the Broca’s area while translating words with low familiarity, but no activation was observed while translating words with high familiarity. On the other hand, the elementary group evoked greater activation on the left temporal area including the superior temporal gyrus (STG) irrespective of the word familiarity. These results suggested that different cognitive process could be involved in word translation corresponding to English proficiency in Japanese learners of English. These difference on the brain activation patterns between the advanced and elementary group may reflect the difference on the cognitive loads depending on the levels of automatization in one’s language processing. (shrink)

In this paper, we discuss semantical properties of the logic \(\textbf{GL}\) of provability. The logic \(\textbf{GL}\) is a normal modal logic which is axiomatized by the the Löb formula \( \Box (\Box p\supset p)\supset \Box p \), but it is known that \(\textbf{GL}\) can also be axiomatized by an axiom \(\Box p\supset \Box \Box p\) and an \(\omega \) -rule \((\Diamond ^{*})\) which takes countably many premises \(\phi \supset \Diamond ^{n}\top \) \((n\in \omega )\) and returns a conclusion \(\phi \supset (...) \bot \). We show that the class of transitive Kripke frames which validates \((\Diamond ^{*})\) and the class of transitive Kripke frames which strongly validates \((\Diamond ^{*})\) are equal, and that the following three classes of transitive Kripke frames, the class which validates \((\Diamond ^{*})\), the class which weakly validates \((\Diamond ^{*})\), and the class which is defined by the Löb formula, are mutually different, while all of them characterize \(\textbf{GL}\). This gives an example of a proof system _P_ and a class _C_ of Kripke frames such that _P_ is sound and complete with respect to _C_ but the soundness cannot be proved by simple induction on the height of the derivations in _P_. We also show Kripke completeness of the proof system with \((\Diamond ^{*})\) in an algebraic manner. As a corollary, we show that the class of modal algebras which is defined by equations \(\Box x\le \Box \Box x\) and \(\bigwedge _{n\in \omega }\Diamond ^{n}1=0\) is not a variety. (shrink)

Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same (...) consequence relations for a given spi-logic. (shrink)

In order to capture the concept of common knowledge, various extensions of multi-modal epistemic logics, such as fixed-point ones and infinitary ones, have been proposed. Although we have now a good list of such proposed extensions, the relationships among them are still unclear. The purpose of this paper is to draw a map showing the relationships among them. In the propositional case, these extensions turn out to be all Kripke complete and can be comparable in a meaningful manner. F. Wolter (...) showed that the predicate extension of the Halpern-Moses fixed-point type common knowledge logic is Kripke incomplete. However, if we go further to an infinitary extension, Kripke completeness would be recovered. Thus there is some gap in the predicate case. In drawing the map, we focus on what is happening around the gap in the predicate case. The map enables us to better understand the common knowledge logics as a whole. (shrink)

The release of AlphaFold2 (AF2), a deep‐learning‐aided, open‐source protein structure prediction program, from DeepMind, opened a new era of molecular biology. The astonishing improvement in the accuracy of the structure predictions provides the opportunity to characterize protein systems from uncultured Asgard archaea, key organisms in evolutionary biology. Despite the accumulation in metagenomics‐derived Asgard archaea eukaryotic‐like protein sequences, limited structural and biochemical information have restricted the insight in their potential functions. In this review, we focus on profilin, an actin‐dynamics regulating protein, (...) which in eukaryotes, modulates actin polymerization through (1) direct actin interaction, (2) polyproline binding, and (3) phospholipid binding. We assess AF2‐predicted profilin structures in their potential abilities to participate in these activities. We demonstrate that AF2 is a powerful new tool for understanding the emergence of biological functional traits in evolution. (shrink)