The anti‐Specker property,positivity, and total boundedness

Working within Bishop‐style constructive mathematics, we examine some of the consequences of the anti‐Specker property, known to be equivalent to a version of Brouwer's fan theorem. The work is a contribution to constructive reverse mathematics (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The Banach‐Steinhaus theorem for the space 𝒟(ℝ) in constructive analysis

We prove the Banach‐Steinhaus theorem for distributions on the space ??(?) within Bishop's constructive mathematics. To this end, we investigate the constructive sequential completion (?) of ??(?).     

Henselian valued fields: a constructive point of view

This article is a logical continuation of the Henri Lombardi and Franz‐Viktor Kuhlmann article [9]. We address some classical points of the theory of valued fields with an elementary and constructive point of view. We deal with Krull valuations, and not simply discrete valuations. First of all, we show how (in the spirit of [9]) to construct the Henselization of a valued field; we restrict to fields in which one has at one's disposal algorithmic tools to test the nullity or the valuation ring membership. It is therefore a work that differs as much in spirit as in field of application from that of Mines, Richman and Bridges (cf. [10]), who address the framework of Heyting fields and discrete valuation. We show then in a constructive way a batch of classical results in Henselian fields, notably factorization criteria and Krasner's Lemma. We conclude by a construction of the inertia field of a valued field. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The constructive completion of the space 𝒟(ℝ)

We prove in the framework of Bishop's constructive mathematics that the sequential completion $ \tilde {\cal D} $(?) of the space ??(?) is filter‐complete. Then it follows as a corollary that the filter‐completeness of ??(?) is equivalent to the principle BD‐?, which can be proved in classical mathematics, Brouwer's intuitionistic mathematics and constructive recursive mathematics of Markov's school, but does not in Bishop's constructive mathematics. We also show that $ \tilde {\cal D} $(?) is identical with the filter‐completion which was provided by Bishop. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Unique solutions

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. (© 2006 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A constructive proof of the Peter‐Weyl theorem

We present a new and constructive proof of the Peter‐Weyl theorem on the representations of compact groups. We use the Gelfand representation theorem for commutative C*‐algebras to give a proof which may be seen as a direct generalization of Burnside's algorithm [3]. This algorithm computes the characters of a finite group. We use this proof as a basis for a constructive proof in the style of Bishop. In fact, the present theory of compact groups may be seen as a natural continuation in the line of Bishop's work on locally compact, but Abelian, groups [2]. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Powers of positive elements in C*‐algebras

In this paper, we show that Ogasawa’s theorem has a proof in Bishop style constructive mathematics (BISH). In 25 , we introduced the elementary constructive theory of C*‐algebras in BISH, but we did not discuss the powers of positive elements there. © 2011 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim     

On proximal convergence in uniform spaces

The paper deals with proximal convergence and Leader's theorem, in the constructive theory of uniform apartness spaces. (© 2003 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

On Farkas' lemma and related propositions in BISH

In this paper we analyse in the framework of constructive mathematics (BISH) the validity of Farkas' lemma and related propositions, namely the Fredholm alternative for solvability of systems of linear equations, optimality criteria in linear programming, Stiemke's lemma and the Superhedging Duality from mathematical finance, and von Neumann's minimax theorem with application to constructive game theory.     

On a theorem of Wald and Wolfowitz on randomization in statistics

In [9] it is proved that to each randomized decision function, there exists an equivalent randomized decision rule (cf. [3]), provided that the space of decisions is Polish. The object of the present paper is to show that the above theorem is a special case of risk-equivalence (cf. [5]) even if the space of decisions is analytic.     

A Definitive Constructive Open Mapping Theorem?

It is proved, within Bishop's constructive mathematics (BISH), that, in the context of a Hilbert space, the Open Mapping Theorem is equivalent to a principle that holds in intuitionistic mathematics and recursive constructive mathematics but is unlikely to be provable within BISH.     

Compactness under constructive scrutiny

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. (© 2004 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The Kripke schema in metric topology

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.     

The anti-Specker property, a Heine–Borel property, and uniform continuity

Working within Bishop’s constructive framework, we examine the connection between a weak version of the Heine–Borel property, a property antithetical to that in Specker’s theorem in recursive analysis, and the uniform continuity theorem for integer-valued functions. The paper is a contribution to the ongoing programme of constructive reverse mathematics.     

Gorenstein quivers

In this paper we characterize when the path ring associated to a quiver is Gorenstein (in the sense of Iwanaga [9]). Then, by using the notion of a Gorenstein category (cf. [2]), we extend the classes of quivers whose corresponding category of representations has finite Gorenstein global dimension. This extension includes non-noetherian quivers. E. E., S.E., and J.R.G.R., partially supported by the DGI MTM2005-03227. Estrada’s work was supported by a MEC/Fulbright grant from the Spanish Secretaría de Estado de Universidades e Investigación del Ministerio de Educación y Ciencia. Received: 28 February 2006     

Comparison of Picard groups in dimension 1

We compare two Picard groups in dimension 1. Our proofs are constructive and the results generalize a theorem of J. Sands [11]. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Hilbert C*-Modules over Monotone Complete C*-Algebras

The aim of the present paper is to describe self-duality and C*-reflexivity of Hilbert A-modules ?? over monotone complete C*-algebras A by the completeness of the unit ball of ?? with respect to two types of convergence being defined, and by a structural criterion. The derived results generalize earlier results ofH. Widom [Duke Math. J. 23, 309-324, MR 17 # 1228] and W. L. Paschke [Trans. Amer. Mat. Soc. 182 , 443-468, MR 50 # 8087, Canadian J. Math. 26, 1272-1280, MR 57 # 10433]. For Hilbert C*-modules over commutative AW*-algebras the equivalence of the self-duality property and of the Kaplansky-Hilbert property is reproved, (cf. M. Ozawa [J. Math. Soc. Japan 36, 589-609, MR 85 # 46068]). Especially, one derives that for a C*-algebra A the A-valued inner product of every Hilbert A-module ?? can be continued to an A-valued inner product on it's A-dual Banach A-module ??' turning ??' to a self-dual Hilbert A-module if and only if A is monotone complete (or, equivalently, additively complete) generalizing a result of M. Hamana [Internat. J. Math. 3 (1992), 185 - 204]. A classification of countably generated self-dual Hilbert A-modules over monotone complete C*-algebras A is established. The set of all bounded module operators End ′(??) on self-dual Hilbert A-modules ?? over monotone complete C*-algebras A is proved again to be a monotone complete C*-algebra. Applying these results a Weyl-Berg type theorem is proved.     

Filtered and stable boolean powers are relativized full boolean powers

The question whether the extended theorem of Feferman and Vaught (cf. Comer [7], Volger [13]) can be applied to filtered boolean powers with arbitrary base was raised by J. H. Schmerl [11]. It can be answered with the help of a relativized version of the theorem (cf. Comer [7], Volger [12], [14]) which seems to have escaped notice. Therefore we shall present in this note a precise formulation of the relativized version and apply it to filtered boolean powers with arbitrary base and to stable boolean powers with finite base and finite group. The former application was mentioned in Comer [7]. The latter application yields a decidability result which seems to be new. The question whether the second application can be extended to arbitrary bases remains open.Presented by E. Nelson.     

Specker sequences revisited

Specker sequences are constructive, increasing, bounded sequences of rationals that do not converge to any constructive real. A sequence is said to be a strong Specker sequence if it is Specker and eventually bounded away from every constructive real. Within Bishop's constructive mathematics we investigate non‐decreasing, bounded sequences of rationals that eventually avoid sets that are unions of (countable) sequences of intervals with rational endpoints. This yields surprisingly straightforward proofs of certain basic results fromconstructive mathematics. Within Russian constructivism, we show how to use this general method to generate Specker sequences. Furthermore, we show that any nonvoid subset of the constructive reals that has no isolated points contains a strictly increasing sequence that is eventually bounded away from every constructive real. If every neighborhood of every point in the subset contains a rational number different from that point, the subset contains a strong Specker sequence. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

Extending the disjoint‐representatives theorems of Hall,Halmos, and Vaughan to list‐multicolorings of graphs

Philip Hall's famous theorem on systems of distinct representatives and its not‐so‐famous improvement by Halmos and Vaughan (1950) can be regarded as statements about the existence of proper list‐colorings or list‐multicolorings of complete graphs. The necessary and sufficient condition for a proper “coloring” in these theorems has a rather natural generalization to a condition we call Hall's condition on a simple graph G, a vertex list assignment to G, and an assignment of nonnegative integers to the vertices of G. Hall's condition turns out to be necessary for the existence of a proper multicoloring of G under these assignments. The Hall‐Halmos‐Vaughan theorem may be stated: when G is a clique, Hall's condition is sufficient for the existence of a proper multicoloring. In this article, we undertake the study of the class HHV of simple graphs G for which Hall's condition is sufficient for the existence of a proper multicoloring. It is shown that HHV is contained in the class ℋ︁₀ of graphs in which every block is a clique and each cut‐vertex lies in exactly two blocks. On the other hand, besides cliques, the only connected graphs we know to be in HHV are (i) any two cliques joined at a cut‐vertex, (ii) paths, and (iii) the two connected graphs of order 5 in ℋ︁₀, which are neither cliques, paths, nor two cliques stuck together. In case (ii), we address the constructive aspect, the problem of deciding if there is a proper coloring and, if there is, of finding one. © 2000 John Wiley & Sons, Inc. J Graph Theory 33: 199–219, 2000