Online resource for type theory?

1. Dec 25, 2004

phoenixthoth

Does anyone know a good online resource for type theory? I've heard that in it, there is a "universal object" which "contains" all other "objects." Is this right? Where can I get the good stuff? I know I can google for it; I'm not a moron. I just want your recommendations instead of a list of random pages containing the text "mathematics" "russell" and "type". Thanks a bunch.

2. Dec 26, 2004

matt grime

But there's a universal "onject" that contains all the sets in ordinary set theory, it just isn't a set.

3. Dec 26, 2004

phoenixthoth

You're right: if I can avoid type theory then I would prefer to.

That's the problem with ZFC set theory, in my opinion, where by "problem" I mean something of my own perception of its aesthetic appeal. Not a problem of mathematical correctness/consistency.

I'm looking for a theory that interfaces with set theory somehow (whatever that means) in which the "universal object" is of the same type as all other "objects."

edit: Quinne's (sp?) "New Foundations" does this but at the cost of the axiom of choice. And I haven't seen an online version of it more than a description of it plus links to (paper) books.

I will check wiki and the philosophy enc. at stanford...

edit: I think type theory does not have this feature.

Last edited: Dec 26, 2004
4. Dec 26, 2004

Hurkyl

Staff Emeritus
Have you looked into Topos theory any? I don't know if exists a Topos that has a "largest" object or not, though.

There's a fun trick you can do with ordinary ZFC -- given suitable assumptions, you can divide all sets into "small" sets, and "large" sets.

The small sets that are (recursively) made up only of small sets, by themselves, satisfy the axioms of ZFC. But, there is a (large) set of all sets.

Of course, though, there isn't a set of all large sets.

5. Dec 26, 2004

phoenixthoth

Did you mean a large set of all *small* sets? Sounds like ultrafilters may be involved...

That's nifty!

There is a heirarchy of "objects", starting with sets and then classes and then something I don't know the name for; an example of the third type is the "object" of all classes, {c : c=c}. It never stops! (Or does it?)

(I did manage to get my ternary universal set theory paper reviewed by an expert who said I can't just invent new axioms; I have to either prove their consistency or find a model of them. So I've been playing around with models a slight bit.)

Oh and the answer to your question is no but I will check wiki...

Edit: I have a question which would be obvious to me if I understood the definition of topos. Is the category of all categories a topos? I know it is a category...

Last edited: Dec 26, 2004
6. Dec 26, 2004

matt grime

but it isn't a small category

7. Dec 26, 2004

phoenixthoth

oh, right...

Then I guess topos theory is not what I'm looking for. I want the "mother of all topoi" to be a topos. I think I am probably horribly misunderstanding topoi! oi vey

Last edited: Dec 26, 2004
8. Dec 26, 2004

Hurkyl

Staff Emeritus
Each individual topos acts like an entire set theoretic universe, that's why I suggested it. There might be some topos that has a "biggest set" in it, and then this topos could serve as the "set theory" in which you are interested.

If you wanna look into this approach, I found "Sheaves in Geometry and Logic" (Saunders Mac Lane) to be helpful (though I can't say I fully understand it). Of the intro to category theory books I've read, "Categories, Types, and Structures" (Andrea Asperti and Giuseppe Longo) cut through a lot of the confusion I had. I've seen Saunders Mac Lane's intro book recommended a lot too.

9. Dec 26, 2004

phoenixthoth

I did a search and read
http://en.wikipedia.org/wiki/Topos_theory
a bit more carefully this time. There are online referneces! One is by Robery Goldblatt who wrote a book part of which I read on nonstandard analysis. I enjoy his style so I'll try that one.

The idea expressed in that first paragraph is very zesty! I will look into it. Hoever I think reading some of these books will be very much not zesty. :yuck: :tongue2:

10. Dec 26, 2004

Hurkyl

Staff Emeritus
If I go into work tomorrow, I'll ask a few people (who might be in) about it -- I don't want to get you all interested just to find out it's impossible! OTOH, it still might give you ideas -- it certainly did for me.

11. Dec 27, 2004

phoenixthoth

So... did you go into work today?

12. Dec 27, 2004

Hurkyl

Staff Emeritus
I was late, I forgot, and I'm pretty sure the people I would've asked weren't in.

13. Dec 28, 2004

phoenixthoth

Categories can have universal elements (or is it objects in the category???) but this is not what I mean by universal. In other words, I've read a definition of universal and it doesn't fit what I am looking for. I don't know how to "define" universal in categories but for sets this would be a set containg all other sets.

Let me try:
Let C be a category.
U is a universal object in the category iff
1. for all objects A in C, there is an injective arrow f:A-->U (does this make sense, ie, am I stating it right?).
2. suppose U has the property 1 and A is an object for which there is an arrow f:U-->A that is injective. Then A is isomorphic to U.

For sport, I will think about trying to prove Set has no universal element.

Maybe this definition is too weak and Set has a universal element. I want this definiton to fail for Set but I do want there to be categories for which this is true. I'm interested in those categories for sure, especially the small ones, if any.

Now you see how much category theory I know which is none! :)

14. Dec 28, 2004

Hurkyl

Staff Emeritus
That sounds like my initial thought -- a set U is "biggest" if every other set has a monic to U. Or, (equivalently?) there is an epic from U to any other set.

This one, though, sounds more accurate to me:

For any A,
there is an f : A --> U such that
for any g : A --> B
there is an h : U --> B such that g = h o f.

That is, each function from A factors through a canonical map from A to U.

(Or, you might prefer to pick g first, then f and h)

These might all be equivalent, though!

15. Dec 28, 2004

phoenixthoth

The simpest seems to be just that there is an epic from U to any other object in the category. Now are there any categories with this kind of universal element that are not too small nor too big? I don't know many examples of categories.

EDIT: Can you prove that if there is a set U satisfying your "factoring" definition then that set is universal (and thus Set does not have such an element)?

Last edited: Dec 28, 2004
16. Dec 28, 2004

matt grime

You can quite trivially cook up hundreds of such examples as you#'re after, such as the category of countably generated (abelian if you must though I think it holds in greater generality) groups.

17. Dec 28, 2004

Hurkyl

Staff Emeritus
Pick your favorite cardinality K, and form the category of all sets with cardinality K or less. Any set with cardinality K would serve as a biggest set. The problem, here, is that such a set wouldn't have a power object.

You could further recursively require that all elements of the sets also have cardinality K or less, and I think that would also be a small category.

18. Dec 28, 2004

matt grime

And one can also easily show that SET can have no universal element: cardinal numbers are isomorphism classes, and any universal set would by definition have to have a surjection onto all (representatives of) these isomorphism classes and thus couldn't be a set.

19. Dec 28, 2004

phoenixthoth

What's the universal element in that category where by universal I mean it has the two properties above?

I love it when people who can easily do somethign I can't call it trivial. I love it even more when it is quite trivial.

20. Dec 28, 2004

matt grime

Let F_w be the free product of Z with itself a countable number of times, then there is an epimorphism onto any countalby presented group. Do you need me to write out the maps? Send as many generators to generators as you need modulo the relations and send any remaining generators to the identity.

If we replace the set with a skeletally small set then this is unique, though not canonically - there are many maps from it to every other group.

You may wish to learn about initial and terminal objects.

21. Dec 28, 2004

phoenixthoth

I see. Thanks.

Edit: Any categories with universal elements of which SET is a subcategory?

Last edited: Dec 28, 2004
22. Jan 3, 2005

Hurkyl

Staff Emeritus
Set is the category of small sets, so you could simply take a category whose elements are all sets with cardinality less than or equal to your favorite large cardinal.

I asked someone at work about topoi, and he refused to be pegged as someone who knows a lot about them, but he said his first instict was that it would not be inconsistent to have an object to which there is a monic from every other object. (your "biggest" set)

23. Jan 4, 2005

Hurkyl

Staff Emeritus
I've been working on categorizing Cantor's diagonal argument in a topos, and I've reduced it to this:

Suppose f:A --> W^A is an isomorphism of an object with its power object. (W is Omega, the subobject classifier)

Then, we can create the map g:A --> AxA --> (W^A)xA --> W by applying delta (in Set, sends x to (x, x)), applying f to the first argument, then applying the evaluation morphism. In Set, we've simply set g(x) := f(x)(x).

Now, select any other morphism h:A --> W. We can then construct maps:

1 --> E --> A

Where E --> A is the equalizer of g and h. (In Set, E is simply the subset of A on which g and h have the same value, with its inclusion map)

So, Cantor's argument boils down to finding a morphism h such that E is the initial object. In Set, this is easy -- let h take the opposite value of g at every point. I can't yet prove I can do that in a topos.

If you can find such a morphism, then we have a morphism 1 --> 0, and if such a morphism exists, the topos is degenerate (aka "inconsistent", because it has a one-valued logic)

It appears essential that the topos not have a two-valued logic -- I don't know yet if it can be Boolean.

24. Jan 6, 2005

Hurkyl

Staff Emeritus
Here's a theorem for you:

Let P(A) be the set of all unary relations on A.

(This notion corresponds to that of the power set in ZFC, because there is a 1-1 correspondence between unary relations on A and subsets of A)

Let f be a bijection from A to P(A).

Let j be any unary operation on the logical values.

Then, j has a fixed point.

Proof:

Define the relation g on A as:

g(x) := f(x)(x). (Remember, f(x) is a relation on A, so it can be evaluated at x)

Then the composition of j and g, (j o g), is also a relation on A.

We can compute s, an element of A, to be f^-1(j o g).

So, we have the following:

g(s) = f(s)(s) = (j o g)(s)

therefore, g(s) is a fixed point of j.

25. Jan 6, 2005

Hurkyl

Staff Emeritus
Oh, and corrolary -- topoi are insufficient for your purposes, since their internal logic is supposed to be a Heyting algebra (Boolean algebras are a kind of Heyting algebra). However, the pseudo-complement (which I'll write as ~) has no fixed points, unless the logic is inconsistent, because:

Suppose s is a fixed point of ~

By definition of ~: s and ~s = 0
Then, s and s = 0
Thus s = 0
But ~0 = 1
Thus, 0 = 1

So, the logic is single-valued. (i.e. inconsistent)