It is a ubiquitous opinion among mathematicians that a real number is just a point in the (real) line. If this rough definition is not enough, then a mathematician may provide a formal definition of the real numbers in the set theoretical and axiomatic fashion, i.e. via Cauchy sequences or Dedekind cuts, or as the collection of axioms (up to isomorphism) characterizing exactly the set of real number as the complete and totally ordered Archimedean field. Actually, the above notions of the real numbers are abstract and do not have a constructive grounding. Definition of Cauchy sequences, and equivalence classes of these sequences explicitly use the actual infinity. The same is for Dedekind cuts, where the set of rational numbers is used as actual infinity. Although there is no direct constructive grounding for the above abstract notions, there are so called intuitions on which they are based. A rigorous approach to express these very intuition in a constructive way is proposed. It is based on the concept of the adjacency relation that seems to be a missing primitive concept in type theory.
In the XIX century and at the beginning of the XX century there was a common view that Continuum cannot be reduced to numbers, that is, Continuum cannot be identified with the set of the real numbers, and in general with a compact connected metric space. Real numbers are defined on the basis of rational numbers as equivalence classes of Cauchy sequences, or Dedekind cuts.
The following citations support this view.
David Hilbert [
Emile Borel [
Luitzen E. J. Brouwer [
Intuitively, continuum (as an object) can be divided finitely many times, so that the resulting parts are of the same type as the original continuum. Two adjacent parts can be united, and the result is of the same type as the original continuum.
Recently, see HoTT [
The Continuum is defined in HoTT as the real numbers via Cauchy sequences. Since the intuitive notion of Continuum is common for all humans (not only for mathematicians), the computational grounding of the Continuum (as a primitive type) must be simple and obvious. The grounding, proposed in the paper, is extremely simple, and may be seen as naive. Actually, it is based on the Brouwer’s notion of Continuum. The introduced new primitive types along with constructors, primitive operations and primitive relations should be seen as the second part of the general framework for a constructive type theory presented in the paper Functionals and hardware, see https://arxiv.org/abs/1501.03043 .
Although mainly the grounding of the Euclidean Continua (the unit interval in particular) is presented in following section, the investigation has been extended to the generic notion of Continuum and various interesting related topological spaces. The main idea is simple and is based on W-types augmented with simply patterns of adjacency relation.
Relations may be introduced as functions with the Boolean type as co-domain. However, the Curry-Howard correspondence: propositions as types and proofs as objects of a type (i.e. the corresponding proposition) has strong intuitive computational meaning.
Martin-Lo¨f’s equality types IdA(a; b) when parameterized, may be considered as a relation. However, can any important relation be constructed from these equality relations? 2.1. Continuum without rational numbers Although the proposed approach concerns W-types in general, for the sake of presentation, let us consider only lists (finite sequences) of elements from some fixed finite collection, say A consisting (as an example) only of a and b. Let a and b be defined as adjacent. Let LA denote the type of lists (finite sequences) over A. List are represented in the dot notation as c1:c2::::ck where ci are elements of A.
The lists may be interpreted as the subintervals of the consecutive partitions of the unit interval [0; 1], i.e. a as [0; 21 ] and b as [ 12 ; 1], a:a as [0; 14 ], a:b as [ 41 ; 42 ], b:a as [ 42 ; 43 ], b:b as [ 34 ; 1], and so on. Then, the adjacency pattern of the lists of length k is determined by the adjacency of the sub-intervals resulting from the k-th division. However, it is a bit misleading because it is based on our intuition. The pattern of this adjacency (without referring to this intuition) is simple, and is defined as follows.
Let a < b. Then, the lexicographical order on the lists can be constructed. The pattern of adjacency (without the reference to intuitions) is defined inductively in the following way. For any list x, x:a and x:b are adjacent. Let x:a and y:b be of the same length and adjacent. If x:a precedes y:b in the lexicographical order, then x:a:b and y:b:a are defined to be adjacent. Otherwise, i.e. if y:b precedes x:a, then y:b:b and x:a:a are defined as adjacent.
The above adjacency pattern is the basis for inductive construction of the adjacency relation for the lists of length k, and then to extend the relation to all lists. That is, list x of length n and list y of length m (where m > n) are defined as adjacent if there is a list z of length m such that x is a prefix of z, and z is adjacent to y. Let this adjacency relation be denoted by Ad jAp, where p denotes specific adjacency pattern from which the relation is constructed. Let the type LA augmented with Ad jAp be denoted by (LA; Ad jAp).
For the simple example above, the infinite lists (denoted by L¥) can be interpreted A as real numbers (modulo equivalence) from the unit interval. That is, prefixes of an infinite sequences, interpreted as intervals, converge to a point (singleton set). Two infinite sequences are equivalent (adjacent) if for any k, their prefixes of length k are adjacent.
Note that if the above pattern is extended with adjacency between border lists, i.e. for any k the lists (a:a::::a) and (b:b::::b), of length k, are adjacent, then LA¥ is (modulo the equivalence) homeomorphic with the circle, i.e. 1-sphere.
The set A may be an arbitrary finite collection of primitive objects (nodes), and the adjacency relation between them may be represented by any connected graph. Also the patterns for constructing the adjacency relation on LA may be more sophisticated like the ones that correspond to n-dimensional cubes, n-spheres, M o¨bius strip, Klein bottle, Sierpinski gasket and carpet, and many interesting fractals. In its generic form, a simple adjacency pattern determines (inductively) the adjacency graph on the lists of length k for any k.
In general case, the adjacency Ad jAp defines natural topology on the quotient set of infinite lists LA¥ by the equivalence relation . Two infinite lists are adjacent if for any k their finite prefixes of length k are adjacent. The relation is defined as the transitive closure of this adjacency between infinite lists. Let this quotient set be denoted by LA¥= . The topology is determined by the definition of converging sequences of infinite lists, i.e. the sequence (cn1 :cn2 ::::cni :::)n:N converges to c1:c2::::ci::: if for any i there is j such that for all k > j the prefixes (finite lists of length i) ck1 :ck2 ::::cki and c1:c2::::ci are adjacent. This definition can be extended to the equivalence classes of . Note that any of such topological spaces is an abstraction of a W-type augmented with an adjacency pattern. Actually, such type is the grounding of the corresponding space. Functions on such augmented types, say from (LA; Ad jAp) into (LB; Ad jBq), are interesting.
A function f : LA ! LB is defined as monotonic if for any lists x and y such that x is prefix of y, then f (x) is a prefix of f (y) or f (x) is equal to f (y). Monotonic function f is strict if for any x there is y such that x is a prefix if y, and f (x) is not f (y). A strict function f : LA ! LB is defined as continuous if for any adjacent lists x and y, the lists f (y) and f (x) are also adjacent.
The extension of a strict function f to function f ¥ from LA¥ into LB¥ is natural. That is, f ¥(c1:c2::::ci:::) is defined as d1:d2::::di::: such that for any i there is k such that d1:d2::::di is a prefix of f (c1:c2::::ck). The strictness of f is essential here.
However, the transformation of f ¥ to function f ¥= from LA¥= into LB¥= is not always possible. For example, if (LA; RAp ) and (LB; RqB) are the same and correspond to the unit interval, then for f ¥= to be total (defined on all elements of its domain), the strict function f must be continuous. This corresponds to the famous Brouwer’s continuity theorem. Infinite lists correspond to the Brouwer’s choice sequences.
The proof is simple. Suppose that the lists u and z (of the same length) are adjacent, and f (u) and f (z) are not adjacent. Then, either u:a and z:b are adjacent, or u:b and z:a are adjacent. That is, either the infinite lists u:a:b:b:b:b: : : : and z:b:a:a:a:a: : : : are equivalent (adjacent), or z:a:b:b:b:b: : : : and u:b:a:a:a:a: : : : are equivalent. Let r1 and r2 be the infinite lists from the above ones that are equivalent, i.e. they represent the same real number. By the assumption that f (u) and f (z) are not adjacent, and by the monotonicity of f , f ¥(r1) and f ¥(r2)) are not equivalent and correspond to different real numbers. Note that if f is continuous, then f ¥= is also continuous in the classical sense.
The functions f ¥ and f ¥= are abstract notions and their grounding (computational contents) is in the function f . Note that in general case for arbitrary adjacency pattern, the adjacency relation Ad jAp has clear computational contents. The co-domain of Ad jAp is constructed on the basis of the primitive propositions (graph edges) of the adjacency pattern p.
In HoTT, equality type IdA(a; b) is interpreted as type of paths between a and b. Adjacency relation also supports the notion of path in more explicit way as a sequence of consecutively adjacent objects. The notion of homotopy equivalence (the same homotopy type) of two topological spaces X and Y (grounded in the W-types with adjacency patterns) has direct computational contents. Note that in the HoTT book, the real numbers were introduced via Cauchy sequences.
Conclusion. Continuum, topologically equivalent (homeomorphic) to the unit interval of real numbers, can be constructed without the rational numbers.
W-types with explicitly introduced adjacency relations by simple adjacency patterns make sense, and may be of some importance for the Foundations of Mathematics.
For more, see Continuum as a primitive type: towards the intuitionistic Analysis on arXiv https://arxiv.org/abs/1510.02787