Searcharxiv⌕ Search

arXiv subjects

Douglas S. Bridges

Publications and source records attributed to Douglas S. Bridges.

11 recordsLinked to original sources
arXiv2026

Notes on q-normed Spaces in Constructive Analysis

What we call q-normed (linear) spaces were introduced (under the name pseudonormed spaces) into constructive analysis by D.L. Johns as a means of handling spaces, such as L-infinity, in which not all elements are constructively normable. We prove a number of q-normed-space analogues/generalisations of standard theorems in the constructive analysis of normed linear spaces, and give examples showing that analogues of two of those theorems are essentially nonconstructive.

math.FA↗
arXiv2026

Axiomatic Justification in Constructive Morse Set Theory

Working within Constructive Morse Set Theory (CMST), we introduce axioms for a new notion, jst Pp, intended to capture what it means for P to prove, or justify, p under the BHK interpretation of intuitionistic logic. Since it makes no distinction between terms and formulae -- every term is also a formula, and vice versa -- CMST is well suited to our axiomatic development of justification theory within set theory itself. After stating our axioms for jst Pp, we derive many consequences thereof. In particular, we show that (with certain restrictions) our axioms for jst Pp align with the intended BHK interpretations of the axioms of intuitionistic logic.

math.LO↗
arXiv2026

Constructive Notes on Locally Convex Spaces

We give a detailed, corrected presentation of some fundamentals of the constructive theory of locally convex spaces that appear without proofs in BVtech . This suffices for some important functional analytic theorems that are stated in our final section.

math.FA↗
arXiv2026

On Constructive Connectedness Properties

We plug two gaps in the constructive proof of Theorem 1 (respectively, Theorem 2) in dsb , showing that the property of C-connectedness (respectively, O-connectedness) of a subset S of R is equivalent to S containing the interval [a,b] (respectively, (a,b)) whenever a and b are in S and a < b.

math.LO↗
arXiv2026

Monotone convergence theorems equivalent to Markov's principle

The notions of provisional, negative, and apparent convergence to 0 are introduced. It is then shown that Markov's principle is equivalent, in Bishop-style constructive mathematics, to the statement `every decreasing sequence of real numbers provisionally convergent to 0 actually converges to 0', and that this equivalence holds with `provisionally' replaced by `negatively'. Finally, apparent convergence and convergence are related by means of the anti-Specker principle.

math.LO↗
arXiv2026

Closing in on the kernel of an operator between Banach spaces

This note deals with the question: If T is a linear mapping between Banach spaces X and Y, and x belongs to X and has small norm, is x close to the kernel of T? It draws on notions of Z-stability and provides an affirmative constructive answer when T is onto Y, sequentially continuous, and has located kernel.

math.FA↗
arXiv2025

Metric Double Complements of Convex Sets

In constructive mathematics the metric complement of a subset S of a metric space X is the set -S of points in X that are bounded away from S. In this note we discuss, within Bishop's constructive mathematics, the connection between the metric double complement, -(-K), and the logical double complement, not not K, where K is a convex subset of a normed linear space X. In particular, we prove that if K has inhabited interior, then -(-K) equals the interior of not not K, that the hypothesis of inhabited interior can be dropped in the finite-dimensional case, and that we cannot constructively replace the interior of not not K by that of K in these results.

math.LO↗
arXiv2025

Affine Hulls and Simplices: a Constructive Analysis

This paper deals with certain fundamental results about affine hulls and simplices in a real normed linear space. The framework of the paper is Bishop's constructive mathematics, which, with its characteristic interpretation of existence as constructibility, often involves more subtle estimation than its classical-logic-based counterpart. As well as technically more involved proofs (for example, that of Theorem 29 on the perturbation of vertices), we have included a number of elementary ones for completeness of exposition.

math.LO↗
arXiv2025

On the Constructive Theory of Jordan Curves

Using a definition of Jordan curve similar to that of Dieudonné, we prove that our notion is equivalent to that used by Berg et al. in their constructive proof of the Jordan Curve Theorem. We then establish a number of properties of Jordan curves and their corresponding index functions, including the important Proposition 32 and its corollaries about lines crossing a Jordan curve at a smooth point. The final section is dedicated to proving that the index of a point with respect to a piecewise smooth Jordan curve in the complex plane is identical to the familiar winding number of the curve around that point. The paper is written within the framework of Bishop's constructive analysis. Although the work in Sections 3--5 is almost entirely new, the paper contains a substantial amount of expository material for the benefit of the reader.

math.LO↗
arXiv2024

Improving Cauchy's Theorem in Constructive Analysis

In his constructive development of complex analysis, Errett Bishop used restrictive notions of homotopy and simple connectedness. Working in Bishop-style constructive mathematics, we prove Cauchy's integral theorem using the standard notions of such properties. In consequence, Bishop's theorems in Chapters 5 of [1, 2] hold under our more normal, less restrictive, definitions.

math.LO↗