arXiv subjects

Dag Normann

Publications and source records attributed to Dag Normann.

At least 19 recordsLinked to original sources

arXiv2026

The uncountability of the reals and the Axiom of Choice

The uncountability of the reals was first established by Cantor in what was later heralded as the first paper on set theory. Since the latter constitutes the official foundations of mathematics, the logical study of the uncountability of the reals is a worthy endeavour for historical, foundational, and conceptual reasons. In this paper, we shall study the following principle: $\textsf{NIN}_{[0,1]}$: there is no injection from the unit interval to the natural numbers. We show that relatively strong logical systems cannot prove $\textsf{NIN}_{[0,1]}$. In particular, the former system implies second-order arithmetic and fragments of the Axiom of Choice, including dependent choice. We also study the latter choice fragments in Kohlenbach's higher-order Reverse Mathematics.

math.LO↗

arXiv2026

On the computational properties of ambivalent sets and functions

Examples of discontinuous functions already appear in the work of Euler, Abel, Dirichlet, Fourier, and Bolzano. A ground-breaking discovery due to Baire was that many discontinuous functions are well-behaved in that they are the pointwise limit of a sequence of continuous functions; the latter form a class nowadays simply called `Baire 1'. We shall study a class strictly between the semi-continuous and Baire 1 functions, called the ambivalent fuctions. In particular, we investigate the computational properties of the class of ambivalent functions and sets, denoted $\bf Δ$, working with Kleene's S1-S9 schemes. Computational equivalences for various standard operations (supremum, Baire 1 representation, \dots) on $\bf Δ$ are established, including the structure functional $Ω_{\bf Δ}$ that decides if a given ambivalent set is non-empty. A selector is shown to be computable relative to $Ω_{\bf Δ}$ and Kleene's quantifier $\exists^{2}$.

math.LO↗

arXiv2024

On some computational properties of open sets

Open sets are central to mathematics, especially analysis and topology, in ways few notions are. In most, if not all, computational approaches to mathematics, open sets are only studied indirectly via their 'codes' or 'representations'. In this paper, we study how hard it is to compute, given an arbitrary open set of reals, the most common representation, i.e. a countable set of open intervals. We work in Kleene's higher-order computability theory, which was historically based on the S1-S9 schemes and which now has an intuitive lambda calculus formulation due to the authors. We establish many computational equivalences between on one hand the 'structure' functional that converts open sets to the aforementioned representation, and on the other hand functionals arising from mainstream mathematics, like basic properties of semi-continuous functions, the Urysohn lemma, and the Tietze extension theorem. We also compare these functionals to known operations on regulated and bounded variation functions, and the Lebesgue measure restricted to closed sets. We obtain a number of natural computational equivalences for the latter involving theorems from mainstream mathematics.

math.LO↗

arXiv2024

On the computational properties of basic mathematical notions

We investigate the computational properties of basic mathematical notions pertaining to $\mathbb{R}\rightarrow \mathbb{R}$-functions and subsets of $\mathbb{R}$, like finiteness, countability, (absolute) continuity, bounded variation, suprema, and regularity. We work in higher-order computability theory based on Kleene's S1-S9 schemes. We show that the aforementioned italicised properties give rise to two huge and robust classes of computationally equivalent operations, the latter based on well-known theorems from the mainstream mathematics literature. As part of this endeavour, we develop an equivalent $λ$-calculus formulation of S1-S9 that accommodates partial objects. We show that the latter are essential to our enterprise via the study of countably based and partial functionals of type $3$.

math.LO↗

arXiv2024

On two recent extensions of the Big Five of Reverse Mathematics

The program Reverse Mathematics in the foundations of mathematics seeks to identify the minimal axioms required to prove theorems of ordinary mathematics. One always assumes the base theory, a logical system embodying computable mathematics. As it turns out, many (most?) theorems are either provable in said base theory, or equivalent to one of four logical systems, collectively called the Big Five. This paper provides an overview of two recent extensions of the Big Five, working in Kohlenbach's higher-order framework. On one hand, we obtain a large number of equivalences between the second-order Big Five and third-order theorems of real analysis dealing with possibly discontinuous functions. On the other hand, we identify four new 'Big' systems, i.e. boasting many equivalences over the base theory, namely the uncountability of the reals, the Jordan decomposition theorem, the Baire category theorem, and Tao's pigeon hole principle for the Lebesgue measure. We discuss a connection to hyperarithmetical analysis, completing the picture.

math.LO↗

arXiv2024

On sequential theorems in Reverse Mathematics

Many theorems of mathematics have the form that for a certain problem, e.g. a differential equation or polynomial (in)equality, there exists a solution. The sequential version then states that for a sequence of problems, there is a sequence of solutions. The original and sequential theorem can often be proved via the same (or similar) proof and often have the same (or similar) logical properties, esp. if everything is formulated in the language of second-order arithmetic. In this paper, we identify basic theorems of third-order arithmetic, e.g. concerning semi-continuous functions, such that the sequential versions have very different logical properties. In particular, depending on the constructive status of the original theorem, very different and independent choice principles are needed. Despite these differences, the associated Reverse Mathematics, working in Kohlenbach's higher-order framework, is rather elegant and is still based at the core on weak König's lemma.

math.LO↗

arXiv2023

The Biggest Five of Reverse Mathematics

The aim of Reverse Mathematics(RM for short)is to find the minimal axioms needed to prove a given theorem of ordinary mathematics. These minimal axioms are almost always equivalent to the theorem, working over the base theory of RM, a weak system of computable mathematics. The Big Five phenomenon of RM is the observation that a large number of theorems from ordinary mathematics are either provable in the base theory or equivalent to one of only four systems; these five systems together are called the 'Big Five'. The aim of this paper is to greatly extend the Big Five phenomenon as follows: there are two supposedly fundamentally different approaches to RM where the main difference is whether the language is restricted to second-order objects or if one allows third-order objects. In this paper, we unite these two strands of RM by establishing numerous equivalences involving the second-order Big Five systems on one hand, and well-known third-order theorems from analysis about (possibly) discontinuous functions on the other hand. We both study relatively tame notions, like cadlag or Baire 1, and potentially wild ones, like quasi-continuity. We also show that slight generalisations and variations of the aforementioned third-order theorems fall far outside of the Big Five.

math.LO↗

arXiv2022

On robust theorems due to Bolzano, Weierstrass, Cantor, and Jordan

Reverse Mathematics (RM hereafter) is a program in the foundations of mathematics where the aim is to identify the minimal axioms needed to prove a given theorem from ordinary, i.e. non-set theoretic, mathematics. This program has unveiled surprising regularities: the minimal axioms are very often equivalent to the theorem over the base theory, a weak system of 'computable mathematics', while most theorems are either provable in this base theory, or equivalent to one of only four logical systems. The latter plus the base theory are called the 'Big Five' and the associated equivalences are robust following Montalban, i.e. stable under small variations of the theorems at hand. Working in Kohlenbach's higher-order RM, we obtain two long series of equivalences based on theorems due to Bolzano, Weierstrass, Jordan, and Cantor; these equivalences are extremely robust and have no counterpart among the Big Five systems, as they are strictly between the base theory and the higher-order counterpart of weak Koenig's lemma. Thus, higher-order RM is much richer than its second-order cousin, boasting (at least) two extra 'Big' systems.

math.LO↗

arXiv2022

On the logical and computational properties of the Vitali covering theorem

We study a version of the Vitali covering theorem, which we call $\textsf{WHBU}$ and which is a direct weakening of the Heine-Borel theorem for uncountable coverings, called $\textsf{HBU}$. We show that $\textsf{WHBU}$ is central to measure theory by deriving it from various central approximation results related to Littlewood's three principles. A natural question is then how hard it is to prove $\textsf{WHBU}$ (in the sense of Kohlenbach's higher-order Reverse Mathematics}), and how hard it is to compute the objects claimed to exist by $\textsf{WHBU}$ (in the sense of Kleene's schemes S1-S9). The answer to both questions is `extremely hard', as follows: on one hand, in terms of the usual scale of (conventional) comprehension axioms, $\textsf{WHBU}$ is only provable using Kleene's $\exists^{3}$, which implies full second-order arithmetic. On the other hand, realisers (aka witnessing functionals) for $\textsf{WHBU}$, so-called $Λ$-functionals, are computable from Kleene's $\exists^{3}$, but not from weaker comprehension functionals. Despite this hardness, we show that $\textsf{WHBU}$, and certain $Λ$-functionals, behave much better than $\textsf{HBU}$ and the associated class of realisers, called $Θ$-functionals. In particular, we identify a specific $Λ$-functional called $Λ_{\textsf{S}}$ which adds no computational power to the Suslin functional $\textsf{S}^2$, in contrast to $Θ$-functionals. Finally, we introduce a hierarchy involving $Θ$-functionals and $\textsf{HBU}$.

math.LO↗

arXiv2022

On the uncountability of $\mathbb{R}$

Cantor's first set theory paper (1874) establishes the uncountability of $\mathbb{R}$. We study this most basic mathematical fact formulated in the language of higher-order arithmetic. In particular, we investigate the logical and computational properties of NIN (resp. NBI), i.e. the third-order statement: there is no injection (resp. bijection) from $[0,1]$ to $\mathbb{N}$. Working in Kohlenbach's higher-order Reverse Mathematics, we show that NIN and NBI are hard to prove in terms of (conventional) comprehension axioms, while many basic theorems, like Arzela's convergence theorem for the Riemann integral (1885), are shown to imply NIN and/or NBI. Working in Kleene's higher-order computability theory based on S1-S9, we show that the following fourth-order process based on NIN is similarly hard to compute: for a given $[0,1]\rightarrow \mathbb{N}$-function, find reals in the unit interval that map to the same natural number.

math.LO↗

arXiv2021

Betwixt Turing and Kleene

Turing's famous 'machine' model constitutes the first intuitively convincing framework for computing with real numbers. Kleene's computation schemes S1-S9 extend Turing's approach and provide a framework for computing with objects of any finite type. Various research programs have been proposed in which higher-order objects, like functions on the real numbers, are represented/coded as real numbers, so as to make them amenable to the Turing framework. It is then a natural question whether there is any significant difference between the Kleene approach or the Turing-approach-via-codes. Continuous functions being well-studied in this context, we study functions of bounded variation, which have at most countably many points of discontinuity. A central result is the Jordan decomposition theorem that a function of bounded variation on $[0, 1]$ equals the difference of two monotone functions. We show that for this theorem and related results, the difference between the Kleene approach and the Turing-approach-via-codes is huge, in that full second-order arithmetic readily comes to the fore in Kleenes approach, in the guise of Kleene's quantifier $\exists^3$.

math.LO↗

arXiv2020

The Axiom of Choice in Computability Theory and Reverse Mathematics, with a cameo for the Continuum Hypothesis

The Axiom of Choice (AC for short) is the most (in)famous axiom of the usual foundations of mathematics, ZFC set theory. The (non-)essential use of AC in mathematics has been well-studied and thoroughly classified. Now, fragments of countable AC not provable in ZF have recently been used in Kohlenbach's higher-order Reverse Mathematics to obtain equivalences between closely related compactness and local-global principles. We continue this study and show that NCC, a weak choice principle provable in ZF and much weaker systems, suffices for many of these results. In light of the intimate connection between Reverse Mathematics and computability theory, we also study realisers for NCC, i.e. functionals that produce the choice functions claimed to exist by the latter from the other data. Our hubris of undertaking the hitherto underdeveloped study of the computational properties of (choice functions from) AC leads to interesting results. For instance, using Kleene's S1-S9 computation schemes, we show that various total realisers for NCC compute Kleene's $\exists^3$, a functional that gives rise to full second-order arithmetic, and vice versa. By contrast, partial realisers for NCC should be much weaker, but establishing this conjecture remains elusive. By way of catharsis, we show that the Continuum Hypothesis (CH for short) is equivalent to the existence of a countably based partial realiser for NCC. The latter kind of realiser does not compute Kleene's $\exists^3$ and is therefore strictly weaker than a total one.

math.LO↗

arXiv2020

Open sets in computability theory and Reverse Mathematics

To enable the study of open sets in computational approaches to mathematics, lots of extra data and structure on these sets is assumed. For both foundational and mathematical reasons, it is then a natural question, and the subject of this paper, what the influence of this extra data and structure is on the logical and computational properties of basic theorems pertaining to open sets. To answer this question, we study various basic theorems of analysis, like the Baire category, Heine, Heine-Borel, Urysohn, and Tietze theorems, all for open sets given by their (third-order) characteristic functions. Regarding computability theory, the objects claimed to exist by the aforementioned theorems undergo a shift from `computable' to `not computable in any type two functional', following Kleene's S1-S9. Regarding Reverse Mathematics, the latter's so-called Main Question, namely which set existence axioms are necessary for proving a given theorem, does not have a unique or unambiguous answer for the aforementioned theorems, working in Kohlenbach's higher-order framework. A finer study of representations of open sets leads to the new `$Δ$-functional' which has unique (computational) properties.

math.LO↗

arXiv2020

Computability and Non-monotone induction

Non-monotone inductive definitions were studied in the late 1960's and early 1970's with the aim of understanding connections between the complexity of the formulas defining the induction steps and the size of the ordinals measuring the duration of the inductions. In general, any type 2 functional will generate an inductive process, and in this paper we will view non-monotone induction as a functional of type 3. We investigate the associated computation theory inherited from the Kleene schemes and we investigate the nature of the associated companion of sets with codes computable in non-monotone induction. The interest in this functional is motivated from observing that constructions via non-monotone induction appear as natural in classical analysis in its original form. There are two groups of results: We establish strong closure properties of the least ordinal without a code computable in non-monotone induction, and we provide a characterisation of the class of functionals of type 3 computable from non-monotone induction, a characterisation in terms of sequential operators working in transfinite time. We will also see that the full power of non-monotone induction is required when this principle is used to construct functionals witnessing the compactness of the Cantor space and of closed, bounded intervals.

math.LO↗

arXiv2020

Pincherle's theorem in Reverse Mathematics and computability theory

We study the logical and computational properties of basic theorems of uncountable mathematics, in particular Pincherle's theorem, published in 1882. This theorem states that a locally bounded function is bounded on certain domains, i.e. one of the first 'local-to-global' principles. It is well-known that such principles in analysis are intimately connected to (open-cover) compactness, but we nonetheless exhibit fundamental differences between compactness and Pincherle's theorem. For instance, the main question of Reverse Mathematics, namely which set existence axioms are necessary to prove Pincherle's theorem, does not have an unique or unambiguous answer, in contrast to compactness. We establish similar differences for the computational properties of compactness and Pincherle's theorem. We establish the same differences for other local-to-global principles, even going back to Weierstrass. We also greatly sharpen the known computational power of compactness, for the most shared with Pincherle's theorem however. Finally, countable choice plays an important role in the previous, we therefore study this axiom together with the intimately related Lindelöf lemma.

math.LO↗

arXiv2019

Computability Theory, Nonstandard Analysis, and their connections

We investigate the connections between computability theory and Nonstandard Analysis. In particular, we investigate the two following topics and show that they are intimately related. (T.1) A basic property of Cantor space $2^{\mathbb{N}}$ is Heine-Borel compactness: For any open cover of $2^{\mathbb{N}}$, there is a finite sub-cover. A natural question is: How hard is it to compute such a finite sub-cover? We make this precise by analyzing the complexity of functionals that given any $g:2^{\mathbb{N}}\rightarrow \mathbb{N}$, output a finite sequence $\langle f_0 , \dots, f_n\rangle $ in $2^{\mathbb{N}}$ such that the neighbourhoods defined from $\bar{f_i}g(f_i)$ for $i\leq n$ form a cover of Cantor space. (T.2) A basic property of Cantor space in Nonstandard Analysis is Abraham Robinson's nonstandard compactness, i.e. that every binary sequence is `infinitely close' to a standard binary sequence. We analyze the strength of this nonstandard compactness property of Cantor space, compared to the other axioms of Nonstandard Analysis and usual mathematics. The study of (T.1) gives rise to exotic objects in computability theory, while (T.2) leads to surprising results in Reverse Mathematics. We stress that (T.1) and (T.2) are highly intertwined and that our study of these topics is `holistic' in nature: results in computability theory give rise to results in Nonstandard Analysis and vice versa.

math.LO↗

arXiv2019

The strength of compactness in Computability Theory and Nonstandard Analysis

Compactness is one of the core notions of analysis: it connects local properties to global ones and makes limits well-behaved. We study the computational properties of the compactness of Cantor space $2^{\mathbb{N}}$ for uncountable covers. The most basic question is: how hard is it to compute a finite sub-cover from such a cover of $2^{\mathbb{N}}$? Another natural question is: how hard is it to compute a sequence that covers $2^{\mathbb{N}}$ minus a measure zero set from such a cover? The special and weak fan functionals respectively compute such finite sub-covers and sequences. In this paper, we establish the connection between these new fan functionals on one hand, and various well-known comprehension axioms on the other hand, including arithmetical comprehension, transfinite recursion, and the Suslin functional. In the spirit of Reverse Mathematics, we also analyse the logical strength of compactness in Nonstandard Analysis. Perhaps surprisingly, the results in the latter mirror (often perfectly) the computational properties of the special and weak fan functionals. In particular, we show that compactness (nonstandard or otherwise) readily brings us to the outer edges of Reverse Mathematics (namely $Π_2^1$-CA$_0$), and even into Schweber's higher-order framework (namely $Σ_{1}^{2}$-separation).

math.LO↗

arXiv2019

On the mathematical and foundational significance of the uncountable

We study the logical and computational properties of basic theorems of uncountable mathematics, including the Cousin and Lindelöf lemma published in 1895 and 1903. Historically, these lemmas were among the first formulations of open-cover compactness and the Lindelöf property, respectively. These notions are of great conceptual importance: the former is commonly viewed as a way of treating uncountable sets like e.g. $[0,1]$ as 'almost finite', while the latter allows one to treat uncountable sets like e.g. $\mathbb{R}$ as 'almost countable'. This reduction of the uncountable to the finite/countable turns out to have a considerable logical and computational cost: we show that the aforementioned lemmas, and many related theorems, are extremely hard to prove, while the associated sub-covers are extremely hard to compute. Indeed, in terms of the standard scale (based on comprehension axioms), a proof of these lemmas requires at least the full extent of second-order arithmetic, a system originating from Hilbert-Bernays' Grundlagen der Mathematik. This observation has far-reaching implications for the Grundlagen's spiritual successor, the program of Reverse Mathematics, and the associated Gödel hierachy. We also show that the Cousin lemma is essential for the development of the gauge integral, a generalisation of the Lebesgue and improper Riemann integrals that also uniquely provides a direct formalisation of Feynman's path integral.

math.LO↗