FOM: Unlimited comprehension; Topos Theory; Map Theory; NaDSet

[Till Mossakowski]

I must admit that in my message from 13th February,
I expected more from topos theory than what can be expected.
In particular, I expected to have a foundation for the 
"category of all categories", without the need to distinguish 
between "large" and "small" categories. But topos theory does 
not allow unlimited comprehension.
I mixed things up with other f.o.m.s (see below).

Harvey Friedman has answered to me:
>>Zermelo-Fraenkel set theory is one answer to Russell's paradox: it
>>carefully limits comprehension, while keeping classical logic.
>>But there also is another answer: keep unlimited comprehension, but not
>>classical logic.
>
>But unlimited comprehension with the barest of logic is equally
>inconsistent. Later he indicates that he is talking about using lambda
>calculi for f.o.m. But the usual ones do not support standard extensional
>equality with definition by cases, as well as other things needed for
>normal f.o.m. It's too logic free.

Russell's Paradox leads to a formula A with A <=> not A,
i.e. "not" has a fixed point.
This is inconsistent both with classical and intuitionistic logic,
but not with logic as such. Namely, in a three-valued logic,
A <=> not A need not be inconsistent. In map theory*, 
a category of all categories can be defined. Indeed, some definitions
by cases that would lead to inconsistencies cannot be performed,
but still map theory is a f.o.m., since it is a true union
of set theory and untyped lambda calculus, and set theory
can be recovered by considering the well-founded maps.


Steve Simpson writes:
>Aren't the set theorists already way out ahead of the topos theorists
>on this?  I'm thinking of alternative set theories with comprehension
>schemes that go beyond what is available in ZFC.

This is an interesting point. Indeed, there is a paper about 
the definition of the category of all categories in NaDSet**,
an alternative set-theoretic foundation.


Now what about topos theory?

As Harvey Friedman pointed out, unlimited comprehension can 
be consistently interpreted in neither topoi nor intuitionistic logic.
(In the internal language of a topos there only exists the 
separation principle: Given a set/type X, and a formula \phi(x)
in a variable x of type X, you can form {x | \phi(x)} ).

But let me note that
- Russell's Paradox, 
- the proof of Cantor's theorem that a set 
  is not equipotent to its powerset, and 
- the proof of the theorem that the category Set has only set-indexed, 
  but not class-indexed products
all have a very similar structure, using the same form of diagonalization
over the membership predicate.

In my message from 13 February, replace "unlimited comprehension" with 
"arbitrary limits". In the effective topos, arbitrary (internal) limits 
exist, in contrast to the category of Sets, where only set-indexed
limits exist.

Of course, arbitrary limits are not unlimited comprehension.
So probably topos theory is not adequate for solving the
foundational problems of category theory.

Till Mossakowski

*K. Grue, Map theory, Theoretical Computer Science 102, pp. 1-133.
See especially p.24ff.

C. Berline and K. Grue, A kappa-denotational semantics for Map Theory in
ZFC+SI, Theoretical Computer Science 179, pp. 137-202.

**P. C. Gilmore and G. K. Tsiknis, A logic for category theory,
Theoretical Computer Science 111, pp. 211-252.