•  80
    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
  •  53
    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
  •  34
    A direct proof of Wiener's theorem
    with Matthew Hendtlass
    In S. Barry Cooper (ed.), How the World Computes, . pp. 293--302. 2012.
  •  77
    Formal Zariski topology: positivity and points
    Annals of Pure and Applied Logic 137 (1-3): 317-359. 2006.
    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
  •  93
    Quasi-apartness and neighbourhood spaces
    with Hajime Ishihara, Ray Mines, and Luminiţa Vîţă
    Annals of Pure and Applied Logic 141 (1): 296-306. 2006.
    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
  •  97
    A predicative completion of a uniform space
    with Josef Berger, Hajime Ishihara, and Erik Palmgren
    Annals of Pure and Applied Logic 163 (8): 975-980. 2012.
  •  138
    A continuity principle, a version of Baire's theorem and a boundedness principle
    with Hajime Ishihara
    Journal 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