The Computable Reals (alpha version)

The Computable Reals (alpha version)
------------------------------------
Julio Di Egidio (JDE)
julio at diegidio dot name
(c)2008 JDE, on behalf of sci.math, sci.logic
All right reserved.

=============================================

I will try to give a construction for the "computable reals".

We are going to deal with infinite decimal expansions in binary
coding.

Given:

N* := N u { 0, oo }

w e N* // omega
n e N*

=============================================
=== Preliminaries ===========================
=============================================

Some preliminary inductive definitions:

--- numToBin(n) / returns the binary representation of n /

Ascending:
numToBin(0) := "0"
numToBin(1) := "1"
numToBin(2) := "10"
numToBin(3) := "11"
numToBin(4) := "100"
...
numToBin(n)

Descending:
numToBin(oo) := "1...1".
numToBin(oo-1) := "1...10"
numToBin(oo-2) := "1...101"
numToBin(oo-3) := "1...100"
numToBin(oo-4) := "1...1011"
...
numToBin(oo-n)

---

--- invNumToBin(n) / returns the negated binary representation of n /

Ascending:
invNumToBin(0) := "1"
invNumToBin(1) := "0"
invNumToBin(2) := "01"
invNumToBin(3) := "00"
invNumToBin(4) := "011"
...
invNumToBin(n)

Descending:
invNumToBin(oo) := "0...0".
invNumToBin(oo-1) := "0...01"
invNumToBin(oo-2) := "0...010"
invNumToBin(oo-3) := "0...011"
invNumToBin(oo-4) := "0...0100"
...
invNumToBin(oo-n)

---

--- binSize(n) / returns the minimal length for the binary
representation of n /

Ascending:
binSize(0) := 1
binSize(1) := 1
binSize(2) := 2
binSize(3) := 2
binSize(4) := 3
...
binSize(n) := countDigits(numToBin(n))
...

Descending:
binSize(oo) := countDigits(numToBin(oo)) =
= countDigits("1...1") =
= oo // O(log_2(oo))

binSize(oo-1)= oo
...
binSize(oo-n)= oo


---

/ We have the following informal properties:

invNumToBin(n) = numToBin(~n); // bitwise negation

binSize(numToBin(n)) = binSize(invNumToBin(n));
binSize(numToBin(oo-n)) = binSize(invNumToBin(oo-n)); /

=============================================
=== Sequence p ==============================
=============================================

Let 'p' be the sequence:

p(w, n) := strRev(numToBin(n)).padRight("0",
binSize(w-1)).concat("(0)"), with n < w

/ 'p' is the sequence of the binary representations of the
indexes, written right to left, with a "period" of '(0)'
appended so that binSize(w) digits remain always visible,
where 'w' is given as the number of iterations. /

For instance, for w = 8 we have the (enumerable) list:

0:000(0) = FstE
1:100(0)
2:010(0)
3:110(0)
4:001(0)
5:101(0)
6:011(0)
7:111(0) = LstE

For any w, we define the "first entry" ('FstE') of p to be: p(w, 0).
For any w, we define the "last entry" ('LstE') of p to be: p(w, w-1).

E.g. FstE(p, w=8) = p(8, 0) = "000(0)",
LstE(p, w=8) = p(8, 7) = "111(0)"

We define the "limit entry" ('LimE') of p to be the LstE for w = oo:
p(oo, oo-1).

The LimE of p is the entry p(oo, oo-1):
oo-1:01...1(0)

In fact:

LimE(p) = LstE(p, w=oo) = p(oo, oo-1) =
= strRev(numToBin(oo-1)).padRight("0",
binSize(oo-1)).concat("(0)") =
= strRev("1...10").padRight("0", binSize(oo-1)).concat("(0)") =
= "01...1".padRight("0", binSize(oo-1)).concat("(0)") =
= "01...1".concat("(0)") = // no padding needed
= "01...1(0)"

We define the "omega entry" ('OmeE') associated to p to be: p(oo, oo).

By extension, the OmeE for p is the entry p(oo, oo):
oo:1...1(0)

In fact:

OmeE(p) = p(oo, oo) =
= strRev(numToBin(oo)).padRight("0",
binSize(oo-1)).concat("(0)") =
= strRev("1...1").padRight("0", binSize(oo-1)).concat("(0)") =
= "1...1".padRight("0", binSize(oo-1)).concat("(0)") =
= "1...1".concat("(0)") = // no padding needed
= "1...1(0)"

=============================================
=== Sequence q ==============================
=============================================

Let 'q' be the sequence:

q(w, n) := strRev(invNumToBin(n))).padRight("1",
binSize(w-1).concat("(1)"), with n < w

/ 'q' is symmetrical to 'p', that is q is the same as p with
the digits inverted. /

For instance, for w = 8 we have the list:

0:111(1) = FstE
1:011(1)
2:101(1)
3:001(1)
4:110(1)
5:010(1)
6:100(1)
7:000(1) = LstE

Symmetrically to p,

For any w, the "first entry" ('FstE') of q is: q(w, 0).
For any w, the "last entry" ('LstE') of q is: q(w, w-1).

E.g. FstE(q, w=8) = q(8, 0) = "111(1)",
LstE(q, w=8) = q(8, 7) = "000(1)"

The "limit entry" ('LimE') of q is: q(oo, oo-1).

The LimE of q is the entry q(oo, oo-1):
oo-1:10...0(1)

The "omega entry" ('OmeE') for q is defined as: q(oo, oo).

By extension, the OmeE for q is the entry q(oo, oo):
oo:1...1(0)

=============================================
=== Sequences p and q confronted ============
=============================================

The two sequences confronted, with q in reverse order after p:

/ For the purpose of the diagram, it is w = 7 in this sample. /

======= p =====
0:0...0(0) -- FstE = p(oo, 0)
- - -
0:000(0) --(FstE = p(w, 0))
= = =
1:100(0)
2:010(0)
3:110(0)
4:001(0)
5:101(0)
= = =
6:011(0) -- LstE = p(w, w-1)
- - -
oo-1:01...1(0) -- LimE = p(oo, oo-1)
= = =
7:111(0) --(OmeE = p(w, w)) // finite (false) omega
- - -
oo-0:1...1(0) -- OmeE = p(oo, oo)
======= / =====
0:0...0(1) -- OmeE = q(oo, oo)
- - -
oo-7:000(1) --(OmeE = q(w, w)) // finite (false) omega
= = =
1:10...0(1) -- LimE = q(oo, oo-1)
- - -
oo-6:100(1) -- LstE = q(w, w-1)
= = =
oo-5:010(1)
oo-4:110(1)
oo-3:001(1)
oo-2:101(1)
oo-1:011(1)
= = =
oo-0:111(1) --(FstE = q(w, 0))
- - -
oo-0:1...1(1) -- FstE = q(w, 0
======= q =====

With the boundaries only, and an overload of notation:

======= p =====
FstE_p = p(oo, 0) = "0...0(0)" = "(0)(0)"
LimE_p = p(oo, oo-1) = "01...1(0)" = "0(1)(0)"
OmeE_p = p(oo, oo) = "1...1(0)" = "(1)(0)"
======= / =====
OmeE_q = q(oo, oo) = "0...0(1)" = "(0)(1)"
LimE_q = q(oo, oo-1) = "10...0(1)" = "1(0)(1)"
FstE_q = q(oo, 0) = "1...1(1)" = "(1)(1)"
======= q =====

=============================================
=== Sequences p and q "matched" =============
=============================================

(DEF) Informally, p and q "match" in that, for any w,
p and q-in-reverse-order not only are equinumerous,
they are actually the exact same list up to
certain transformations we are going to apply. /

Given the diagram on the boundary cases just above:

On a side, we now note that the "period" is indeed not a real period.
It is a string we have appended to the printed entry in order to later
reason about decimal expansions and a specific interval of the
(computable) real numbers. Its length is finite and it is in fact
equal to 3, as the two possible "periods" are (0) and (1). On the
other side, what is now a "pre-period" is always a string of infinite
length (we are talking about the boundary cases).

If now we *do* start reasoning about a list of the decimal expansions
of the computable reals in the interval [0.(0), 0.(1)], we can try a
next step. We will drop the "period" from our representation, as less
significant than our "infinite anti-period". The justification I can
give for this choise is not formal (contributions are welcome), it is
rather in the result.

// [result - finite case]

The result for the finite case (I assume induction is enough to prove
this step) is that p and q-in-reverse-order do "match", where for
there being a match we mean:

======= p =====
p(w, 0) = q(w, w-1)
....
p(w, w-1) = q(w, 0)
======= q =====

This is a diagram of the two finite lists for w = 8, with the
"periods" dropped:

======= p =====
0:000 = FstE
1:100
2:010
3:110
4:001
5:101
6:011
7:111 = LstE
======= / =====
7:000 = LstE
6:100
5:010
4:110
3:001
2:101
1:011
0:111 = FstE
======= q =====

// [result - extended case]

For the result in the extended case, we need a preliminary step.

This is the boundary diagram, with the "periods" dropped:

======= p =====
FstE_p = p(oo, 0) = "(0)(0)" = "(0)"
LimE_p = p(oo, oo-1) = "0(1)(0)" = "0(1)"
OmeE_p = p(oo, oo) = "(1)(0)" = "(1)"
======= / =====
OmeE_q = q(oo, oo) = "(0)(1)" = "(0)"
LimE_q = q(oo, oo-1) = "1(0)(1)" = "1(0)"
FstW_q = q(oo, 0) = "(1)(1)" = "(1)"
======= q =====

It is now again with reference to our intended interpretation that we
will state the "usual" equality between LimE_p and LimE_q:

LimE_p = LimE_q

We can then get the result for the extended case, that p and q-in-
reverse-order keep "matching", where for there being a match we mean:

======= p =====
p(oo, 0) = q(oo, oo)
p(oo, oo-1) = q(oo, oo-1)
p(oo, oo) = q(oo, 0)
======= q =====

This is the boundary diagram, with the introduced equality:

======= p =====
FstE_p = OmeE_q = "(0)"
LimE_p = LimE_q = "0(1)" = "1(0)"
OmeE_p = FstW_q = "(1)"
======= q =====

// [final result]

The overal "matching":

======= p =====
p(w, 0) = q(w, w-1)
....
p(w, w-1) = q(w, 0)
======= q =====

======= p =====
p(oo, 0) = q(oo, oo)
p(oo, oo-1) = q(oo, oo-1)
p(oo, oo) = q(oo, 0)
======= q =====

=============================================
=== Conclusions =============================
=============================================

/ Very tentative, just some ideas. /

We have two sequences, p and q-in-reverse-order, that "match" (in the
sense given above) over the whole domain N*, namely for any w in N*.

By interpreting the entries in the list as binary decimal expansions,
we have also (indirectly, it is actually the interval [0.(0),0.(1)])
established the domain (overriding the symbol) R* of the "computable
reals".

R* is defined in terms of p and q. Our very construction provides a
bijection between R* and N*. R* is a "subcountable" w.r.t. N*,
although R* has got "the power of cross-induction".

The "matching" in the [final result] just above is possibly better
appreciated by now looking back at the first diagram given on top, the
confrontation of p and q:

======= p =====
0:0...0(0) -- FstE = p(oo, 0)
- - -
0:000(0) --(FstE = p(w, 0))
= = =
1:100(0)
2:010(0)
3:110(0)
4:001(0)
5:101(0)
= = =
6:011(0) -- LstE = p(w, w-1)
- - -
oo-1:01...1(0) -- LimE = p(oo, oo-1)
= = =
7:111(0) --(OmeE = p(w, w)) // finite (false) omega
- - -
oo-0:1...1(0) -- OmeE = p(oo, oo)
======= / =====
0:0...0(1) -- OmeE = q(oo, oo)
- - -
oo-7:000(1) --(OmeE = q(w, w)) // finite (false) omega
= = =
1:10...0(1) -- LimE = q(oo, oo-1)
- - -
oo-6:100(1) -- LstE = q(w, w-1)
= = =
oo-5:010(1)
oo-4:110(1)
oo-3:001(1)
oo-2:101(1)
oo-1:011(1)
= = =
oo-0:111(1) --(FstE = q(w, 0))
- - -
oo-0:1...1(1) -- FstE = q(w, 0
======= q =====

=============================================
=== Final remarks ======================
=============================================

I have tried to give a construction for the "computable reals".

This "double construction" should provide uniqueness and completeness.

Among the various results, it seems no diagonal argument can in fact
work against this list.

Another significant results is the subcountability of R*, although R*
has got what I have improperly called: "the power of cross-induction".

There are many more properties I can glimpsy but not qualify, as well
as surely some gaps. I hope in your feedback to keep improving the
overall construction.

Finally, there might be some trivial mistakes, even typos and "bugs"
but I am too tired and too "in it" to find any more bugs. Maybe keep
in mind I have strived for consistency.

Thanks for your attention and enjoy! I'll go enjoy some pasta
now...

-LV

On 12 Aug, 10:29, ju...@diegidio.name wrote:

> If now we *do* start reasoning about a list of the decimal expansions
> of the computable reals in the interval [0.(0), 0.(1)], we can try a
> next step. We will drop the "period" from our representation, as less
> significant than our "infinite anti-period". The justification I can

Should read "pre-period".

-LV

On 12 Aug, 10:29, ju...@diegidio.name wrote:

> * */ 'p' is the sequence of the binary representations of the
> * * *indexes, written right to left, with a "period" of '(0)'
> * * *appended so that binSize(w) digits remain always visible,
> * * *where 'w' is given as the number of iterations. /

Should read binSize(w-1).

-LV

On 12 Aug, 10:29, ju...@diegidio.name wrote:

> By extension, the OmeE for q is the entry q(oo, oo):
> * oo:1...1(0)

Should read oo:0...0(1).

-LV

On Tue, 12 Aug 2008 02:29:01 -0700 (PDT), julio@diegidio.name wrote:

>The Computable Reals (alpha version)
>------------------------------------
>Julio Di Egidio (JDE)
>julio at diegidio dot name
>(c)2008 JDE, on behalf of sci.math, sci.logic
>All right reserved.
>
>[long construction snipped]
>
>
>
>=============================================
>=== Final remarks ======================
>=============================================
>
>I have tried to give a construction for the "computable reals".

But you didn't. There's nothing above that explains how you
know that _every_ computable real appears somewhere on
your list.

>This "double construction" should provide uniqueness and completeness.
>
>Among the various results, it seems no diagonal argument can in fact
>work against this list.
>
>Another significant results is the subcountability of R*, although R*
>has got what I have improperly called: "the power of cross-induction".
>
>There are many more properties I can glimpsy but not qualify, as well
>as surely some gaps. I hope in your feedback to keep improving the
>overall construction.
>
>Finally, there might be some trivial mistakes, even typos and "bugs"
>but I am too tired and too "in it" to find any more bugs. Maybe keep
>in mind I have strived for consistency.
>
>Thanks for your attention and enjoy! I'll go enjoy some pasta
>now...
>
>-LV

David C. Ullrich

"Understanding Godel isn't about following his formal proof.
That would make a mockery of everything Godel was up to."
(John Jones, "My talk about Godel to the post-grads."
in sci.logic.)

On 12 Aug, 11:58, David C. Ullrich <dullr...@sprynet.com> wrote:
> On Tue, 12 Aug 2008 02:29:01 -0700 (PDT), ju...@diegidio.name wrote:
> >The Computable Reals (alpha version)
> >------------------------------------
> >Julio Di Egidio (JDE)
> >julio at diegidio dot name
> >(c)2008 JDE, on behalf of sci.math, sci.logic
> >All right reserved.
>
> >[long construction snipped]
>
> >=============================================
> >=== Final remarks ======================
> >=============================================
>
> >I have tried to give a construction for the "computable reals".
>
> But you didn't. There's nothing above that explains how you
> know that _every_ computable real appears somewhere on
> your list.

That is very right, I have not stated it explicitly. Given the
subtlety of the argument, please let me by converse remark that you
are not really asking about the construction, but rather about its
interpretation as the decimal expansions etc. etc.

As to why I believe (think) that the list is "complete": because it is
the _complete_ (over N*) list of _all_ the possible infinite (over N*)
binary expansions. What then we can, quite "sensibly", name R* -- the
computable reals, is a step away along the path of my construction as
a matter of definitions (in the sense of defining things of the
article).

Indeed, what I have given IS _per definition_ the list of the
"computable reals" (modulo the usual adjustments).

Hope this clarifies.

Of course one could prove that the list is not in fact complete; but
I, for one, can't see what more could be missing.

-LV

julio@diegidio.name wrote:
>
> The Computable Reals (alpha version)
> ------------------------------------
> Julio Di Egidio (JDE)
> julio at diegidio dot name
> (c)2008 JDE, on behalf of sci.math, sci.logic
> All right reserved.
>
> =============================================
>
> I will try to give a construction for the "computable reals".
>
> We are going to deal with infinite decimal expansions in binary
> coding.
>
> Given:
>
> N* := N u { 0, oo }
>
> w e N* // omega

So is omega the same as oo? And is it what other people mean by omega?

Below you use such expressions as log_2(oo) and oo - n. How are these
defined?

> n e N*
>
> =============================================
> === Preliminaries ===========================
> =============================================
>
> Some preliminary inductive definitions:
>
> --- numToBin(n) / returns the binary representation of n /
>
> Ascending:
> numToBin(0) := "0"
> numToBin(1) := "1"
> numToBin(2) := "10"
> numToBin(3) := "11"
> numToBin(4) := "100"
> ...
> numToBin(n)
>
> Descending:
> numToBin(oo) := "1...1".
> numToBin(oo-1) := "1...10"
> numToBin(oo-2) := "1...101"
> numToBin(oo-3) := "1...100"
> numToBin(oo-4) := "1...1011"
> ...
> numToBin(oo-n)
>
> ---
>
> --- invNumToBin(n) / returns the negated binary representation of n /
>
> Ascending:
> invNumToBin(0) := "1"
> invNumToBin(1) := "0"
> invNumToBin(2) := "01"
> invNumToBin(3) := "00"
> invNumToBin(4) := "011"
> ...
> invNumToBin(n)
>
> Descending:
> invNumToBin(oo) := "0...0".
> invNumToBin(oo-1) := "0...01"
> invNumToBin(oo-2) := "0...010"
> invNumToBin(oo-3) := "0...011"
> invNumToBin(oo-4) := "0...0100"
> ...
> invNumToBin(oo-n)
>
> ---
>
> --- binSize(n) / returns the minimal length for the binary
> representation of n /
>
> Ascending:
> binSize(0) := 1
> binSize(1) := 1
> binSize(2) := 2
> binSize(3) := 2
> binSize(4) := 3
> ...
> binSize(n) := countDigits(numToBin(n))
> ...
>
> Descending:
> binSize(oo) := countDigits(numToBin(oo)) =
> = countDigits("1...1") =
> = oo // O(log_2(oo))
>
> binSize(oo-1)= oo
> ...
> binSize(oo-n)= oo
>
> ---
>
> / We have the following informal properties:
>
> invNumToBin(n) = numToBin(~n); // bitwise negation
>
> binSize(numToBin(n)) = binSize(invNumToBin(n));
> binSize(numToBin(oo-n)) = binSize(invNumToBin(oo-n)); /
>
> =============================================
> === Sequence p ==============================
> =============================================
>
> Let 'p' be the sequence:
>
> p(w, n) := strRev(numToBin(n)).padRight("0",
> binSize(w-1)).concat("(0)"), with n < w
>
> / 'p' is the sequence of the binary representations of the
> indexes, written right to left, with a "period" of '(0)'
> appended so that binSize(w) digits remain always visible,
> where 'w' is given as the number of iterations. /
>
> For instance, for w = 8 we have the (enumerable) list:
>
> 0:000(0) = FstE
> 1:100(0)
> 2:010(0)
> 3:110(0)
> 4:001(0)
> 5:101(0)
> 6:011(0)
> 7:111(0) = LstE
>
> For any w, we define the "first entry" ('FstE') of p to be: p(w, 0).
> For any w, we define the "last entry" ('LstE') of p to be: p(w, w-1).
>
> E.g. FstE(p, w=8) = p(8, 0) = "000(0)",
> LstE(p, w=8) = p(8, 7) = "111(0)"
>
> We define the "limit entry" ('LimE') of p to be the LstE for w = oo:
> p(oo, oo-1).
>
> The LimE of p is the entry p(oo, oo-1):
> oo-1:01...1(0)
>
> In fact:
>
> LimE(p) = LstE(p, w=oo) = p(oo, oo-1) =
> = strRev(numToBin(oo-1)).padRight("0",
> binSize(oo-1)).concat("(0)") =
> = strRev("1...10").padRight("0", binSize(oo-1)).concat("(0)") =
> = "01...1".padRight("0", binSize(oo-1)).concat("(0)") =
> = "01...1".concat("(0)") = // no padding needed
> = "01...1(0)"
>
> We define the "omega entry" ('OmeE') associated to p to be: p(oo, oo).
>
> By extension, the OmeE for p is the entry p(oo, oo):
> oo:1...1(0)
>
> In fact:
>
> OmeE(p) = p(oo, oo) =
> = strRev(numToBin(oo)).padRight("0",
> binSize(oo-1)).concat("(0)") =
> = strRev("1...1").padRight("0", binSize(oo-1)).concat("(0)") =
> = "1...1".padRight("0", binSize(oo-1)).concat("(0)") =
> = "1...1".concat("(0)") = // no padding needed
> = "1...1(0)"
>
> =============================================
> === Sequence q ==============================
> =============================================
>
> Let 'q' be the sequence:
>
> q(w, n) := strRev(invNumToBin(n))).padRight("1",
> binSize(w-1).concat("(1)"), with n < w
>
> / 'q' is symmetrical to 'p', that is q is the same as p with
> the digits inverted. /
>
> For instance, for w = 8 we have the list:
>
> 0:111(1) = FstE
> 1:011(1)
> 2:101(1)
> 3:001(1)
> 4:110(1)
> 5:010(1)
> 6:100(1)
> 7:000(1) = LstE
>
> Symmetrically to p,
>
> For any w, the "first entry" ('FstE') of q is: q(w, 0).
> For any w, the "last entry" ('LstE') of q is: q(w, w-1).
>
> E.g. FstE(q, w=8) = q(8, 0) = "111(1)",
> LstE(q, w=8) = q(8, 7) = "000(1)"
>
> The "limit entry" ('LimE') of q is: q(oo, oo-1).
>
> The LimE of q is the entry q(oo, oo-1):
> oo-1:10...0(1)
>
> The "omega entry" ('OmeE') for q is defined as: q(oo, oo).
>
> By extension, the OmeE for q is the entry q(oo, oo):
> oo:1...1(0)
>
> =============================================
> === Sequences p and q confronted ============
> =============================================
>
> The two sequences confronted, with q in reverse order after p:
>
> / For the purpose of the diagram, it is w = 7 in this sample. /
>
> ======= p =====
> 0:0...0(0) -- FstE = p(oo, 0)
> - - -
> 0:000(0) --(FstE = p(w, 0))
> = = =
> 1:100(0)
> 2:010(0)
> 3:110(0)
> 4:001(0)
> 5:101(0)
> = = =
> 6:011(0) -- LstE = p(w, w-1)
> - - -
> oo-1:01...1(0) -- LimE = p(oo, oo-1)
> = = =
> 7:111(0) --(OmeE = p(w, w)) // finite (false) omega
> - - -
> oo-0:1...1(0) -- OmeE = p(oo, oo)
> ======= / =====
> 0:0...0(1) -- OmeE = q(oo, oo)
> - - -
> oo-7:000(1) --(OmeE = q(w, w)) // finite (false) omega
> = = =
> 1:10...0(1) -- LimE = q(oo, oo-1)
> - - -
> oo-6:100(1) -- LstE = q(w, w-1)
> = = =
> oo-5:010(1)
> oo-4:110(1)
> oo-3:001(1)
> oo-2:101(1)
> oo-1:011(1)
> = = =
> oo-0:111(1) --(FstE = q(w, 0))
> - - -
> oo-0:1...1(1) -- FstE = q(w, 0
> ======= q =====
>
> With the boundaries only, and an overload of notation:
>
> ======= p =====
> FstE_p = p(oo, 0) = "0...0(0)" = "(0)(0)"
> LimE_p = p(oo, oo-1) = "01...1(0)" = "0(1)(0)"
> OmeE_p = p(oo, oo) = "1...1(0)" = "(1)(0)"
> ======= / =====
> OmeE_q = q(oo, oo) = "0...0(1)" = "(0)(1)"
> LimE_q = q(oo, oo-1) = "10...0(1)" = "1(0)(1)"
> FstE_q = q(oo, 0) = "1...1(1)" = "(1)(1)"
> ======= q =====
>
> =============================================
> === Sequences p and q "matched" =============
> =============================================
>
> (DEF) Informally, p and q "match" in that, for any w,
> p and q-in-reverse-order not only are equinumerous,
> they are actually the exact same list up to
> certain transformations we are going to apply. /
>
> Given the diagram on the boundary cases just above:
>
> On a side, we now note that the "period" is indeed not a real period.
> It is a string we have appended to the printed entry in order to later
> reason about decimal expansions and a specific interval of the
> (computable) real numbers. Its length is finite and it is in fact
> equal to 3, as the two possible "periods" are (0) and (1). On the
> other side, what is now a "pre-period" is always a string of infinite
> length (we are talking about the boundary cases).
>
> If now we *do* start reasoning about a list of the decimal expansions
> of the computable reals in the interval [0.(0), 0.(1)], we can try a
> next step. We will drop the "period" from our representation, as less
> significant than our "infinite anti-period". The justification I can
> give for this choise is not formal (contributions are welcome), it is
> rather in the result.
>
> // [result - finite case]
>
> The result for the finite case (I assume induction is enough to prove
> this step) is that p and q-in-reverse-order do "match", where for
> there being a match we mean:
>
> ======= p =====
> p(w, 0) = q(w, w-1)
> ...
> p(w, w-1) = q(w, 0)
> ======= q =====
>
> This is a diagram of the two finite lists for w = 8, with the
> "periods" dropped:
>
> ======= p =====
> 0:000 = FstE
> 1:100
> 2:010
> 3:110
> 4:001
> 5:101
> 6:011
> 7:111 = LstE
> ======= / =====
> 7:000 = LstE
> 6:100
> 5:010
> 4:110
> 3:001
> 2:101
> 1:011
> 0:111 = FstE
> ======= q =====
>
> // [result - extended case]
>
> For the result in the extended case, we need a preliminary step.
>
> This is the boundary diagram, with the "periods" dropped:
>
> ======= p =====
> FstE_p = p(oo, 0) = "(0)(0)" = "(0)"
> LimE_p = p(oo, oo-1) = "0(1)(0)" = "0(1)"
> OmeE_p = p(oo, oo) = "(1)(0)" = "(1)"
> ======= / =====
> OmeE_q = q(oo, oo) = "(0)(1)" = "(0)"
> LimE_q = q(oo, oo-1) = "1(0)(1)" = "1(0)"
> FstW_q = q(oo, 0) = "(1)(1)" = "(1)"
> ======= q =====
>
> It is now again with reference to our intended interpretation that we
> will state the "usual" equality between LimE_p and LimE_q:
>
> LimE_p = LimE_q
>
> We can then get the result for the extended case, that p and q-in-
> reverse-order keep "matching", where for there being a match we mean:
>
> ======= p =====
> p(oo, 0) = q(oo, oo)
> p(oo, oo-1) = q(oo, oo-1)
> p(oo, oo) = q(oo, 0)
> ======= q =====
>
> This is the boundary diagram, with the introduced equality:
>
> ======= p =====
> FstE_p = OmeE_q = "(0)"
> LimE_p = LimE_q = "0(1)" = "1(0)"
> OmeE_p = FstW_q = "(1)"
> ======= q =====
>
> // [final result]
>
> The overal "matching":
>
> ======= p =====
> p(w, 0) = q(w, w-1)
> ...
> p(w, w-1) = q(w, 0)
> ======= q =====
>
> ======= p =====
> p(oo, 0) = q(oo, oo)
> p(oo, oo-1) = q(oo, oo-1)
> p(oo, oo) = q(oo, 0)
> ======= q =====
>
> =============================================
> === Conclusions =============================
> =============================================
>
> / Very tentative, just some ideas. /
>
> We have two sequences, p and q-in-reverse-order, that "match" (in the
> sense given above) over the whole domain N*, namely for any w in N*.
>
> By interpreting the entries in the list as binary decimal expansions,
> we have also (indirectly, it is actually the interval [0.(0),0.(1)])
> established the domain (overriding the symbol) R* of the "computable
> reals".
>
> R* is defined in terms of p and q. Our very construction provides a
> bijection between R* and N*. R* is a "subcountable" w.r.t. N*,
> although R* has got "the power of cross-induction".
>
> The "matching" in the [final result] just above is possibly better
> appreciated by now looking back at the first diagram given on top, the
> confrontation of p and q:
>
> ======= p =====
> 0:0...0(0) -- FstE = p(oo, 0)
> - - -
> 0:000(0) --(FstE = p(w, 0))
> = = =
> 1:100(0)
> 2:010(0)
> 3:110(0)
> 4:001(0)
> 5:101(0)
> = = =
> 6:011(0) -- LstE = p(w, w-1)
> - - -
> oo-1:01...1(0) -- LimE = p(oo, oo-1)
> = = =
> 7:111(0) --(OmeE = p(w, w)) // finite (false) omega
> - - -
> oo-0:1...1(0) -- OmeE = p(oo, oo)
> ======= / =====
> 0:0...0(1) -- OmeE = q(oo, oo)
> - - -
> oo-7:000(1) --(OmeE = q(w, w)) // finite (false) omega
> = = =
> 1:10...0(1) -- LimE = q(oo, oo-1)
> - - -
> oo-6:100(1) -- LstE = q(w, w-1)
> = = =
> oo-5:010(1)
> oo-4:110(1)
> oo-3:001(1)
> oo-2:101(1)
> oo-1:011(1)
> = = =
> oo-0:111(1) --(FstE = q(w, 0))
> - - -
> oo-0:1...1(1) -- FstE = q(w, 0
> ======= q =====
>
> =============================================
> === Final remarks ======================
> =============================================
>
> I have tried to give a construction for the "computable reals".
>
> This "double construction" should provide uniqueness and completeness.
>
> Among the various results, it seems no diagonal argument can in fact
> work against this list.
>
> Another significant results is the subcountability of R*, although R*
> has got what I have improperly called: "the power of cross-induction".
>
> There are many more properties I can glimpsy but not qualify, as well
> as surely some gaps. I hope in your feedback to keep improving the
> overall construction.
>
> Finally, there might be some trivial mistakes, even typos and "bugs"
> but I am too tired and too "in it" to find any more bugs. Maybe keep
> in mind I have strived for consistency.
>
> Thanks for your attention and enjoy! I'll go enjoy some pasta
> now...
>
> -LV


--
He is not here; but far away
The noise of life begins again
And ghastly thro' the drizzling rain
On the bald street breaks the blank day.

In article
<8e76b453-0a39-4dce-bc15-765e0b5b9edf@j22g2000hsf.googlegroups.com>,
julio@diegidio.name wrote:

> On 12 Aug, 11:58, David C. Ullrich <dullr...@sprynet.com> wrote:
> > On Tue, 12 Aug 2008 02:29:01 -0700 (PDT), ju...@diegidio.name wrote:
> > >The Computable Reals (alpha version)
> > >------------------------------------
> > >Julio Di Egidio (JDE)
> > >julio at diegidio dot name
> > >(c)2008 JDE, on behalf of sci.math, sci.logic
> > >All right reserved.
> >
> > >[long construction snipped]
> >
> > >=============================================
> > >=== Final remarks ======================
> > >=============================================
> >
> > >I have tried to give a construction for the "computable reals".
> >
> > But you didn't. There's nothing above that explains how you
> > know that _every_ computable real appears somewhere on
> > your list.
>
> That is very right, I have not stated it explicitly. Given the
> subtlety of the argument, please let me by converse remark that you
> are not really asking about the construction, but rather about its
> interpretation as the decimal expansions etc. etc.
>
> As to why I believe (think) that the list is "complete": because it is
> the _complete_ (over N*) list of _all_ the possible infinite (over N*)
> binary expansions.

No, that's not possible.

> What then we can, quite "sensibly", name R* -- the
> computable reals, is a step away along the path of my construction as
> a matter of definitions (in the sense of defining things of the
> article).
>
> Indeed, what I have given IS _per definition_ the list of the
> "computable reals" (modulo the usual adjustments).

No, you haven't. There _is_ a standard definition of "computable
real", and it simply doesn't appear anywhere in your post.

> Hope this clarifies.
>
> Of course one could prove that the list is not in fact complete; but
> I, for one, can't see what more could be missing.
>
> -LV

--
David C. Ullrich

On 12 Aug, 18:43, "David C. Ullrich" <dullr...@sprynet.com> wrote:

> > As to why I believe (think) that the list is "complete": because it is
> > the _complete_ (over N*) list of _all_ the possible infinite (over N*)
> > binary expansions.
>
> No, that's not possible.

In this context, funny statement to say the least.

> > Indeed, what I have given IS _per definition_ *the list of the
> > "computable reals" (modulo the usual adjustments).
>
> No, you haven't. There _is_ a standard definition of "computable
> real", and it simply doesn't appear anywhere in your post.

Another funny statement, even more funny considering that the standard
definition happens to correspond to mine were it not for your pre-
judgement.

I wander what you really don't know. For instance, it is far from a
pleasure, apart from how improductive, to keep on these tones. You
maybe don't take me for serious on this.

-LV

On 12 Aug, 13:36, Frederick Williams <frederick.willia...@tesco.net>
wrote:
> ju...@diegidio.name wrote:

> > Given:
>
> > * N* := N u { 0, oo }
>
> > * w e N* // omega

> So is omega the same as oo?

No, omega -- in the metalanguage or otherwise informally -- denotes
'w', which is "an upper bound for the construction".

> And is it what other people mean by omega?

Funny question... I guess some do, at least in some contexts, I for
one, above all when induction and transfinite induction are involved.
I don't claim it is the best choise ever. It is still an irrelevant
objections here, at least from the formal point, which, OTOH, seemed
to be the only thing able to give dignity to any argument. For my
choices, with "omega" as with anything alse, I do always have my
reasons, within an always limited knowledge.

> Below you use such expressions as log_2(oo) and oo - n.
> How are these defined?

It was O(log_2(oo)) and it was a side comment. The result of that
counting of digits, by the (inductive) definitions given, simply IS oo
for the whole descending enumeration. (That note on the order of the
infinity was a bookmark for later consideration which I forgot to
remove before publishing: it is irrelevant to the construction given
above.)

'oo-n' is the (n-10)-th index for the descending enumeration. To make
a long story short, I think the correct answer is: it belongs to the
primitives.

-LV