•  115
    Linear independence without choice
    with Douglas Bridges and Fred Richman
    Annals 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
  •  157
    Countable choice as a questionable uniformity principle
    Philosophia 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.
  •  101
    Compactness under constructive scrutiny
    with Hajime Ishihara
    Mathematical Logic Quarterly 50 (6): 540-550. 2004.
    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 co…Read more
  •  147
    The Fan Theorem and Unique Existence of Maxima
    with Josef Berger and Douglas Bridges
    Journal 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
  •  105
    Strong continuity implies uniform sequential continuity
    with Douglas Bridges, Hajime Ishihara, and Luminiţa Vîţa
    Archive 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.
  •  78
    Corrigendum to “Unique solutions”
    Mathematical Logic Quarterly 53 (2): 214-214. 2007.
  •  84
    On the contrapositive of countable choice
    with Hajime Ishihara
    Archive for Mathematical Logic 50 (1-2): 137-143. 2011.
    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 …Read more
  •  54
    The Kripke schema in metric topology
    with Robert Lubarsky and Fred Richman
    Mathematical 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