Online resource for type theory?

[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.

 

[matt grime]

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

 

[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.

 

[Hurkyl]

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.

 

[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...

 

[matt grime]

but it isn't a small category

 

[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

 

[Hurkyl]

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 want to 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.

 

[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:

 

[Hurkyl]

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.

 

[phoenixthoth]

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!

So... did you go into work today?

 

[Hurkyl]

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

 

[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! :)

 

[Hurkyl]

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!

 

[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)?

 

[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.

 

[Hurkyl]

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.

 

[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.

 

[phoenixthoth]

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.

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.

 

[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.

 

[phoenixthoth]

I see. Thanks.

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

 

[Hurkyl]

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)

 

[Hurkyl]

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.

 

[Hurkyl]

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.

 

[Hurkyl]

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)

 

[phoenixthoth]

Thanks Hurkyl

You probably knew where I was going with this:

In three valued logic: ~0 != 1, right?

As in Max Tegmark's level 4 theory, I'm looking for something which can be somewhat correctly be called "the universe." Categories with universal objects (by that I mean objects for which all other objects are monic to it--rather than the standard definition of universal) seem to be the closest thing.

 

[Hurkyl]

Hrm, isn't ~0 = 1 one of the more desirable properties of a negation operator?


In a Heyting algebra (and thus a Boolean algebra), ~x is supposed to be the maximum possible value for s in the equation s and x = 0, so ~0 = 1.


The other multivalued logic I know (that isn't Boolean) is the arithmetic one, of numbers between 0 and 1, where ~x = 1 - x.

 

[Hurkyl]

Now, flipping through one of the texts I have checked out yields something interesting:

As a reminder, a Cartesian Closed Category is one with a terminal object, all binary products, and all exponentials.

Anyways, this text mentions the possibility of a "reflexive" object, having the property that:

V^V < V

Where A < B means there exists a monic A --> B and an epic B --> A that, when composed, yield the identity on A.


If an object is reflexive, then we also have VxV < V, as well as t < V. (So, all powers of V are < V)


It turns out that if V is reflexive, then the set of all A with A < V is a cartesian closed category. (And, clearly, V is the "biggest element" in precisely the sense you want)


Now, I didn't come across any nearby examples of reflexive objects... I suspect it has more to do with logic, propositional calculus, lambda calculus, and related concepts than with set theory. (The applications occur in a chapter called "Formulae, Types, and Objects" -- this is a computer science text)

 

[phoenixthoth]

Yes, I do believe that is what I'm looking for. If you find an example, please let me know.

 

[Hurkyl]

The category of Scott Domains has some reflexive objects. I don't understand that chapter yet, though, so I'm not much help! We seem to be beyond the point where I can find useful information on the web, too.

 

[Hurkyl]

New theorem, but I think you already anticipated this one.


Suppose f is a bijection between V and V^V.
Then, every function V--->V has a fixed point.


Proof is roughly the same as the previous one I gave:

Let j by a function from V to V.

Define g(x) = f(x)(x)
Let s = f^-1(j o g)

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

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

 

[phoenixthoth]

Just a shot in the dark, but does this property characterize the V such that V is in bijection with V^V?

In other words, if every function from V to V has a fixed point, then is V in bijection with V^V?

(This links up with my definition of a awareness, but let's discuss that there and not here.)

I will work on this, too.

 

[Hurkyl]

Note that we have a binary composition on V, given by:

VxV ---> (V^V)xV ---> V

Where the first arrow applies the isomorphism to the first argument, and the second arrow is the evaluation morphism.

In a more set theoretic presentation, for a in V, let $\bar{a}$ be the corresponding element in V^V. Then, $a \cdot b := \bar{a}(b)$

Clearly, in general, this operation appears to be noncommutative and nonassociative. Such a thing is called a "magma"

http://en.wikipedia.org/wiki/Magma_(algebra)

Maybe something in there is useful.


Clearly, elements of a magma M act on that magma by left multiplication, and in this way we recover part of M^M... but not necessarily all of it, I suppose.


Actually, we have what might be a different binary operation. If V is reflexive, then we have VxV <= V. (I've changed notation -- I hate using < when the objects can be isomorphic) By definition, there's a monic VxV --> V, so this can be taken as a binary operation.

 

[Hurkyl]

It strikes me that I have not proven it impossible for V^V <= V in a topos either. I'm working on seeing if it can be true for the subobjects of 1 (i.e. the logic values).

Also, technically I have not proven it impossible for PV < V in a topos... there's certainly a monic V --> PV, but I don't know if the existence of a monic PV --> V implies V and PV are isomorphic.