Classically, weak König's lemma and Brouwer's fan theorem for detachable bars are equivalent. We give a direct constructive proof that the former implies the latter.

In this essay I present the philosophy of Nishida Kitarō, the father of the Kyoto School tradition, as an alternative version of transcendental philosophy. While following the steps of Kant and Husserl in important ways, Nishida attempts to take the transcendental approach even further, finally leaving us with a different view of reality that is neither realist nor idealist, but, rather, radically realist. I call this radical transcendental position, “awakened realism”. Due to word limitations, I can only set the stage (...) for further discussion on what kind of implication this may have for transcendental philosophy. But if I succeed in making my presentation clear enough, it should naturally ignite discussion on how far we can radicalize transcendental philosophy without making it into something else. (shrink)

The purpose of this paper is an axiomatic study of the interrelations between certain continuity properties. We deal with principles which are equivalent to the statements "every mapping is sequentially nondiscontinuous", "every sequentially nondiscontinuous mapping is sequentially continuous", and "every sequentially continuous mapping is continuous". As corollaries, we show that every mapping of a complete separable space is continuous in constructive recursive mathematics (the Kreisel-Lacombe-Schoenfield-Tsejtin theorem) and in intuitionism.

Aristotle, in his Nicomachean Ethics, considers how one becomes virtuous. However, when asking the question of how, he does not refer to ‘by friend’ as an option; all he refers to are ‘by learning’, ‘by training’, ‘by habituation’, ‘by god’ and ‘by luck’. Why does he not do so? First, I point out the fact that both Aristotle and Plato do not refer to the option of ‘by friend’ when asking the question of how. Second, I argue that Aristotle does (...) not overlook the educational role of friendship. He understands that one needs friends. Third and finally, I consider the reason why Aristotle hesitates to emphasize the educational role of friendship and indicate that his theory of the mean causes it. This reveals the strained relationship between his theory of the mean and that of friendship in his ethical theory. (shrink)

Proof-theory has traditionally been developed based on linguistic (symbolic) representations of logical proofs. Recently, however, logical reasoning based on diagrammatic or graphical representations has been investigated by logicians. Euler diagrams were introduced in the eighteenth century. But it is quite recent (more precisely, in the 1990s) that logicians started to study them from a formal logical viewpoint. We propose a novel approach to the formalization of Euler diagrammatic reasoning, in which diagrams are defined not in terms of regions as in (...) the standard approach, but in terms of topological relations between diagrammatic objects. We formalize the unification rule, which plays a central role in Euler diagrammatic reasoning, in a style of natural deduction. We prove the soundness and completeness theorems with respect to a formal set-theoretical semantics. We also investigate structure of diagrammatic proofs and prove a normal form theorem. (shrink)

In this note, we prove that certain theories of (many‐sorted) intuitionistic predicate logic are closed under the independence of premiss rule (IPR). As corollaries, we show that and extended by some non‐classical axioms and non‐constructive axioms are closed under IPR.

The purpose of this paper is an axiomatic study of the interrelations between certain continuity properties. We show that every mapping is sequentially continuous if and only if it is sequentially nondiscontinuous and strongly extensional, and that "every mapping is strongly extensional", "every sequentially nondiscontinuous mapping is sequentially continuous", and a weak version of Markov's principle are equivalent. Also, assuming a consequence of Church's thesis, we prove a version of the Kreisel-Lacombe-Shoenfield-Tsĕitin theorem.

We give a variant of the Gödel-Gentzen-negative translation, and a syntactic characterization which entails conservativity result for formulas.

How are the various classically equivalent definitions of compactness for metric spaces constructively interrelated? This question is addressed with Bishop-style constructive mathematics as the basic system – that is, the underlying logic is the intuitionistic one enriched with the principle of dependent choices. Besides surveying today's knowledge, the consequences and equivalents of several sequential notions of compactness are investigated. For instance, we establish the perhaps unexpected constructive implication that every sequentially compact separable metric space is totally bounded. As a by-product, (...) the fan theorem for detachable bars of the complete binary fan proves to be necessary for the unit interval possessing the Heine-Borel property for coverings by countably many possibly empty open balls. (shrink)

We show that in elementary analysis (EL) the contrapositive of countable choice is equivalent to double negation elimination for \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Sigma_{2}^{0}}$$\end{document}-formulas. By also proving a recursive adaptation of this equivalence in Heyting arithmetic (HA), we give an instance of the conservativity of EL over HA with respect to recursive functions and predicates. As a complement, we prove in HA enriched with the (extended) Church thesis that every decidable predicate is recursive.

We extend the concept of apartness spaces to the concept of quasi-apartness spaces. We show that there is an adjunction between the category of quasi-apartness spaces and the category of neighbourhood spaces, which indicates that quasi-apartness is a more natural concept than apartness. We also show that there is an adjoint equivalence between the category of apartness spaces and the category of Grayson’s separated spaces.

The standard construction of quotient spaces in topology uses full separation and power sets. We show how to make this construction using only the predicative methods available in constructive type theory and constructive set theory.

We will overview the results in an informal approach to constructive reverse mathematics, that is reverse mathematics in Bishop’s constructive mathematics, especially focusing on compactness properties and continuous properties.

This paper gives new confluence proofs for several lambda calculi with permutation-like reduction, including lambda calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions, and a lambda calculus with explicit substitutions. For lambda calculi with permutative conversion, naïve parallel reduction technique does not work, and traditional notion of residuals is required as Ando pointed out. This paper shows that the difficulties can be avoided by extending the technique proposed by Dehornoy and van Oostrom, called the Z (...) theorem: existence of a mapping on terms with the Z property concludes the confluence. Since it is still hard to directly define a mapping with the Z property for the lambda calculi with permutative conversions, this paper extends the Z theorem to compositional functions, called compositional Z, and shows that we can adopt it to the calculi. (shrink)

Feinberg and Mallatt, in their presentation of neurobiological naturalism, have suggested that visual consciousness was acquired by early vertebrates and inherited by a wide range of descendants, and that its neural basis has shifted to nonhomologous nervous structures during evolution. However, their evolutionary scenario of visual consciousness relies on the assumption that visual consciousness is closely linked with survival, which is not commonly accepted in current consciousness research. We suggest an alternative idea that visual consciousness is linked to a specific (...) class of agency, consequently justifying their phylogenetic claim. We also examine the implication of their phylogenetic claim: visual consciousness is homologous across vertebrates, but its neural basis is not. This apparent incongruence illustrates a general phenomenon of homology, and that the resulting hierarchical view of visual consciousness and its neural basis can be straightforwardly accommodated by neurobiological naturalism. Throughout these discussions, we aim to address the potential theoretical issues in neurobiological naturalism and refine the picture illustrated by Feinberg and Mallatt regarding phylogenetic distribution and trajectories of visual consciousness. (shrink)

Consider the problem which set V of propositional variables suffices for whenever, where, and ⊢c and ⊢i denote derivability in classical and intuitionistic implicational logic, respectively. We give a direct proof that stability for the final propositional variable of the (implicational) formula A is sufficient; as a corollary one obtains Glivenko's theorem. Conversely, using Glivenko's theorem one can give an alternative proof of our result. As an alternative to stability we then consider the Peirce formula. It is an easy consequence (...) of the result above that adding a single instance of the Peirce formula suffices to move from classical to intuitionistic derivability. Finally we consider the question whether one could do the same for minimal logic. Given a classical derivation of a propositional formula not involving ⊥, which instances of the Peirce formula suffice as additional premises to ensure derivability in minimal logic? We define a set of such Peirce formulas, and show that in general an unbounded number of them is necessary. (shrink)

In this paper we introduce effectiveness into model theory of intuitionistic logic. The main result shows that any computable theory T of intuitionistic predicate logic has a Kripke model with decidable forcing such that for any sentence φ, φ is forced in the model if and only if φ is intuitionistically deducible from T.

Consistency with the formal Church’s thesis, for short CT, and the axiom of choice, for short AC, was one of the requirements asked to be satisfied by the intensional level of a two-level foundation for constructive mathematics as proposed by Maietti and Sambin From sets and types to topology and analysis: practicable foundations for constructive mathematics, Oxford University Press, Oxford, 2005). Here we show that this is the case for the intensional level of the two-level Minimalist Foundation, for short MF, (...) completed in 2009 by the second author. The intensional level of MF consists of an intensional type theory à la Martin-Löf, called mTT. The consistency of mTT with CT and AC is obtained by showing the consistency with the formal Church’s thesis of a fragment of intensional Martin-Löf’s type theory, called \, where mTT can be easily interpreted. Then to show the consistency of \ with CT we interpret it within Feferman’s predicative theory of non-iterative fixpoints \ by extending the well known Kleene’s realizability semantics of intuitionistic arithmetics so that CT is trivially validated. More in detail the fragment \ we interpret consists of first order intensional Martin-Löf’s type theory with one universe and with explicit substitution rules in place of usual equality rules preserving type constructors -rule which is not valid in our realizability semantics). A key difficulty encountered in our interpretation was to use the right interpretation of lambda abstraction in the applicative structure of natural numbers in order to model all the equality rules of \ correctly. In particular the universe of \ is modelled by means of \-fixpoints following a technique due first to Aczel and used by Feferman and Beeson. (shrink)

A logic is said to be paraconsistent if it does not allow everything to follow from contradictory premises. There are several approaches to paraconsistency. This paper is concerned with several philosophical positions on paraconsistency. In particular, it concerns three ‘schools’ of paraconsistency: Australian, Belgian and Brazilian. The Belgian and Brazilian schools have raised some objections to the dialetheism of the Australian school. I argue that the Australian school of paraconsistency need not be closed down on the basis of the Belgian (...) and Brazilian schools’ objections. In the appendix of the paper, I also argue that the Brazilian school’s view of logic is not coherent. (shrink)

We extend Bishopʼs concept of function spaces to the concept of pre-function spaces. We show that there is an adjunction between the category of neighbourhood spaces and the category of Φ-closed pre-function spaces. We also show that there is an adjunction between the category of uniform spaces and the category of Ψ-closed pre-function spaces.

In this paper, we deal with compact operators on a Hilbert space, within the framework of Bishop's constructive mathematics. We characterize the compactness of a bounded linear mapping of a Hilbert space into C n , and prove the theorems: Let A and B be compact operators on a Hilbert space H , let C be an operator on H and let α ϵ C . Then α A is compact, A + B is compact, A ∗ is compact, CA (...) is compact and if C ∗ exists, then AC is compact; An operator on a Hilbert space has an adjoint if and only if it is weakly compact. (shrink)

In this paper, we deal with a relationship among the law of excluded middle, the double negation elimination and the independence of premiss rule ) for intuitionistic predicate logic. After giving a general machinery, we give, as corollaries, several examples of extensions of \ and \ which are closed under \ but do not derive the independence of premiss axiom.

This paper proves the strong normalization of classical natural deduction with disjunction and permutative conversions, by using CPS-translation and augmentations. Using them, this paper also proves the strong normalization of classical natural deduction with general elimination rules for implication and conjunction, and their permutative conversions. This paper also proves that natural deduction can be embedded into natural deduction with general elimination rules, strictly preserving proof normalization.

In the 1958-1959 Collège de France course, Merleau-Ponty expounds a detailed commentary on the last paragraphs of the Einleitung from Hegel’s Phenomenology of Spirit. We examine in what sense this course has developed the notions that he was in the process of defining, notions such as “chiasm,” “reversibility,” “depth,” and “flesh.” What seems crucial in this course is to clearly define good ambiguity as opposed to bad ambiguity, that is, to the simple mixture of finitude and universality, of interiority and (...) exteriority. It is a question then of revealing, even within Hegelian thought, the operation, although unstable, of good ambiguity and of instituting it beyond the distinction between anthropology and logic without a return to naturalism. It should first be noted that consciousness is for Hegel violence against itself, it gives itself its measure, such that the distinction between measuring and measured is internal to it. By insisting on this “reversibility” of the measuring and the measured, Merleau-Ponty comes to emphasize that the self-relation of consciousness is simultaneously its opening onto a transcendent – an opening whereby it learns something. This leads him to define “the new ontological milieu” which is the depth of the life of consciousness. It is within this depth that the interrogative experience winds on itself. Secondly, if there truly must be a moment where the Hegelian Zweideutigkeit becomes good ambiguity, it will not suffice to explore preobjective depth; it would still be necessary to discern “the hinge” which is “solid, unwavering” and which “remains irremediably hidden.” It is this unwavering hinge that supports phenomena and that, in simultaneously decentering and recentering the fields of appearances, opens a place where one can follow the genesis of sense. Finally, we note that this discovery of the new ontological milieu can be considered as the recovery of the notion of institution that Merleau-Ponty had proposed in 1954-1955: on the one hand, the notion of chiasm invites us to reveal the hinge which at once decenters and recenters the fields of appearances. This hinge is free from the alternative of nature and culture, of subjective and objective spirit; it is the rootedness of our interrogative experience in brute being, which is not object but starts an indefinite search of self. But, on the other hand, the notion of institution, which is essentially descriptive and factual, makes us better feel the weight of the instituted that is also irremediably hidden. It makes us feel the inertia of the instituting event, as well as its fecundity and its cumulativity. (shrink)

The Dedekind cuts in an ordered set form a set in the sense of constructive Zermelo—Fraenkel set theory. We deduce this statement from the principle of refinement, which we distill before from the axiom of fullness. Together with exponentiation, refinement is equivalent to fullness. None of the defining properties of an ordering is needed, and only refinement for two—element coverings is used. In particular, the Dedekind reals form a set; whence we have also refined an earlier result by Aczel and (...) Rathjen, who invoked the full form of fullness. To further generalise this, we look at Richman's method to complete an arbitrary metric space without sequences, which he designed to avoid countable choice. The completion of a separable metric space turns out to be a set even if the original space is a proper class; in particular, every complete separable metric space automatically is a set. (shrink)

In this paper, I argue that later Nishida's analysis of self-awareness (jikaku) provides a new perspective on the nature of self-awareness as understood in the philosophical literature today. I argue that the contemporary literature deals with two kinds of self-awareness; the higher-order theory understands self-awareness to be an objectified awareness and the phenomenological tradition generally understands self-awareness to be, at least primarily, a non-objectified awareness. In light of this, I first give an account of Nishida's ?acting-intuition? with reference to the (...) ?historical body.? Then I argue that later Nishida's analysis of self-awareness depicts the inadequacy of the two kinds of self-awareness as both being stuck in the subject-object dichotomy which, according to Nishida, is but one mode of experience, namely the mode of difference. Nishida provides an account that ultimately foregrounds the experiential mode of unity that negates any sense of differentiation between the subject and object. (shrink)

We deal with a restricted form WC-N' of the weak continuity principle, a version BT' of Baire's theorem, and a boundedness principle BD-N. We show, in the spirit of constructive reverse mathematics, that WC-N'. BT' + ¬LPO and BD-N + ¬LPO are equivalent in a constructive system, where LPO is the limited principle of omniscience.

Intercultural Phenomenology explores the nature of reality by engaging in a cross-cultural dialogue between two of the most influential philosophical traditions of the 20th century. Drawing on ideas from phenomenology, Japanese philosophy and Zen Buddhism, it follows the philosophers who changed their perception of the world by choosing to suspend judgement. Guided by this philosophical method known as the "epoché", or suspension of judgment in ancient Greek, it is an introduction to the philosophy and practice of letting objects in the (...) world speak for themselves. (shrink)