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.

Second-order abstract categorial grammars (de Groote in Association for computational linguistics, 39th annual meeting and 10th conference of the European chapter, proceedings of the conference, pp. 148–155, 2001) and hyperedge replacement grammars (Bauderon and Courcelle in Math Syst Theory 20:83–127, 1987; Habel and Kreowski in STACS 87: 4th Annual symposium on theoretical aspects of computer science. Lecture notes in computer science, vol 247, Springer, Berlin, pp 207–219, 1987) are two natural ways of generalizing “context-free” grammar formalisms for string and tree (...) languages. It is known that the string generating power of both formalisms is equivalent to (non-erasing) multiple context-free grammars (Seki et al. in Theor Comput Sci 88:191–229, 1991) or linear context-free rewriting systems (Weir in Characterizing mildly context-sensitive grammar formalisms, University of Pennsylvania, 1988). In this paper, we give a simple, direct proof of the fact that second-order ACGs are simulated by hyperedge replacement grammars, which implies that the string and tree generating power of the former is included in that of the latter. The normal form for tree-generating hyperedge replacement grammars given by Engelfriet and Maneth (Graph transformation. Lecture notes in computer science, vol 1764. Springer, Berlin, pp 15–29, 2000) can then be used to show that the tree generating power of second-order ACGs is exactly the same as that of hyperedge replacement grammars. (shrink)

Within a weak subsystem of second-order arithmetic , that is -conservative over , we reformulate Kreisel's proof of the Second Incompleteness Theorem and Boolos' proof of the First Incompleteness Theorem.

We identify bar recursion on moduli of continuity as a fundamental notion of constructive mathematics. We show that continuous functions from the Baire space \ to the natural numbers \ which have moduli of continuity with bar recursors are exactly those functions induced by Brouwer operations. The connection between Brouwer operations and bar induction allows us to formulate several continuity principles on the Baire space stated in terms of bar recursion on continuous moduli which naturally characterise some variants of bar (...) induction. These principles state that a certain kind of continuous function from \ to \ admits a modulus of continuity with a bar recursor. The results for the Baire space are recast in the setting of the Cantor space \ using the notion of fan recursor, a bar recursor for binary trees. This yields characterisations of uniformly continuous functions on the Cantor space and fan theorem in terms of fan recursors. The results for the Cantor space hold over the extensional version of intuitionistic arithmetic in all finite types ), and those for the Baire space hold over \ extended with the type for Brouwer operations. Our work places Spector’s bar recursion in a proper context of Brouwer’s intuitionistic mathematics and clarifies the connection between bar recursion and bar induction. (shrink)

Along the line of Hirst‐Mummert and Dorais, we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2‐statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2‐statement S of some syntactical form, if its uniform version derives the uniform variant of over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi‐intuitionistic systems (...) including bar induction in all finite types but also nonconstructive principles such as Kőnig's lemma and uniform weak Kőnig's lemma. Our result is applicable to many mathematical principles whose sequential versions imply. (shrink)

没後20年、いま必要な歴史に裏打ちされた予見力、現実政治に提言する率直さ、道義性と理想主義。.

One of the primary views on our supposed obligation towards our descendants in the context of environmental problems invokes the idea of the rights of future generations. A growing number of authors also hold that the descendants of those victimized by historical injustices, including colonialism and slavery, have the right to demand financial reparations for the sufferings of their distant ancestors. However, these claims of intergenerational rights face theoretical difficulties, notably the non-identity problem. To circumvent this problem in a relationship (...) between present and future generations, some rights theorists replace future individual rights with such collective rights. Others advance the threshold conception of harm in discussing intergenerational relationships in general. Despite the significant implications these revisionist views might have, few efforts have been made to scrutinize their solidity. To plug such a gap in the literature, this paper examines to what extent the collective understanding of intergenerational rights is pertinent. I also explore the virtues and drawbacks of the threshold interpretation of harm. The paper concludes by suggesting that the motivation behind these and other versions of the rights theory suffers from the ambiguity of a traditional dichotomy between perfect and imperfect duties. (shrink)

Savant syndrome and prime numbers Oliver Sacks reported that a pair of autistic twins had extraordinary number abilities and that they spontaneously generated huge prime numbers. Such abilities could contradict our understanding of human abilities. Sacks' report attracted widespread attention, and several researchers speculated theoretically. Unfortunately, most of the explanations in the literature are wrong. Here a correct explanation on prime number identification is provided. Fermat's little theorem is implemented in spreadsheet. Also, twenty years after the report, questionable aspects were (...) found in it. Extreme abilities became dubious. One possibility for the less extreme abilities is incomplete trial division. (shrink)

We propose a new game to strategically justify the constrained equal awards rule in claims problems. Our game is “procedurally fair” and “multilateral”. In addition, even if claimants cannot reach an agreement in any period, they can renegotiate in the next period. We show that, for each claims problem, the awards vector chosen by the constrained equal awards rule achieved at period 1 is the unique subgame perfect equilibrium outcome of the game.

Kierstead showed that every computable marriage problem has a computable matching under the assumption of computable expanding Hall condition and computable local finiteness for boys and girls. The strength of the marriage theorem reaches or if computable expanding Hall condition or computable local finiteness for girls is weakened. In contrast, the provability of the marriage theorem is maintained in even if local finiteness for boys is completely removed. Using these conditions, we classify the strength of variants of marriage theorems in (...) the context of reverse mathematics. Furthermore, we introduce another condition that also makes the marriage theorem provable in, and investigate the sequential and Weihrauch strength of marriage theorems under that condition. (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 stationarity of types over models in simple theories. In particular, we show that in simple theories with finite SU-rank, any complete type over a model having Cantor-Bendixson rank is stationary.

Tanabe Hajime, another pole of the so-called Kyoto-School of Philosophy of modern Japan, attempts to construct a dialectical, triadic logic of genus, species and individual as a creative synthesis between Eastern and Western philosophy. Although the formal pattern of his method is influenced by the Hegelian dialectic, the way of his thinking is rather prevailed by Kantian dualism. This makes a sharp contrast to his mentor Nishida Kitaro, whose logic of Topos or Place qua Absolute Nothingness is criticized as all-embracing (...) and static in character by him. The difference between them might be parallel to that of Greek and Latin theology concerning the Trinity. Tanabe never presupposes any preexistent entity as the primordial One in the eternal dimension, but rather maintains the individuality as the free subjective agent in the field of history. The dichotomy between the universal and the individual is overcome in and through the mediation of the third term— the species — as the negatively self-realized, specific form of the genus. The species, however, turns out to be the self-estrangement, when it loses the perpetually negative mediation of the free subjective activity of the individual. (shrink)

In this paper, I show that the availability of what some authors have called the weak reading and the strong reading of donkey sentences with relative clauses is systematically related to monotonicity properties of the determiner. The correlation is different from what has been observed in the literature in that it concerns not only right monotonicity, but also left monotonicity (persistence/antipersistence). I claim that the reading selected by a donkey sentence with a double monotone determiner is in fact the one (...) that validates inference based on the left monotonicity of the determiner. This accounts for the lack of strong reading in donkey sentences with MON determiners, which have been neglected in the literature. I consider the relevance of other natural forms of inference as well, but also suggest how monotonicity inference might play a central role in the actual process of interpretation. The formal theory is couched in dynamic predicate logic with generalized quantifiers. (shrink)

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)