-
144Binary Refinement Implies Discrete ExponentiationStudia Logica 84 (3): 361-368. 2006.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 prov…Read more
-
83Are There Enough Injective Sets?Studia Logica 101 (3): 467-482. 2013.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 ar…Read more
-
75A revival of the landscape paradigm: Large scale data harvesting provides access to fitness landscapesComplexity 17 (5): 6-10. 2012.
-
60On constructing completionsJournal of Symbolic Logic 70 (3): 969-978. 2005.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 an…Read more
-
59Classifying Dini's TheoremNotre Dame Journal of Formal Logic 47 (2): 253-262. 2006.Dini's theorem says that compactness of the domain, a metric space, ensures the uniform convergence of every simply convergent monotone sequence of real-valued continuous functions whose limit is continuous. By showing that Dini's theorem is equivalent to Brouwer's fan theorem for detachable bars, we provide Dini's theorem with a classification in the recently established constructive reverse mathematics propagated by Ishihara. As a complement, Dini's theorem is proved to be equivalent to the an…Read more
-
56Linear independence without choiceAnnals of Pure and Applied Logic 101 (1): 95-102. 1999.The notions of linear and metric independence are investigated in relation to the property: if U is a set of n+1 independent vectors, and X is a set of n independent vectors, then adjoining some vector in U to X results in a set of n+1 independent vectors. It is shown that this property holds in any normed linear space. A related property – that finite-dimensional subspaces are proximinal – is established for strictly convex normed spaces over the real or complex numbers. It follows that metric …Read more
-
53Power laws in biology: Between fundamental regularities and useful interpolation rulesComplexity 16 (3): 6-9. 2011.
-
51Too simple solutions of hard problemsNordic Journal of Philosophical Logic 6 (2): 138-146. 2010.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.
-
51Countable choice as a questionable uniformity principlePhilosophia Mathematica 12 (2): 106-134. 2004.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.
-
49A beginning of the end of the holism versus reductionism debate?: Molecular biology goes cellular and organismicComplexity 13 (1): 10-13. 2007.
-
43Apartness, Topology, and Uniformity: a Constructive ViewMathematical Logic Quarterly 48 (4): 16-28. 2002.The theory of apartness spaces, and their relation to topological spaces (in the point–set case) and uniform spaces (in the set–set case), is sketched. New notions of local decomposability and regularity are investigated, and the latter is used to produce an example of a classically metrisable apartness on R that cannot be induced constructively by a uniform structure.
-
39The Fan Theorem and Unique Existence of MaximaJournal of Symbolic Logic 71 (2). 2006.The existence and uniqueness of a maximum point for a continuous real—valued function on a metric space are investigated constructively. In particular, it is shown, in the spirit of reverse mathematics, that a natural unique existence theorem is equivalent to the fan theorem
-
39Mathesis Universalis, Computability and Proof (edited book)Springer Verlag. 2019.In a fragment entitled Elementa Nova Matheseos Universalis Leibniz writes “the mathesis [...] shall deliver the method through which things that are conceivable can be exactly determined”; in another fragment he takes the mathesis to be “the science of all things that are conceivable.” Leibniz considers all mathematical disciplines as branches of the mathesis and conceives the mathesis as a general science of forms applicable not only to magnitudes but to every object that exists in our imaginat…Read more
-
37Unique solutionsMathematical Logic Quarterly 52 (6): 534-539. 2006.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. …Read more
-
36From sets and types to topology and analysis: towards practicable foundations for constructive mathematics (edited book)Oxford University Press. 2005.This edited collection bridges the foundations and practice of constructive mathematics and focuses on the contrast between the theoretical developments, which have been most useful for computer science (ie: constructive set and type theories), and more specific efforts on constructive analysis, algebra and topology. Aimed at academic logician, mathematicians, philosophers and computer scientists with contributions from leading researchers, it is up to date, highly topical and broad in scope
-
35A predicative completion of a uniform spaceAnnals of Pure and Applied Logic 163 (8): 975-980. 2012.
-
34The Kripke schema in metric topologyMathematical Logic Quarterly 58 (6): 498-501. 2012.A form of Kripke's schema turns out to be equivalent to each of the following two statements from metric topology: every open subspace of a separable metric space is separable; every open subset of a separable metric space is a countable union of open balls. Thus Kripke's schema serves as a point of reference for classifying theorems of classical mathematics within Bishop-style constructive reverse mathematics
-
33Strong continuity implies uniform sequential continuityArchive for Mathematical Logic 44 (7): 887-895. 2005.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.
-
33A continuity principle, a version of Baire's theorem and a boundedness principleJournal of Symbolic Logic 73 (4): 1354-1360. 2008.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
-
32Evolution and design: The Darwinian view of evolution is a scientific fact and not an ideologyComplexity 11 (1): 12-15. 2005.
-
32Finite Methods in Mathematical PracticeIn Godehard Link (ed.), Formalism and Beyond: On the Nature of Mathematical Discourse, De Gruyter. pp. 351-410. 2014.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 i…Read more
-
30Untamable curiosity, innovation, discovery, and bricolage: Are we doomed to progress to ever increasing complexity?Complexity 11 (5): 9-11. 2006.
-
University of LeedsRegular Faculty
Leeds, West Yorkshire, United Kingdom of Great Britain and Northern Ireland
Areas of Interest
Logic and Philosophy of Logic |
Medieval and Renaissance Philosophy |