Epi-constructivism: Decidable sets of computable numbers as foundational objects for mathematics

As an informal introduction, let us consider the riddle that a friend told me over dinner which motivated this line of research. Versions of the riddle are found in [CSH08].

An infinite number of people numbered $1,2,3,...$ are given time to confer, then they are arranged in a line so that person $n=k$ is facing all the people with $n>k$. Each has a hat with a random natural number placed on their head (the distribution is not important). Each must guess the number on their head, with all but a finite number guessing correctly.

This challenge appears impossible, given that nobody has any information at all about the hat on their head and so they are purely guessing. But the following solution is based on a suggestion attributed in [CSH08] to Yuval Gabay and Michael O’Connor, as graduate students at Cornell University in 2004.

While confering, the people consider all sequences $(a_{i})$ of natural numbers grouped into the equivalence class of sequences which defer at only finitely many positions. The axiom of choise ensures that there is a choice of sequences which includes just one representative of each equivalence class. Imagine the people could make such a choice.

Now once lined up with the hats, each person can see all but finitely many hats, and can therefore determine the equivalence class of the full sequence of hats. They assume that the hats are in fact arranged according to the representative sequence of that equivalence class, and guess their own hat accordingly. Since the real sequence of hats, and the class representative defer at finitely manly places, all but finitely many people guess their own hat correctly.

Of all the paradoxical corollaries of the axiom of choice, it was this one that I find hardest to accept. Clearly while the axoim of choice stiuplates that there exists a choice of a representative of each equivalence class of sequences, this choice could not in fact be constructed. So in what sense does it exist? This riddle motivated a study of whether we could have a foundation of mathematics which only reasons about objects which we can actually represent.

Although we can discuss the axioms of the real numbers $\mathbb{R}$ as an abstract set, it is well known that there is limited opportunity to describe the specific elements of the set, as only countably many elements of $\mathbb{R}$ can be described by any finite expression in any natural or mathematical language; consequently, almost all elements of $\mathbb{R}$ are inherently indescribable. Related to this, it is well known that there is not a unique model of the axioms of $\mathbb{R}$ (there is not even a unique model of the Peano axioms [Pea89] of $\mathbb{N}$), and there are some fundamental undecidable questions regarding the nature of $\mathbb{R}$; for example, the continuum hypothesis that $\mathbb{R}$ doesn’t have a subset strictly larger than $\mathbb{N}$ is undecidable [Coh66].

There some well-known constructive approaches to mathematics. Most work in constructive mathematics focuses on the nature of mathematical proof, namely the banning of proving $\exists x:P(x)$ without finding $x$. With this limitation, the axiom of choice is discarded, or severely limited, and even the simplest choice, the law of excluded middle (LEM), is dropped from logic. Thus, we cannot prove $p\vee q$ without providing at least one of $p$ or $q$. This approach is associated mostly with Brouwer’s intuitionism [Bro23].

Historically, it came as a surprise to many when Bishop showed that a large portion of mathematics survives this limitation [Bis67]. Constructive expositions of real analysis have continued to the present [Abe01, Bri06, DSB06, Bri19].

Here we instead consider what we will call epi-constructivism, so called to distinguish it from constructivism. The principle is that the objects which we wish reason about–the numbers, and more generally the elements in our sets–are constructed explicitly, in the sense that we can write down every object using a string of symbols and that given a string of symbols we can determine in finite time if it is one of our objects or not.

This requirement of constructive objects is orthogonal to the requirement of constructive proofs. That is, we may choose to study only epi-constructive objects, and reject sets like $\mathbb{R}$ which have indescribable elements, but we do not necessarily reject LEM. Conversely, we may accept non-constructive proofs of $\exists x\in\mathbb{R}:P(x)$ without identifying which specific $x$ has the property, while however rejecting the abstract set $\mathbb{R}$ and focusing instead on classes of constructive objects, maintaining that even if one doesn’t know which $x$ has the property, one knows that it is some describable $x$.

It was A. A. Markov who most clearly set an agenda that mathematics should study objects that may be explicitly constructed. Quoting from [Mar62, Mar71]:

Constructive objects are certain figures that are put together in particular ways from elementary figures, which are the elementary constructive objects. An example would be the structures built up with the help of a child’s “Erector” set [like lego]…In constructive mathematical theories we limit ourselves to the consideration of constructive objects of some standard type…One of the simplest types of constructive objects are the words in a particular fixed alphabet. A word in a given alphabet is a string of letters of that alphabet…

Markov constructs the natural numbers, integers, rationals, and finally real numbers in such as way that they can be written as strings of symbols:

The natural numbers are introduced as words 0, 01, 011, … in the alphabet {0, 1}. The rational numbers are introduced as certain words in the alphabet of rational numbers {0, 1, -, /}…  The normal algorithms in this alphabet that take each natural number into some rational number are called constructive sequences of rational numbers…  Let $\mathbb{U}$ be a constructive sequence of rational numbers. We will say that $\mathbb{U}$ converges regularly if $\forall:i\leq j\implies i|\mathbb{U}(i)-\mathbb{U}(j)|<1)$…

We will call proper real numbers the words…  encoding of a regularly convergent sequence. The constructive real numbers…  will be the proper real numbers and the rational numbers.

As paraphrased by [Kus06]:

A pair of algorithms is called a constructive real number if the first algorithm is a constructive sequence of rational numbers and the second effectively estimates the rate of convergence of this sequence. For such constructive real numbers one can define in some natural way the relations of order and equality as well as arithmetical operations.

In other words, the second algorithm gives a modulus of Cauchy convergence to ensure constructively that the first algorithm yields a convergent sequence of rational numbers.

A similar definition may be found, among other equivalent definitions, in [Ric54]

A recursively enumerable sequence of rational numbers $a_{0},a_{1},a_{2},\ldots$ is recursively convergent (r.c.) when there exists a general recursive function $g(x)$ such that $|a_{n}-a_{m}|<\frac{1}{N}$ for $g(N)<n,m$. And a recursive real number is the limit of an r.e., r.c. sequence of rational numbers.

Unfortunately, all the above formulations of constructive real numbers or recursive real numbers fall short of the goal of having decidable elements. Given a pair of algorithms (representing a rational sequence and an explicit Cauchy modulus as in [Kus06]) we cannot decide algorithmically if the second algorithm is indeed a valid modulus of Cauchy convergence for the first, as famously, we cannot even decide if it halts [Tur37]. All of the other definitions suffer from the same limitation. They allow a constructive description of real numbers, but the construction is not decidable; given a string of symbols we cannot generally determine if it represents a real number, particularly whether the algorithm describes a Cauchy sequence of rational numbers. Interestingly, Markov defined the integers and rationals in a decidably constructive manner, but then accepted an undecidably constructive definition of the reals.

This paper offers a preliminary investigation of epi-constructivism, by exploring sets of representations of real numbers (i.e., explicitly constructed convergent sequences of rational numbers) that are decidable in that the “numbers” are represented symbolically (as in Markov’s formulation) but with the additional property that the class is a decidable (/enumerable/computable) set, meaning that given a string of symbols, a terminating algorithm can determine whether it is in the set or not. This also implies that our classes of constructive numbers will be enumerable, i.e., an algorithm can output an enumeration of all the valid constructive real numbers in the classes that we present.

The classes we will consider include Primitive Recursive Computed Numbers (PRCN) which are expressed as a binary power series, where the coefficients are output by a primitive recursive function, and the important generalization of Signed Primitive Recursive Computed Numbers (SPRCN) where the binary power series may have negative coefficients. Finally we consider Generalized Computed Numbers (GCN) which are algorithms that may not have an explicit power series, but where nevertheless we can confirm by inspection that the algorithm outputs a convergent sequence of rationals. This latter broadest group includes the limit of the Specker Sequence which is not normally considered computable.

In exploring decidable constructive real numbers, we may borrow not only from ideas of constructive mathematics, but also from the closely related ideas of computable analysis. Accordingly, we first present a very short survey of useful definitions of computable numbers, as they are closely related to constructive real numbers.

A set is computable (also known as recursive or decidable) if its characteristic function (which maps elements of the set to $1$ and non-elements to $0$) is computable, that is, if a computer program can determine in a finite time whether a given element belongs to the set [Dav58].

The term computable number is variously use in the literature to refer to specific representations (i.e. the algorithm) or to the underlying abstract real number. Henceforth we will use the term computed number to emphasize that we are referring to the concrete representation (or “name”), i.e., the algorithm or computer program that can compute a convergent sequence of rationals. The term computed number does refer to the abstract concept of a real number, which might be computable, nor to the concept from [Abe01] and others of an equivalence class of computed numbers, since these are non-determinable.

This is not an entirely formal definition, as it leaves open the question of the language for algorithms, although per the Church-Turing thesis [Chu36], this may be any Turing-complete language.

There are two desirable properties of a computed number. The first is that every sequence should be infinite, or should declare when it finishes, i.e., we don’t prefer an algorithm which outputs a finite sequence of rational numbers and then fails to halt leaving us in suspense as to whether further rational numbers are forthcoming; rather the algorithm should preferably either output a finite sequence of rational numbers followed by a token representing “finished” (if the represented number is in fact rational) or should output a convergent infinite sequence. We call a computed number with this desirable property a Halting Computed Number, in the sense that each time the program is called upon to produce the next number in the sequence it will halt (not in the sense that the overall sequence halts).

Another desirable property is that every computed number should have an explicit computable modulus of convergence, to enable us to know how long to run the algorithm to reach a given accuracy. We can call this a Modulated Computed Number. Without loss of generality, if we have a constructive method to output a convergent sequence of rationals $(q_{i})$, we call it Modulated if it has a modulus of convergence $|q_{i}-q_{j}|<2^{-i}\,(j>i)$. In case there is a different modulus of convergence, we can simply adapt the algorithm to skip elements and yield, as the $i$th element, the first element for which the modulus of convergence gives $2^{-i}$.

Indeed for many constructive mathematicians, a sequence with an explicit modulus of convergence is the only acceptable Cauchy sequence (this is at least implied by the definition of a Cauchy sequence in [Bis67]).

There are many (Modulated) (Halting) Computed Numbers in the literature quoted above. But our goal in this paper is to explore not individual numbers, but rather classes of computed numbers which are decidably so.

Generally, we will present two useful approaches to defining a class of computed number algorithms for which we can decide deterministically if an algorithm belongs to the class. The first approach suitable for Modulated Halting Computed Numbers is insisting that the sequence has the form of an exponential power sequence $\sum_{i}P(i)2^{-i}$ where the $P(i)$ are in turn given by a well-defined algorithm, guaranteed to halt and output an integer within some bound. This type of Computed Number may be called a Power Series Computed Number.

The second approach, which may produce computed numbers that are not halting or not modulated, is to take any computer program $P$ that outputs a sequence of rationals, and add a constraint to ensure that it outputs a convergent subsequence. We call this approach a Constrained Computed Number and will return to it later.

The most obvious approach to the goal of constructing a decidable class of Modulated Halting Computed Numbers is to represent numbers as a power series with bounded coefficients given by primitive recursive functions. Thus, the Primitive Recursive Computed Numbers are specified using an integer and then a fraction, specified with a power series with the coefficients given by a primitive recursive function. This ensures that the computation to any accuracy will terminate. A naive definition, inspired by Turing’s original definition of a computable number, would be that the primitive recursive function takes an argument $n$ and returns $0$ or $1$ for the $n$th digit of the binary expansion.

Primitive recursive functions are typically defined to be $P^{\prime}:\mathbb{N}\to\mathbb{N}$. But we can simply ignore $P^{\prime}(0)$ and interpret any value $P^{\prime}(i)\geq 1$ as a $1$m thereby giving us a function $P:\mathbb{Z}^{+}\to\{0,1\}$.

By limiting ourselves to primitive recursive functions (which have a decidable syntax and are always total), we can easily validate by means of a simple terminating algorithm whether any given $(I,P(n))$ is a PRCN. Hence, this definition realizes the goal of this paper of mathematical objects that are decidably constructive.

It should be clear that the PRCNs are a decidable class of Computed Numbers, indeed of Modulated Halting Computed Numbers. If we wish to be very strict regarding representing the elements as words in a language, à la Markov, we may write each PRCN as:

$I$ + $\Sigma$ |sgn( $P(i)$ )|*2$\uparrow$(-i)

where for $I$ we substitute any integer O11…or -O11…and for $P(i)$ we substitute the syntactic representation of any primitive recursive function. Note the use of |sgn()| wherein sgn is the sign function and $||$ the absolute value, to constrain the value to $0$ or $1$. The summation implicitly ranges over $i=1,2,3\ldots$. A computer program could determine in finite time if a given string of symbols is in this class.

Indeed, using what is now known as a Markov Algorithm (which Markov called a Normal Algorithm), we can build all the PRCNs with string rewriting rules, beginning with 0+ $\Sigma$ |sgn(i)|*2$\uparrow$(-i) and applying the rules 0$\rightarrow$10, 0$\rightarrow$-0 and rules to repeatedly substitute for (i) syntactic representations of the various primitive recursive functions: constant, successor, projection, composition, and primitive recursion.

Unfortunately, this definition leaves no flexibility. Every real number has a unique binary expansion (except for numbers of the form $I/2^{n}$ which have a finite expansion and classically also have a second representation with infinite trailing $1$’s).

Using this specific definition, it is therefore difficult to provide a Primitive Recursive Computed Number representing a real number as basic as say $\pi$. The reason again is the Table Maker’s Dilemma, namely in order to calculate the $n$th digit in the binary expansion of $\pi$, it is necessary to calculate not an accuracy of $2^{-n}$ but rather an accuracy of $2^{-(n+k)}$ where $k$ is the number of consecutive $0$s or $1$s following the $n$th digit (or $9$’s in decimal). Given that $k$ is not known in advance, there is no obvious primitive recursive function to calculate the $n$th digit, as primitive recursive functions allow only loops with a pre-determined bounded number of iterations.

(For $\pi$ specifically we can leverage the property $\lvert\pi-\frac{p}{q}\rvert\geq q^{-42}$ [Mah53] or better $\lvert\frac{\pi}{\sqrt{3}}-\frac{p}{q}\rvert\geq q^{-4.6016}$ [Hat92] to provide an upper bound on the number of consecutive $1$s (or $9$s) following the $n$th digit and use this bound to create a primitive recursive function which calculates the $n$th digit. But this would not be obvious a priori, and for other transcendental numbers there may not be such a bound.)

Hence the motivation to generalize the definition in the following section.

Again if $P^{\prime}:\mathbb{N}\to\mathbb{N}$ is a primitive recursive function with the traditional domain and co-domain, we interpret the numbers $\{P(i)\}$ ($i>1$) as representing the coefficients $-1,0,1$ respectively depending if $P(i)>1$, $P(i)=0$, $P(i)=1$ respectively.

This generalized definition also gives us computed numbers as recognizable constructive objects in line with the goals of the paper. Syntactically we can write each SPRCN as:

$I$ + $\Sigma^{+}$ sgn( $P(x)$ )*2$\uparrow$(-i)

where again $I$ is the syntatic representation of an integer and $P(x)$ a syntactic representation of a primitive recursive function, and we use the special summation $\Sigma^{+}$ which always takes the absolute value of the first non-zero summand if any.

Although in the abstract sense you could express any number using only the coefficients $0$ and $1$ as a PRCN, by allowing the $P(i)$ to have the value $-1$ we solve the Table Maker’s Dilemma, as we can make corrections. For example if at first we have an estimate $2^{-1}$ or $0.1$ we can later correct it to $0.0111$ by subtracting $2^{-4}$. We will see in a theorem below that this enables us to express most known power series as SPRCNs.

We find SPRCNs to be the most natural and useful decidable class of Computed Numbers, indeed SPRCN is a Decidable class of Modulated Halting Computed Numbers.

It is a apparent that every Signed Primitive Computed Number converges to an abstract computable number in the classical sense, although we will see that the converse is not true. Of course, primitive recursive functions could be substituted with another class of total functions, although primitive recursive functions are widely considered to be the most natural class of functions that are obviously total.

Now we must prove that we can find Signed Primitive Computed Numbers to represent useful irrationals such as $\sqrt{2}$, $\pi$.

For $\sqrt{2}$ we can easily formulate a signed primitive recursive function that initially guesses $2+\frac{1}{2}$ and then seeing that $(2+\frac{1}{2})^{2}>2$ guesses $2+\frac{1}{2}-\frac{1}{4}$, etc., fluctuating above and below $\sqrt{2}$ converging exponentially.

For $\pi$ we can use the Madhava–Leibniz sequence $\pi_{n}=4\,-\,{\frac{4}{3}}\,+\,{\frac{4}{5}}\,-\,{\frac{4}{7}}\,+\,{\frac{4}{9}}\,-\,\cdots\pm\,{\frac{4}{2n-1}}$ which we can rewrite as $3+\frac{7}{15}\,\,\,-\,{\frac{4}{7}}+\,\frac{4}{9}\cdots$. Now we will show that in order to recursively choose $P(i)$ we need to find an $n$ such that $\forall m>n:|\pi_{m}-\pi_{n}|\leq 2^{-i-1}$. In this case $n=2^{i}$ would work. We then choose $P(i)$ so that $|(I+\sum_{i=1}P(i)2^{-i})-\pi_{n}|<2^{-i-1}$.

(Of course in practice we may choose a faster converging series such as the Nilakantha series $\pi=3+{\frac{4}{2\times 3\times 4}}-{\frac{4}{4\times 5\times 6}}+{\frac{4}{6\times 7\times 8}}-{\frac{4}{8\times 9\times 10}}+\cdots$)

We will now formalize this and prove more generally that we have a Signed Primitive Recursive Computed Number (SPRCN) representation for any series of rationals with summands given by primitive recursive functions and with an explicit modulus of Cauchy convergence.

The SPRCN are our most natural decidable class of Computed Numbers. They are well behaved in that they always produce an infinite exponentially convergent sequence of rationals. Moreover as we have seen, the class includes representations of most popular irrationals like the algebraic numbers, $\pi$, $e$ etc. However, they cannot necessarily represent all abstract computable numbers, as our next result shows.

A natural extension (but one that turns out to be of limited use) is to drop the requirement for the function $P$ to be primitive recursive. Thus a Recursive Computed Number is a pair $(I,P(n))$ where $I$ is an integer and $P(n)$ is a recursive function which takes a positive integer and can only return the values $0,1$ where $(I,P(n))$ represents the rational series $I+\sum_{i=1}P(i)2^{-i}$ or equivalently the rational sequence $(I+\sum_{i=1}^{n}P(i)2^{-i})_{n}$ which may terminate as a finite sequence in case some $P(m)$ doesn’t terminate.

In other words, in computing terms, we have an arbitrary computer program constructed to output a sequences of $0,1$ providing the coefficients of a power series. This definition is equivalent to that of the classical computable numbers, restated to be a Modulated Decidable class of Computed Numbers by focusing on the algorithm and removing any reference to the abstract real numbers. That is, we can determine by syntactic inspection if we have a recursive computed number.

However, clearly these recursive computed numbers are not in general Halting and therefore do not provide a satisfying foundation of constructive real numbers, as we may try to output successive rational approximations and be left hanging forever wondering if another approximation is forthcoming.

We could again allow coefficients of $-1$, although a recursive function can calculated ahead an arbitrary number of places so is able to calculate power series without this relaxation.

We suggested an approach of epi-constructionism and explored computable sets of computable numbers, or, equivalently, decidable constructive real numbers. We were able to define Computed Numbers as fundamental objects without relying on the abstraction of real numbers. The Computed Numbers are algorithms which output convergent sequences of rational numbers. This much was well known in the literature. Here we studied Decidable classes of Computed Numbers.

The best behaved class are the Signed Primitive Recursive Computed Numbers given by a binary power series with coefficients yielded by primitive recursive functions, allowing for negative coefficients. This means we can obtain an approximation of the limit to any accuracy in finite time. The class is closed under addition, subtracting and multiplication but there is no division and we cannot in general determine equality of the limit.

A more general class, the Recursive Computed Numbers, corresponds to the concrete representations of the classical computable numbers, but this class is not closed under arithmetic operations and is not “halting” - the algorithm outputting a sequence might become stuck in an infinite loop.

Finally we introduced the Generalized Computed Numbers which admit decidable representations of non-computable numbers such as the Specker limit, and still satisfy the requirement that each Generalized Computed Number has a concrete decidable syntactic representation. However these sequences are not modulated - we do not know when an output sequence will settle down to within a given error range. GCNs might be considered curiosities, they show that the concept of a computable set of computable numbers can stretch to include represent the Specker limit which is not classically a computable number. But GCNs are not a particularly natural set and being unmodulated, are not suitable for computation in practice.

It is the signed primitive recursive computed numbers which are the most likely foundation for a decidably constructive mathematics.

My thanks to Frank Waaldijk, Nachi Avraham Reem, Joshua Fox, Ziv Hellman, Benjamin Fox, Thorsten Altenkirch for their constructive feedback.

No funding was received. The author has no conflicts of interest.