* Re: A category internal to itself_correction
[not found] <52279262.4070909@dm.uba.ar>
@ 2013-09-04 20:14 ` Eduardo J. Dubuc
0 siblings, 0 replies; only message in thread
From: Eduardo J. Dubuc @ 2013-09-04 20:14 UTC (permalink / raw)
To: Andrej Bauer; +Cc: Categories list
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/ ]
^ permalink raw reply [flat|nested] only message in thread