Re: A category internal to itself_correction

["Eduardo J. Dubuc" <edubuc@dm.uba.ar>]

Where it says U[1, U'_0] = U_0 it should say U_0[1, U'_0] = U_0


On 04/09/13 06:23, Andrej Bauer wrote:
> Chatting at a conference, the question came up why there is no
> (non-trivial) category which is "internal to itself" (interpret this
> in some sensible sense). And over coffee we thought this must be well
> known, but not to us. Can somene shed some light on the matter?
>
> With kind regards,
>
> Andrej
>

Interesting and difficult question. Related to incompletness problems
and diagonal arguments.

Joyal considered arithmetic universes U (*), and an initial such U_0.
(for example, for U = Sets: U_0[1, N] = standard Natural Numbers).

Then show that within any arithmetic universe U you can construct
internally a U_0. In particular U_0 exist (called U'_0) inside U_0. You
have U[1, U'_0] = U_0. With this he proves Godel Incompletness.

(*) A pretopos U such that admits free monoids:
       X \in U, X ---> M(X), in particular, N = M(0).
(with this you have primitive recursive arithmetics and construct U_0).

I sort of remember also that Penon considered a topos object E' internal
to a topos E and such that E[1, E'] = E.

It is a challenge to to fill all the technical details and make rigorous
sense of all this.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]