Re: Zenkin's paper on Cantor (reply of Dr. Zenkin)

From: Josh Purinton (usenet-noreply.a.jp_at_xoxy.net)
Date: 11/18/04 

Date: Thu, 18 Nov 2004 15:33:26 GMT

In article <320e992a.0411180152.30a39fa7@posting.google.com>,
Eray Ozkural exa <examachine@gmail.com> wrote:
>Josh Purinton <usenet-noreply.a.jp@xoxy.net> wrote in message
>news:<izUmd.110236$R05.98736@attbi_s53>...
>> 4. G is well-defined, and, by construction, G differs from each
>> expansion in S by at least one digit. Thus any sequence of binary
>> expansions of the reals in [0,1) is necessarily incomplete.
>
>What does it mean to say that something differs from something else by
>construction when things talked of are supposedly infinite objects?

Here, it means that we can show that G(i) =/= S_i(i) for all i, using only
simple substitution and the definition of G.

If it helps, here's a formalization of the argument that is accepted by
the ACL2 proof checker. ACL2 uses Lisp's prefix notation, so (S i j)
represents S_i(j), (G i) represents G(i), etc.
  
  (defstub S (* *) => *) ; let S be any function of two arguments.

  (defun G (i)
     (if (equal (S i i) 0) 1 0)) ; we define G as above

  (defthm G-differs-from-every-S
    (not (equal (G i) (S i i)))) ; the proof of this theorem is immediate 

-- 
Josh Purinton