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.

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.

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.

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 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.

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)

We show, within the framework of Bishop's constructive mathematics, that (sequential) completeness of the locally convex space $\mathcal{D} (\mathbb{R})$ of test functions is equivalent to the principle BD-N which holds in classical mathemtatics, Brouwer's intuitionism and Markov's constructive recursive mathematics, but does not hold in Bishop's constructivism.

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 give a variant of the Gödel-Gentzen-negative translation, and a syntactic characterization which entails conservativity result for formulas.

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)

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.

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)

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.

Beka Jalagania has recently argued that benefiting from wild animals generates special duties to assist them. To show this, Jalagania offers an argument that focuses on their contribution to the production of the benefits we receive, which he calls the contribution argument. In this paper I aim to show that this argument fails. One of the premises on which the contribution argument rests is that we ought to share the benefits we receive with whoever contributed to their production. However, the (...) idea of contribution in this premise is somewhat ambiguous as it stands and can be further clarified in at least two ways: a counterfactual way and a causal way. I examine these two interpretations of contribution in turn, focusing mainly on their counterintuitive implications, and argue that under both interpretations, the contribution argument faces some difficulties. Therefore, unless a plausible interpretation of contribution is offered, we should conclude that this argument fails. (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.

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)

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)

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.

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.

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 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)

Constructive mathematics – mathematics in which ‘there exists’ always means ‘we can construct’ – is enjoying a renaissance. Fifty years on from Bishop’s groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject’s myriad aspects. Major themes include: constructive algebra and geometry, constructive analysis, constructive topology, (...) constructive logic and foundations of mathematics, and computational aspects of constructive mathematics. A series of introductory chapters provides graduate students and other newcomers to the subject with foundations for the surveys that follow. Edited by four of the most eminent experts in the field, this is an indispensable reference for constructive mathematicians and a fascinating vista of modern constructivism for the increasing number of researchers interested in constructive approaches. (shrink)

Many existence propositions in constructive analysis are implied by the lesser limited principle of omniscience LLPO; sometimes one can even show equivalence. It was discovered recently that some existence propositions are equivalent to Bouwer's fan theorem FAN if one additionally assumes that there exists at most one object with the desired property. We are providing a list of conditions being equivalent to FAN, such as a unique version of weak König's lemma. This illuminates the relation between FAN and LLPO. Furthermore, (...) we give a short and elementary proof of the fact that FAN is equivalent to each positive valued function with compact domain having positive infimum. (shrink)

We systematically study several principles and give a principle which is weaker than disjunctive Markov’s principle. We also show that the principle is underivable and strictly weaker than MP∨ in certain extensions of the system EL of elementary analysis.

Uniform sequential continuity, a property classically equivalent to sequential continuity on compact sets, is shown, constructively, to be a consequence of strong continuity on a metric space. It is then shown that in the case of a separable metric space, uniform sequential continuity implies strong continuity if and only if one adopts a certain boundedness principle that, although valid in the classical, recursive and intuitionistic setting, is independent of Heyting arithmetic.

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)

We introduce the notion of a convex tree. We show that the binary expansion for real numbers in the unit interval ) is equivalent to weak König lemma ) for trees having at most two nodes at each level, and we prove that the intermediate value theorem is equivalent to \ for convex trees, in the framework of constructive reverse mathematics.

This book provides linguists with a clear, critical, and comprehensive overview of theoretical and experimental work on information structure. Leading researchers survey the main theories of information structure in syntax, phonology, and semantics as well as perspectives from psycholinguistics and other relevant fields. Following the editors' introduction the book is divided into four parts. The first, on theories of and theoretical perspectives on information structure, includes chapters on topic, prosody, and implicature. Part 2 covers a range of current issues in (...) the field, including focus, quantification, and sign languages, while Part 3 is concerned with experimental approaches to information structure, including processes involved in its acquisition and comprehension. The final part contains a series of linguistic case studies drawn from a wide variety of the world's language families. This volume will be the standard guide to current work in information structure and a major point of departure for future research. (shrink)

Working in the weakening of constructive Zermelo-Fraenkel set theory in which the subset collection scheme is omitted, we show that the binary refinement principle implies all the instances of the exponentiation axiom in which the basis is a discrete set. In particular binary refinement implies that the class of detachable subsets of a set form a set. Binary refinement was originally extracted from the fullness axiom, an equivalent of subset collection, as a principle that was sufficient to prove that the (...) Dedekind reals form a set. Here we show that the Cauchy reals also form a set. More generally, binary refinement ensures that one remains in the realm of sets when one starts from discrete sets and one applies the operations of exponentiation and binary product a finite number of times. (shrink)

We propose a natural definition of what it means in a constructive context for a Banach space to be reflexive, and then prove a constructive counterpart of the Milman-Pettis theorem that uniformly convex Banach spaces are reflexive.