User:Hakerh400/Bijection between reals and the powerset of naturals
In this article we explain how to establish a bijection between the set of real numbers and the powerset of natural numbers.
The existence of a bijection
If two sets have the same cardinality, then there exists a bijection between them. The set of natural numbers has cardinality , so its powerset has cardinality . The cardinality of the set of real numbers is also , so there must exist a bijection between them.
What is a real number
Without digging too much into the axiomatization, intuitively a real number consists of a sign, integral part and fractional part. Sign is a boolean value: positive or negative. Integral part is a natural number. Fractional part can be viewed as an infinite sequence of binary digits, or bits. However, if the sequence of bits ends with infinitely many 1s, then it also represents a different real number. For example, (the numbers are represented in base 2). So, not every sequence of bits uniquely represents the fractional part of a real number.
From naturals to reals
In higher-order logic, a set can be represented as a function from the type of the set elements to booleans. For each set there exists a unary predicate such that . A subset of natural numbers can therefore be considered as an infinite sequence of boolean values, or bits. So, we want to establish a bijection between infinite sequences of bits and reals.
Given an infinite sequence of bits . We want to obtain the sign , integral part and fractional part of the corresponding real number. We split the algorithm into two cases based on whether ends with infinitely many same digits (case 2) or not (case 1).
Sequence does not end with infinitely many same digits. Remove the first bit from . If the bit is , then is positive, otherwise is negative. Count the number of 1s at the beginning of . It represents the integral part . Now remove bits from the beginning of (the last bit after 1s must be 0, and 0 exists in the sequence because the sequence is infinite and does not end with infinitely many 1s). The remaining bits in the sequence represent fractional part .
Sequence ends with infinitely many same digits. Locate where the infinite sequence of same digits begins and let it be index . If the ending bits of the sequence are 0s, then is positive, otherwise is negative. Additionally, if is negative, replace all 1s starting from index with 0s. Parse and like in the Case 1.
Correctness of the algorithm
Hakerh400 is working on a formal proof that this algorithm indeed represents a bijection between the powerset of natural numbers and the set of all 3-tuples where is a boolean, is a natural number and is a sequence of bits that does not end with infinitely many 1s. There is also additional constraint that if consists only of 0s and , then cannot be negative.
The algorithm is uncumputable, but it can be used in a formal theorem prover to construct real numbers using codatatypes. The type of real numbers can be represented as
data Real = Real (Nat -> Bool)