Fixing the constructive continued-fraction definition of the reals: proofs and refutations

[Vaughan Pratt <pratt@cs.stanford.edu>]

Prof. Peter Johnstone wrote:
> On Wed, 11 Feb 2009, Vaughan Pratt wrote:
>
>> Prof. Peter Johnstone wrote:
>>>  Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
>>>  looks like, it must (thanks to Lambek) be isomorphic to N x itself,
>>>  and therefore (since equality for N is decidable) must have lots of
>>>  complemented subobjects {0} x itself, {1} x itself, ... The point of
>>>  the continuity theorem for functions R --> R is that there are toposes
>>>  in which R has *no* nontrivial complemented subobjects [...]
>>>  The only way to get round it (apart from using glue)
>>>  is to replace N by some "nonstandard natural number object" having no
>>>  nontrivial complemented subobjects -- but where you get that from, I
>>>  don't know.
>>
>> You're assuming product distributes over sums, which would be true for
>> ordinary product but I specified lexicographic product, with the left
>> argument as the "high order digit" (converse of the usual convention for
>> ordinal product in ordinal arithmetic).
>
> For goodness' sake, Vaughan! How many times do I have to tell you that
> I'm talking about *the underlying object* of the final coalgebra, and
> not its order structure or its topology? If the underlying object of
> the lexicographic product is the ordinary (cartesian) product -- and
> if it's not, then I don't know what it is -- then it distributes over
> sums because that's what products do in a topos.

Peter, if you don't mind my answering a question with a question, did
either of us mention underlying objects before?  (I could have
overlooked an earlier message.)

When you speak out of the blue about "the underlying object of the final
coalgebra," what exactly is underlying what?  I feel like I've abruptly
stepped through a mirror into some strange part of topos theory that
will be covered in Volume 3 of the Elephant.

One notion of underlying object that makes sense for me in the context
so far is the set E(1,X) of elements of an object X in a topos E.  With
this notion I have a prayer of making sense of your claim in the context
of the following four objects of a topos E with NNO N (and whatever else
if anything is needed to ensure that objects 2-4 exist in E).

1.  N^2.

2.  The initial object among all objects X with an element 0: 1 --> X
and maps s,t: X --> X satisfying st = ts.

3.  As for 2 with ts = t in place of st = ts.

4.  As for 3 with st = s in place of ts = t.

If I've grasped this slippery topos concept, all four objects X of E
have, as their underlying set E(1,X), the set of all pairs (m,n) of
natural numbers (up to isomorphism of course).  In 2 the elements take
the form of terms (s^m||t^n)(0) meaning m s's and n t's applied in any
order to 0.  In 3 the elements take the form of maps s^m(t^n(0)) meaning
n applications of t (coarse tuning) followed by m applications of s
(fine tuning), while in 4 they take the form of maps t^m(s^n(0)) (3 with
s and t interchanged).

I could well imagine 1 and 2 turning out to be isomorphic, but I feel I
would get a lot from seeing the proof of whichever way that goes.

I presume that 3 and 4 are isomorphic on the ground that s and t can be
mapped to any two endomorphisms whence there must exist an isomorphism
exchanging s and t.  I imagine I would get less out of a rigorous proof
of that unless there's a bug in the previous sentence.  If there's no
bug then this would seem to constitute a subtle difference from algebra,
where the signature labels the operations in a way that prevents such an
interchange and puts 3 and 4 in distinct albeit equivalent varieties.

Whether or not 1 and 2 are isomorphic, they are in some sense both
representations of the ordinary product of N with itself.

Where I have greater difficulty is imagining an isomorphism between 2
and 3 merely on the ground that they have the same underlying object.
I'm really not following your logic here.  2 implements product
concurrently whereas 3 and 4 implement it sequentially.  How could they
be isomorphic in every topos?  (I can see that they'd have to be
isomorphic in Set, and presumably certain other toposes which however I
have no idea how to characterize.)  I regard 3 and 4 as equivalent
definitions of the ordinal w^2 (w = \omega) in a topos.

What are the necessary subobjects of 3, and which of those are
necessarily complemented?  I can think of the singletons {(m,n)}, the
set of successor elements (since s: X --> X is a monic), and the
*uniform* tails s^m: X --> X of the successor elements, but not the set
of limit ordinals in w^2 since t: X --> X is not a monic, and hence not
anything involving t.  Are there other subobjects of 3, and can you
characterize them all in some neat way?

If as you seem to be implying, 1-4 are isomorphic, then I would have to
agree with your "for goodness' sake" (yes it was really stupid of me not
to see that) and resign myself to the absence (thus far) of any
alternative to apartness for representing the reals.

If however you agree with me that they can't be isomorphic (via
something more reliable than my proof by agitated gesticulation born of
summary dismissal) then we can move on with the rest of my envisaged
program to define the continuum [0,x) in a topos without appealing to
apartness.  This too may or may not have bugs, whence the "proofs and
refutations" qualification in the new subject line.  (If this were darts
there'd be a sequential scoreboard, concurrently with beer.)

Vaughan