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)

The seventeenth century marked a critical phase in the emergence of modern science. But we misunderstand this process, if we assume that seventeenth-century modes of natural inquiry were identical to the highly specialised, professionalised and ever proliferating family of modern sciences practised today.

Should weak forms of the axiom of choice really be accepted within constructive mathematics? A critical view of the Brouwer-Heyting-Kolmogorov interpretation, accompanied by the intention to include nondeterministic algorithms, leads us to subscribe to Richman's appeal for dropping countable choice. As an alternative interpretation of intuitionistic logic, we propose to renew dialogue semantics.

This book bridges the gaps between logic, mathematics and computer science by delving into the theory of well-quasi orders, also known as wqos. This highly active branch of combinatorics is deeply rooted in and between many fields of mathematics and logic, including proof theory, commutative algebra, braid groups, graph theory, analytic combinatorics, theory of relations, reverse mathematics and subrecursive hierarchies. As a unifying concept for slick finiteness or termination proofs, wqos have been rediscovered in diverse contexts, and proven to be (...) extremely useful in computer science. The book introduces readers to the many facets of, and recent developments in, wqos through chapters contributed by scholars from various fields. As such, it offers a valuable asset for logicians, mathematicians and computer scientists, as well as scholars and students. (shrink)

Even after yet another grand conjecture has been proved or refuted, any omniscience principle that had trivially settled this question is just as little acceptable as before. The significance of the constructive enterprise is therefore not affected by any gain of knowledge. In particular, there is no need to adapt weak counterexamples to mathematical progress.

The topic of this article is the formal topology abstracted from the Zariski spectrum of a commutative ring. After recollecting the fundamental concepts of a basic open and a covering relation, we study some candidates for positivity. In particular, we present a coinductively generated positivity relation. We further show that, constructively, the formal Zariski topology cannot have enough points.

The intersection of a linearly ordered set of total subrelations of a total relation with range 2 need not be total, constructively.

A proof is a successful demonstration that a conclusion necessarily follows by logical reasoning from axioms which are considered evident for the given context and agreed upon by the community. It is this concept that sets mathematics apart from other disciplines and distinguishes it as the prototype of a deductive science. Proofs thus are utterly relevant for research, teaching and communication in mathematics and of particular interest for the philosophy of mathematics. In computer science, moreover, proofs have proved to be (...) a rich source for already certified algorithms. This book provides the reader with a collection of articles covering relevant current research topics circled around the concept 'proof'. It tries to give due consideration to the depth and breadth of the subject by discussing its philosophical and methodological aspects, addressing foundational issues induced by Hilbert's Programme and the benefits of the arising formal notions of proof, without neglecting reasoning in natural language proofs and applications in computer science such as program extraction. (shrink)

It is folklore that if a continuous function on a complete metric space has approximate roots and in a uniform manner at most one root, then it actually has a root, which of course is uniquely determined. Also in Bishop's constructive mathematics with countable choice, the general setting of the present note, there is a simple method to validate this heuristic principle. The unique solution even becomes a continuous function in the parameters by a mild modification of the uniqueness hypothesis. (...) Moreover, Brouwer's fan theorem for decidable bars turns out to be equivalent to the statement that, for uniformly continuous functions on a compact metric space, the crucial uniform “at most one” condition follows from its non-uniform counterpart. This classification in the spirit of the constructive reverse mathematics, as propagated by Ishihara and others, sharpens an earlier result obtained jointly with Berger and Bridges. (shrink)

In the present contribution we look at the legacy of Hilbert's programme in some recent developments in mathematics. Hilbert's ideas have seen new life in generalised and relativised forms by the hands of proof theorists and have been a source of motivation for the so--called reverse mathematics programme initiated by H. Friedman and S. Simpson. More recently Hilbert's programme has inspired T. Coquand and H. Lombardi to undertake a new approach to constructive algebra in which strong emphasis is laid on (...) the use of finite methods. The main aim is to eliminate the ideal objects and in so doing obtain more elementary and informative proofs. We survey some work in commutative algebra---mainly about and around the Zariski spectrum and the Krull dimension of a commutative ring---which witnesses the feasibility of such a revised Hilbert's programme. (shrink)

The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of enough projective sets has been discussed as an additional axiom taken from the interpretation of CZF in Martin-Löf’s intuitionistic type theory. On the other hand, every non-empty set is injective in classical ZF, which argument fails to work in CZF. The aim of this paper is to shed some light on (...) the problem whether there are (enough) injective sets in CZF. We show that no two element set is injective unless the law of excluded middle is admitted for negated formulas, and that the axiom of power set is required for proving that “there are strongly enough injective sets”. The latter notion is abstracted from the singleton embedding into the power set, which ensures enough injectives both in every topos and in IZF. We further show that it is consistent with CZF to assume that the only injective sets are the singletons. In particular, assuming the consistency of CZF one cannot prove in CZF that there are enough injective sets. As a complement we revisit the duality between injective and projective sets from the point of view of intuitionistic type theory. (shrink)

We investigate how nonstandard reals can be established constructively as arbitrary infinite sequences of rationals, following the classical approach due to Schmieden and Laugwitz. In particular, a total standard part map into Richman's generalised Dedekind reals is constructed without countable choice.

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