Since sentences over any finite alphabet are encodable as bitstrings, without loss of generality we focus on the binary alphabet . denotes the empty string, the set of finite sequences over , the set of infinite sequences over , . stand for strings in . If then is the concatenation of and (e.g., if and then ). Let us order lexicographically: if precedes alphabetically (like in the example above) then we write or ; if may also equal then we write or (e.g., ). The context will make clear where we also identify with a unique nonnegative integer (e.g., string 0100 is represented by integer 10100 in the dyadic system or in the decimal system). Indices range over the positive integers, constants over the positive reals, denote functions mapping integers to integers, the logarithm with basis 2, for real . For , stands for the real number with dyadic expansion (note that for , although ). For , denotes the number of bits in , where for ; . is the prefix of consisting of the first bits, if , and otherwise ( ). For those that contain at least one 0-bit, denotes the lexicographically smallest satisfying ( is undefined for of the form ). We write if there exists such that for all .
For notational simplicity we will use the sign also to indicate summation over uncountably many strings in , rather than using traditional measure notation and signs. The reader should not feel uncomfortable with this notational liberty -- density-like nonzero sums over uncountably many bitstrings, each with individual measure zero, will not play any critical role in the proofs.