Proof-theoretic conservations of weak weak intuitionistic constructive set theories

The paper aims to provide precise proof theoretic characterizations of Myhill–Friedman-style “weak” constructive extensional set theories and Aczel–Rathjen analogous constructive set theories both enriched by Mostowski-style collapsing axioms and/or related anti-foundation axioms. The main results include full intuitionistic conservations over the corresponding purely arithmetical formalisms that are well known in the reverse mathematics – which strengthens analogous results obtained by the author in the 80s. The present research was inspired by the more recent Sato-style “weak weak” classical extensional set theories whose proof theoretic strengths are shown to strongly exceed the ones of the intuitionistic counterparts in the presence of the collapsing axioms.     

The axiom of choice and the law of excluded middle in weak set theories

A weak form of intuitionistic set theory WST lacking the axiom of extensionality is introduced. While WST is too weak to support the derivation of the law of excluded middle from the axiom of choice, we show that bee.ng up WST with moderate extensionality principles or quotient sets enables the derivation to go through. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

The computable Lipschitz degrees of computably enumerable sets are not dense

The computable Lipschitz reducibility was introduced by Downey, Hirschfeldt and LaForte under the name of strong weak truth-table reducibility (Downey et al. (2004) [6]). This reducibility measures both the relative randomness and the relative computational power of real numbers. This paper proves that the computable Lipschitz degrees of computably enumerable sets are not dense. An immediate corollary is that the Solovay degrees of strongly c.e. reals are not dense. There are similarities to Barmpalias and Lewis’ proof that the identity bounded Turing degrees of c.e. sets are not dense (George Barmpalias, Andrew E.M. Lewis (2006) [2]), however the problem for the computable Lipschitz degrees is more complex.     

Locatedness and overt sublocales

Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected.Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact set is Bishop compact iff it is located. We translate this result to formal topology. ‘Bishop compact’ is translated as compact and overt. We propose a definition of locatedness on subspaces of a formal topology, and prove that a closed subspace of a compact regular formal space is located iff it is overt. Moreover, a Bishop-closed subset of a complete metric space is Bishop compact — that is, totally bounded and complete — iff its localic completion is compact overt.Finally, we show by elementary methods that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales.We work constructively, predicatively and avoid the use of the axiom of countable choice.     

Injective power objects and the axiom of choice

“The axiom of choice states that any set X of non-empty sets has a choice function—i.e. a function satisfying f(x)∈x for all x∈X. When we want to generalise this to a topos, we have to choose what we mean by non-empty, since in , the three concepts non-empty, inhabited, and injective are equivalent, so the axiom of choice can be thought of as any of the three statements made by replacing “non-empty” by one of these notions.It seems unnatural to use non-empty in an intuitionistic context, so the first interpretation to be used in topos theory was the notion based on inhabited objects. However, Diaconescu (1975) [1] showed that this interpretation implied the law of the excluded middle, and that without the law of the excluded middle, even the finite version of the axiom of choice does not hold! Nevertheless some people still view this as the most appropriate formulation of the axiom of choice in a topos.In this paper, we study the formulation based upon injective objects. We argue that it can be considered a more natural formulation of the axiom of choice in a topos, and that it does not have the undesirable consequences of the inhabited formulation. We show that if it holds for , then it holds in a wide variety of topoi, including all localic topoi. It also has some of the classical consequences of the axiom of choice, although a lot of classical results rely on both the axiom of choice and the law of the excluded middle. An additional advantage of this formulation is that it can be defined for a slightly more general class of categories than just topoi.We also examine the corresponding injective formulations of Zorn’s lemma and the well-order principle. The injective form of Zorn’s lemma is equivalent to the axiom of injective choice, and the injective well-order principle implies the axiom of injective choice.     

Independence results for variants of sharply bounded induction

The theory , axiomatized by the induction scheme for sharply bounded formulae in Buss’ original language of bounded arithmetic (with ⌊x/2⌋ but not ⌊x/2^y⌋), has recently been unconditionally separated from full bounded arithmetic S₂. The method used to prove the separation is reminiscent of those known from the study of open induction.We make the connection to open induction explicit, showing that models of can be built using a “nonstandard variant” of Wilkie’s well-known technique for building models of IOpen. This makes it possible to transfer many results and methods from open to sharply bounded induction with relative ease.We provide two applications: (i) the Shepherdson model of IOpen can be embedded into a model of , which immediately implies some independence results for ; (ii) extended by an axiom which roughly states that every number has a least 1 bit in its binary notation, while significantly stronger than plain , does not prove the infinity of primes.     

Realisability in weak systems of explicit mathematics

This paper is a direct successor to 12 . Its aim is to introduce a new realisability interpretation for weak systems of explicit mathematics and use it in order to analyze extensions of the theory PET in 12 by the so‐called join axiom of explicit mathematics.     

The axiomatic power of Kolmogorov complexity

The famous Gödel incompleteness theorem states that for every consistent, recursive, and sufficiently rich formal theory T there exist true statements that are unprovable in T. Such statements would be natural candidates for being added as axioms, but how can we obtain them? One classical (and well studied) approach is to add to some theory T an axiom that claims the consistency of T  . In this paper we discuss another approach motivated by Chaitin's version of Gödel's theorem where axioms claiming the randomness (or incompressibility) of some strings are probabilistically added, and show that it is not really useful, in the sense that this does not help us prove new interesting theorems. This result answers a question recently asked by Lipton. The situation changes if we take into account the size of the proofs: randomly chosen axioms may help making proofs much shorter (unless NP=PSPACE$\mathrm{NP}=\mathrm{PSPACE}$).     

Itô’s stochastic calculus: Its surprising power for applications

We trace Itô’s early work in the 1940s, concerning stochastic integrals, stochastic differential equations (SDEs) and Itô’s formula. Then we study its developments in the 1960s, combining it with martingale theory. Finally, we review a surprising application of Itô’s formula in mathematical finance in the 1970s. Throughout the paper, we treat Itô’s jump SDEs driven by Brownian motions and Poisson random measures, as well as the well-known continuous SDEs driven by Brownian motions.     

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.     

Sets versus trial sequences,Hausdorff versus von Mises: “Pure” mathematics prevails in the foundations of probability around 1920

The paper discusses the tension which occurred between the notions of set (with measure) and (trial-) sequence (or—to a certain degree—between nondenumerable and denumerable sets) when used in the foundations of probability theory around 1920. The main mathematical point was the logical need for measures in order to describe general nondiscrete distributions, which had been tentatively introduced before (1919) based on von Mises’s notion of the “Kollektiv.” In the background there was a tension between the standpoints of pure mathematics and “real world probability” (in the words of J.L. Doob) at the time. The discussion and publication in English translation (in Appendix) of two critical letters of November 1919 by the “pure” mathematician Felix Hausdorff to the engineer and applied mathematician Richard von Mises compose about one third of the paper. The article also investigates von Mises’s ill-conceived effort to adopt measures and his misinterpretation of an influential book of Constantin Carathéodory. A short and sketchy look at the subsequent development of the standpoints of the pure and the applied mathematician—here represented by Hausdorff and von Mises—in the probability theory of the 1920s and 1930s concludes the paper.     

Low upper bounds in the LR degrees

We say that A≤_LRB if every B-random real is A-random—in other words, if B has at least as much derandomization power as A. The LR reducibility is a natural weak reducibility in the context of randomness, and generalizes lowness for randomness. We study the existence and properties of upper bounds in the context of the LR degrees. In particular, we show that given two (or even finitely many) low sets, there is a low c.e. set which lies LR above both. This is very different from the situation in the Turing degrees, where Sacks’ splitting theorem shows that two low sets can join to 0^′.     

A measure-theoretic proof of Turing incomparability

We prove that if S is an ω-model of weak weak König’s lemma and , is incomputable, then there exists , such that A and B are Turing incomparable. This extends a recent result of Ku?era and Slaman who proved that if S₀ is a Scott set (i.e. an ω-model of weak König’s lemma) and A∈S₀, A⊆ω, is incomputable, then there exists B∈S₀, B⊆ω, such that A and B are Turing incomparable.     

Nonstandard arithmetic and recursive comprehension

First order reasoning about hyperintegers can prove things about sets of integers. In the author’s paper Nonstandard Arithmetic and Reverse Mathematics, Bulletin of Symbolic Logic 12 (2006) 100-125, it was shown that each of the “big five” theories in reverse mathematics, including the base theory , has a natural nonstandard counterpart. But the counterpart of has a defect: it does not imply the Standard Part Principle that a set exists if and only if it is coded by a hyperinteger. In this paper we find another nonstandard counterpart, , that does imply the Standard Part Principle.     

God, king, and geometry: revisiting the introduction to Cauchy’s Cours d’analyse

This article offers a systematic reading of the introduction to Augustin-Louis Cauchy’s landmark 1821 mathematical textbook, the Cours d’analyse. Despite its emblematic status in the history of mathematical analysis and, indeed, of modern mathematics as a whole, Cauchy’s introduction has been more a source for suggestive quotations than an object of study in its own right. Cauchy’s short mathematical metatext offers a rich snapshot of a scholarly paradigm in transition. A close reading of Cauchy’s writing reveals the complex modalities of the author’s epistemic positioning, particularly with respect to the geometric study of quantities in space, as he struggles to refound the discipline on which he has staked his young career.     

Three models for the homotopy theory of homotopy theories

Given any model category, or more generally any category with weak equivalences, its simplicial localization is a simplicial category which can rightfully be called the “homotopy theory” of the model category. There is a model category structure on the category of simplicial categories, so taking its simplicial localization yields a “homotopy theory of homotopy theories”. In this paper we show that there are two different categories of diagrams of simplicial sets, each equipped with an appropriate definition of weak equivalence, such that the resulting homotopy theories are each equivalent to the homotopy theory arising from the model category structure on simplicial categories. Thus, any of these three categories with the respective weak equivalences could be considered a model for the homotopy theory of homotopy theories. One of them in particular, Rezk’s complete Segal space model category structure on the category of simplicial spaces, is much more convenient from the perspective of making calculations and therefore obtaining information about a given homotopy theory.     

An axiom system for Lingenberg’s metric-Euclidean planes

We show that Lingenbergs metric-Euclidean planes are the rectangular planes of Karzel and Stanik which satisfy the axiom If two of the perpendicular bisectors of a triangle exist, then so does the third.This paper was written while the author was at the Institute of Mathematics of University of Biaystok with a Fulbright grant. I thank the Polish-U.S. Fulbright Commission for the grant, Professor Krzysztof Pramowski for the hospitality, and Ewa Walecka for drawing the figures.     

A note on the maximum correlation for Baker’s bivariate distributions with fixed marginals

We investigate Baker’s bivariate distributions with fixed marginals which are based on order statistics, and find conditions under which the correlation converges to the maximum for Fréchet-Hoeffding upper bound as the sample size tends to infinity. The convergence rate of the correlation is also investigated for some specific cases.     

Spaces of orders and their Turing degree spectra

We investigate computability theoretic and topological properties of spaces of orders on computable orderable groups. A left order on a group G is a linear order of the domain of G, which is left-invariant under the group operation. Right orders and bi-orders are defined similarly. In particular, we study groups for which the spaces of left orders are homeomorphic to the Cantor set, and their Turing degree spectra contain certain upper cones of degrees. Our approach unifies and extends Sikora’s (2004) [28] investigation of orders on groups in topology and Solomon’s (2002) [31] investigation of these orders in computable algebra. Furthermore, we establish that a computable free group F_n of rank n>1 has a bi-order in every Turing degree.     

Canonical subbase-compactness of topological products

For topological products the concept of canonical subbase-compactness is introduced, and the question analyzed under what conditions such products are canonically subbase-compact in ZF-set theory.Results: (1) Products of finite spaces are canonically subbase-compact iff AC(fin), the axiom of choice for finite sets, holds.(2) Products of n-element spaces are canonically subbase-compact iff AC(<n), the axiom of choice for sets with less than n elements, holds.(3) Products of compact spaces are canonically subbase-compact iff AC, the axiom of choice, holds.(4) All powers XI of a compact space X are canonically subbase compact iff X is a Loeb-space.These results imply that in ZF the implications