We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes $\mathrm {B}$, $\Delta (\mathrm {B})$, and $\Sigma (\mathrm {B})$ of formulas of modal arithmetic and study basic properties of them. Then, we prove several implications between the properties. In particular, among other things, we prove that for any consistent recursively enumerable extension T of $\mathbf {PA}(\mathbf {K})$ with $T \nvdash \Box \bot $, the $\Sigma (\mathrm {B})$ -disjunction property, the (...) $\Sigma (\mathrm {B})$ -existence property, and the $\mathrm {B}$ -existence property are pairwise equivalent. Moreover, we introduce the notion of the $\Sigma (\mathrm {B})$ -soundness of theories and prove that for any consistent recursively enumerable extension of $\mathbf {PA}(\mathbf {K4})$, the modal disjunction property is equivalent to the $\Sigma (\mathrm {B})$ -soundness. (shrink)

We investigate relationships between versions of derivability conditions for provability predicates. We show several implications and non-implications between the conditions, and we discuss unprovability of consistency statements induced by derivability conditions. First, we classify already known versions of the second incompleteness theorem, and exhibit some new sets of conditions which are sufficient for unprovability of Hilbert–Bernays’ consistency statement. Secondly, we improve Buchholz’s schematic proof of provable $\Sigma_1$ -completeness. Then among other things, we show that Hilbert–Bernays’ conditions and Löb’s conditions are (...) mutually incomparable. We also show that neither Hilbert–Bernays’ conditions nor Löb’s conditions accomplish Gödel’s original statement of the second incompleteness theorem. (shrink)

We prove that for any recursively axiomatized consistent extension T of Peano Arithmetic, there exists a \ provability predicate of T whose provability logic is precisely the modal logic \. For this purpose, we introduce a new bimodal logic \, and prove the Kripke completeness theorem and the uniform arithmetical completeness theorem for \.

We study modal completeness and incompleteness of several sublogics of the interpretability logic. We introduce the sublogic, and prove that is sound and complete with respect to Veltman prestructures which are introduced by Visser. Moreover, we prove the modal completeness of twelve logics between and with respect to Veltman prestructures. On the other hand, we prove that eight natural sublogics of are modally incomplete. Finally, we prove that these incomplete logics are complete with respect to generalized Veltman prestructures. As a (...) consequence of these investigations, we obtain that the twenty logics studied in this paper are all decidable. (shrink)

We prove that for each recursively axiomatized consistent extension T of Peano Arithmetic and \, there exists a \ numeration \\) of T such that the provability logic of the provability predicate \\) naturally constructed from \\) is exactly \ \rightarrow \Box p\). This settles Sacchetti’s problem affirmatively.

It is widely considered that Gödel’s and Rosser’s proofs of the incompleteness theorems are related to the Liar Paradox. Yablo’s paradox, a Liar-like paradox without self-reference, can also be used to prove Gödel’s first and second incompleteness theorems. We show that the situation with the formalization of Yablo’s paradox using Rosser’s provability predicate is different from that of Rosser’s proof. Namely, by using the technique of Guaspari and Solovay, we prove that the undecidability of each instance of Rosser-type formalizations of (...) Yablo’s paradox for each consistent but not Σ1-sound theory is dependent on the choice of a standard proof predicate. (shrink)

Akama et al. [1] systematically studied an arithmetical hierarchy of the law of excluded middle and related principles in the context of first-order arithmetic. In that paper, they first provide a prenex normal form theorem as a justification of their semi-classical principles restricted to prenex formulas. However, there are some errors in their proof. In this paper, we provide a simple counterexample of their prenex normal form theorem [1, Theorem 2.7], then modify it in an appropriate way which still serves (...) to largely justify the arithmetical hierarchy. In addition, we characterize a variety of prenex normal form theorems by logical principles in the arithmetical hierarchy. The characterization results reveal that our prenex normal form theorems are optimal. For the characterization results, we establish a new conservation theorem on semi-classical arithmetic. The theorem generalizes a well-known fact that classical arithmetic is $\Pi _2$ -conservative over intuitionistic arithmetic. (shrink)

We investigate several consequences of inclusion relations between quantified provability logics. Moreover, we give a necessary and sufficient condition for the inclusion relation between quantified provability logics with respect to \ arithmetical interpretations.

Let \ be a class of formulas. We say that a theory T in classical logic has the \-disjunction property if for any \ sentences \ and \, either \ or \ whenever \. First, we characterize the \-disjunction property in terms of the notion of partial conservativity. Secondly, we prove a model theoretic characterization result for \-disjunction property. Thirdly, we investigate relationships between partial disjunction properties and several other properties of theories containing Peano arithmetic. Finally, we investigate unprovability of (...) formalized partial disjunction properties. (shrink)

Solovay proved the arithmetical completeness theorem for the system GL of propositional modal logic of provability. Montagna proved that this completeness does not hold for a natural extension QGL of GL to the predicate modal logic. Let Th(QGL) be the set of all theorems of QGL, Fr(QGL) be the set of all formulas valid in all transitive and conversely well-founded Kripke frames, and let PL(T) be the set of all predicate modal formulas provable in Tfor any arithmetical interpretation. Montagna’s results (...) are described as Th(QGL) ⊊ (Fr(QGL), PL(PA) ⊈ Fr(QGL), and Th(QGL) ⊊ PL(PA). In this paper, we prove the following three theorems: (1) Fr(QGL) ⊈ PL(T) for any Σ1-sound recursively enumerable extension T of I Σ1, (2) PL(T) ⊈ Fr(QGL) for any recursively enumerable S1755020312000275_inline1 A -theory T extending I Σ1, and (3) Th(QGL) ⊊ Fr(QGL) ∩ PL(T) for any recursively enumerable S1755020312000275_inline2 A -theory T extending I Σ2. To prove these theorems, we use iterated consistency assertions and nonstandard models of arithmetic, and we improve Artemov’s lemma which is used to prove Vardanyan’s theorem on the Π0 2-completeness of PL(T). (shrink)

In this paper, we investigate Rosser provability predicates whose provability logics are normal modal logics. First, we prove that there exists a Rosser provability predicate whose provability logic is exactly the normal modal logic \. Secondly, we introduce a new normal modal logic \ which is a proper extension of \, and prove that there exists a Rosser provability predicate whose provability logic includes \.

Akama et al. [1] introduced a hierarchical classification of first-order formulas for a hierarchical prenex normal form theorem in semi-classical arithmetic. In this paper, we give a justification for the hierarchical classification in a general context of first-order theories. To this end, we first formalize the standard transformation procedure for prenex normalization. Then we show that the classes $$\textrm{E}_k$$ and $$\textrm{U}_k$$ introduced in [1] are exactly the classes induced by $$\Sigma _k$$ and $$\Pi _k$$ respectively via the transformation procedure in (...) any first-order theory. (shrink)

Solovay proved (Israel J Math 25(3–4):287–304, 1976) that the propositional provability logic of any ∑2-sound recursively enumerable extension of PA is characterized by the propositional modal logic GL. By contrast, Montagna proved in (Notre Dame J Form Log 25(2):179–189, 1984) that predicate provability logics of Peano arithmetic and Bernays–Gödel set theory are different. Moreover, Artemov proved in (Doklady Akademii Nauk SSSR 290(6):1289–1292, 1986) that the predicate provability logic of a theory essentially depends on the choice of a binumeration of the (...) theory which is used to construct the provability predicate. In this paper, we compare predicate provability logics of I∑ n ’s. For a binumeration α(x) of a recursive theory T, let PL α(T) be the predicate provability logic of T defined by α(x). We prove that for any natural numbers i, j such that 0 < i < j, there exists a ∑1 binumeration α(x) of some recursive axiomatization of I∑ i such that ${{\sf PL}_\alpha({\rm I \Sigma}_i) \nsupseteq \bigcap_{\beta(x)}{\sf PL}_\beta({\rm I \Sigma}_j)}$ and ${{\sf PL}_\alpha({\rm I \Sigma}_i) \nsubseteq \bigcup_{\beta(x)}{\sf PL}_\beta({\rm I \Sigma}_j)}$ , where β(x) ranges over all ∑1 binumerations of recursive axiomatizations of I∑ j. (shrink)

We refine the arithmetical hierarchy of various classical principles by finely investigating the derivability relations between these principles over Heyting arithmetic. We mainly investigate some restricted versions of the law of excluded middle, De Morgan's law, the double negation elimination, the collection principle and the constant domain axiom.

We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf {PA}$ and intuitionistic arithmetic $\mathsf {HA}$. Using a generalized negative translation, we first provide a structured proof of the fact that $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over $\mathsf {HA} + {\Sigma _k}\text {-}\mathrm {LEM}$ where ${\Sigma _k}\text {-}\mathrm {LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $\Sigma _k$. In addition, we show that this conservation theorem is optimal in the (...) sense that for any semi-classical arithmetic T, if $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over T, then ${T}$ proves ${\Sigma _k}\text {-}\mathrm {LEM}$. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles. (shrink)

We investigate the Friedman–Goldfarb–Harrington theorem from two perspectives. Firstly, in the frameworks of classical and modal propositional logics, we study the forms of sentences whose existence is guaranteed by the FGH theorem. Secondly, we prove some variations of the FGH theorem with respect to Rosser provability predicates.

We introduce and investigate the notion of uniform Lyndon interpolation property which is a strengthening of both uniform interpolation property and Lyndon interpolation property. We prove several propositional modal logics including \, \, \ and \ enjoy ULIP. Our proofs are modifications of Visser’s proofs of uniform interpolation property using layered bisimulations Gödel’96, logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy, Springer, Berlin, 1996). Also we give a new upper bound on the complexity of uniform interpolants for \ (...) and \. (shrink)

By formalizing Berry's paradox, Vopěnka, Chaitin, Boolos and others proved the incompleteness theorems without using the diagonal argument. In this paper, we shall examine these proofs closely and show their relationships. Firstly, we shall show that we can use the diagonal argument for proofs of the incompleteness theorems based on Berry's paradox. Then, we shall show that an extension of Boolos' proof can be considered as a special case of Chaitin's proof by defining a suitable Kolmogorov complexity. We shall show (...) also that Vopěnka's proof can be reformulated in arithmetic by using the arithmetized completeness theorem. (shrink)

It is well known that Gödel’s incompleteness theorems hold for ∑1-definable theories containing Peano arithmetic. We generalize Gödel’s incompleteness theorems for arithmetically definable theories. First, we prove that every ∑n+1-definable ∑n-sound theory is incomplete. Secondly, we generalize and improve Jeroslow and Hájek’s results. That is, we prove that every consistent theory having ∏n+1set of theorems has a true but unprovable ∏nsentence. Lastly, we prove that no ∑n+1-definable ∑n-sound theory can prove its own ∑n-soundness. These three results are generalizations of Rosser’s (...) improvement of the first incompleteness theorem, Gödel’s first incompleteness theorem, and the second incompleteness theorem, respectively. (shrink)

We study the fixed point property and the Craig interpolation property for sublogics of the interpretability logic \(\textbf{IL}\). We provide a complete description of these sublogics concerning the uniqueness of fixed points, the fixed point property and the Craig interpolation property.

We define a liar-type paradox as a consistent proposition in propositional modal logic which is obtained by attaching boxes to several subformulas of an inconsistent proposition in classical propositional logic, and show several famous paradoxes are liar-type. Then we show that we can generate a liar-type paradox from any inconsistent proposition in classical propositional logic and that undecidable sentences in arithmetic can be obtained from the existence of a liar-type paradox. We extend these results to predicate logic and discuss Yablo’s (...) Paradox in this framework. Furthermore, we define explicit and implicit self-reference in paradoxes in the incompleteness phenomena. (shrink)

Monism is a metaphysical view according to which there is only one fundamental object. This paper will explore monism within the context of truthmaker theory, or Truthmaker Monism, a view rarely discussed in literature. Although few truthmaker theorists defend monism, at least explicitly, some theories seem to share the spirit of monism to some extent. Interestingly, they are proposed as solutions for the same problem, called the problem of negative truth. A close examination will show that while each of these (...) solutions can account for the problem, they are unsatisfactory for different reasons. This paper will suggest a novel solution to the problem of negative truth which preserves the advantages of existing solutions while avoiding the difficulties with which they are faced. (shrink)

Prior studies suggest that psychological difficulties arise from higher trait rejection sensitivity (RS)—heightened vigilance and differential detection of social rejection cues and defensive response to. On the other hand, from an evolutionary perspective, rapid and efficient detection of social rejection cues can be considered beneficial. We conducted a survey and an electrophysiological experiment to reconcile this seeming contradiction. We compared the effects of RS and rejection detection capability (RDC) on perceived interpersonal experiences (Study 1) and on neurocognitive processes in response (...) to cues of social rejection (disgusted faces; Study 2). We found that RS and RDC were not significantly related, although RS was positively related to perceived social rejection experiences and RDC was positively related to perceived social inclusion experiences. Event-related brain potentials (ERPs) revealed that higher RS was related to cognitive avoidance (i.e., P1) and heightened motivated attention (i.e., late positive potential: LPP), but not to facial expression encoding (i.e., N170) toward disgusted faces. On the other hand, higher RDC was related to heightened N170 amplitude, but not to P1 and LPP amplitudes. These findings imply that sensitivity to rejection is apparently distinct from the ability to detect social rejection cues and instead reflects intense vigilance and defensive response to those cues. We discussed an alternative explanation of the relationship between RS and RDC from a signal detection perspective. (shrink)

The influence of attachment style—anxious and avoidant attachment—on subjective responses to socially excluded experiences termed “Need-Threat” remains inconsistent. Need-Threat is a composite score of four fundamental needs: belonging, self-esteem, control, and meaningful existence. Individuals with high AX tend to spend much effort maintaining strong connections with others, while those with high AV tend to maintain high levels of self-esteem by distancing themselves from others. Therefore, attachment style is most likely to influence the need associated with each style. In addition, since (...) individuals with high AV satisfy their needs by keeping independence from others, they would experience the Need-Threat against excessive inclusion from others. This study aimed to investigate the influence of attachment style on each Need-Threat response to various inclusionary statuses. A total of 133 undergraduate students were equally assigned to low or high groups for each attachment style. Participants played one of the three types of the cyberball task : excluded, included, or over-included situation. The high AV group felt fewer threats to self-esteem than the low AV group in the excluded situation. Furthermore, only in the over-included situation did the high AV group feel more threats to belonging and self-esteem than the low AV group. AX did not influence any situation. These findings suggest that individuals with high AV would have a restrictive alleviation effect on adverse subjective responses to socially excluded experiences but demonstrate maladaptive subjective responses to over-included experiences. (shrink)

The theme of article is a short investigation of the problem of virtue in compositions of Prince Shotoku (Shotoku Taishi) such as “Seventeen-Article Constitution” and “Shomangyo gisho” (“Commentary on the Sri-mala Sutra”). Prince Shotoku (574 - 622) is a well-known religious leader in a history of Ancient Japan whoplayed a paramount role in Japanese Buddhism. He supervised over the construction of the first Buddhist temples and, more over, was a first Buddhist in Japan who interpreted Buddhist philosophical texts. Shotoku (...) Taishi wrote three commentaries known as “Commentaries on the Three Sutras” (Sangyo gisho). This work contains interpretation of three Buddhist sutras: “Lotus Sutra” (“Saddharmapundarica sutra”, “Hokke gisho”), “Vimalakirti sutra” (“Vimalakirtinirdesa sutra”, “Yuimagyo gisho”) and “Sri-Mala” sutra (“Sri-Malashimhanda sutra”, “Shomangyo gisho”). One of the most interesting aspects of this work, on my opinion, is a category of “virtue” (“zen”). While “virtue” in the concept of Shotoku Taishi is a basis of the One Vehile. At the same time, it differs from the Buddhist sense of this word. Also, the influence of “virtue” is reflected in articles of “Seventeen-Article Constitution”. Category of “virtue”, on my opinion, shows the new sights in the personality of Prince Shotoku. It leads as to moral aspects of religious and cultural policy which still not explored well in Western (Russian) scholarship. (shrink)

1. Tōzai bunka no kōryū -- 2. Shōtoku Taishi -- 3. Kinsei Nihon no hihanteki seishin -- 4. Nihon shūkyō no kindaisei.

1. Kodai shisō -- 3. Chūsei shisō -- 4. Kindai shisō -- 5. Tōzai bunka no kōryū -- 6. Shōtoku Taishi -- 7. Kinsei Nihon no hihanteki seishin -- 8. Nihon shūkyō no kindaisei.

In lieu of an abstract, here is a brief excerpt of the content:Reviewed by:The Artist as Professional in JapanKazuyo Nakamura and Akio OkazakiThe Artist as Professional in Japan, edited by Melinda Takeuchi. Stanford, Calif.: Stanford University Press, 2004, 262pp., $45.00 cloth.With the increase of cross-cultural academic exchange in our time, more accurate information on art from other cultures has become more easily available, and curriculum development of art education directed toward multiculturalism has been brought to realization. There is need emerging (...) among art educators for academic resources for teaching cross-cultural subject matters, and The Artist as Professional in Japan provides historical information helpful in gaining a critical understanding of the nature of Japanese art discourse. The volume is edited from a fresh sociocultural perspective by Melinda Takeuchi, professor of Japanese art at Stanford University.Takeuchi, noticing that few scholarly books on the profession of Japanese artists are available to students of art history in the United States, set about the volume in concerted efforts with her colleagues. The volume consists of individual case studies on different Japanese artists; they are well-known sculptors, painters, potters, printmakers, and architects and are recognized in Japan as representative in different eras from the seventh to the twentieth century. Running through the individual studies, there is a concern for political forces that shaped art discourse and the identity of the Japanese artist. The following questions are asked: What degree of control did the artists exercise over their métier? What were some of the dynamics operating in the production, consummation, and evaluation of art and artist? How was the image of the artist formed during various periods? Working with these questions, seven case studies address issues of canon formation of art by looking into the terrain of the meaning of a critical word, Shoku-nin; it literally means people (nin) with an occupation (shoku) and denotes the collective artisan class.Different art historians and art theorists take a unique approach for developing each case study in the volume. Donald F. McCallum's study in chapter 2 is on the Buddhist Icons of the Shaka Triad during the Asuka Period (ca.590-ca.650), and it is asked what were the political forces working on the production of the [End Page 118] icons. In contrary to orthodox view, it is argued that the icons were produced not by an individual sculptor named Tori-busshi but by the guilds of which the supervisor was Tori. Also, it is argued that the icons were produced with the patronage of soga clan, the dominant political force of the time, not by the imperial family, including Shotoku Taishi.Karen L. Brock in chapter 3 examines the case of E'nichibo Jonin (active ca.1211-ca.1243), the painter of Saint Myoe. The case shows that the ateliers of temples, such as Kozanji in Kyoto, played a central role in producing and distributing sacred images. This study makes clear that few individual painters, such as those named ebusshi, participated in the formation of the canon of Japanese painting, but collective political forces, such as Kozanji ateliers, exercised power in bringing out sacred objects.In chapter 4 Melinda Takeuchi takes up the case of Tosa Mitsunobu (1434-ca.1523), an artisan painter active in Kyoto court circles. It shows a historical fact particular to Japanese art discourse—that later artists manipulated the names of earlier ones for professional or cultural merits. Taking notice of the fact that Mitsunobu's name late became synonymous with a production unit that shares secret techniques of products, Takeuchi concludes, "In the end, the name of an artist transcends time, space, materiality, and ultimately discourse itself" (101).The study of Louise Allison Cort in chapter 5 is on the case of Morita Kyuemon in the seventeenth century, a warrior trained as a potter and running the Odo pottery in the Tosa domain. By exploring the motivations of the Tosa domain in trying to transform local products into refined and stylish pottery worthy of formal presentation to other domain rulers (daimyo), to government officials, and to the shogun in Edo, this chapter demonstrates how both the potter and the ruler actively sought to join the aesthetic mainstream of their own day.In... (shrink)