When did you grow out of set theory?

>>8270707
Why should i grow out of set theory?

>>8270707
When I learned about category theory

>>8273014
test

>>8273014
Do you mind explaining to be how categorical foundations for math and categorical logic works in broad terms? I've only read the first 7 chapters of Awodey though.

>>8270707
When I fucked your mum and lost my virginity.

No need to worry about autistic math shit when you're an alpha male :^)

>>8273020
For categorical foundations you're best off just reading the HoTT book.

In general categorical logic is based on a correspondence between different classes of categories and logics. The types are objects and a term of type X is a certain type of morphism into X, roughly speaking. So if you have products you can get product types, sums give you sum types etc. A product type is just a type of pairs which corresponds to the categorical product. But you can have other type-formers, like in multiplicative linear logic where you have a non-Cartesian monoidal product.

But the problem with categories is that hom-sets are sets, so subobjects of A form a preorder, which means they automatically give you an *extensional* type theory where the identity types are just truth values. So people conjecture that HoTT is modeled by some kind of infinity category but they haven't worked out all the details yet.

>>8273020
one way is topos theory.

basically, a (Grothendieck) topos has a few basic propeties that make it act "as good as" sets; namely:

-has finite limits and arbitrary colimits
-has image factorization system
-has "singletons"
-comes with internal higher-order logic: i.e. can construct all of higher-order logic on a topos, so long as the basic symbols come from objects in the topos; e.g. can form predicates, quantifiers, can "curry", etc.
-has a notion of "power object"
-is "extensional" in some sense - it has a set of generators which can be used to "test" if morphisms are "the same or not"

The characterization of a Grothendieck topos however uses the notion of a set in at least one place usually: either by constructing the topos a Set-valued sheaves on a site; or abstractly by saying that the topos must have a SET of generators.

That said, once you "have" one, you can do pretty much all of your reasoning "internal" to the category. Issues like >>8273064 mentioned (hom-SETS) are not as much of an issue, because E(x,y) can be represented as an object x^y inside the topos itself (we don't need to refer to set E(x,y)). Similarly, power sets can be constructed internally as O^x, where O is the subobject classifier of the topos (the "truth table" which classifies monomorphisms in the topos).

An example of "internalization": O is usually thought of as a lattice, given the logical operations "and" and "or". This is often done "externally" by looking at the SET E(1,O) of global sections. However, O also forms a lattice-object in E, meaning that there are diagrams in E expressing the fact that O is a lattice without reference to sets of homomorphisms into it.

We can in fact construct syntactic sites for geometric theories and the G.topoi on them "classify" models of that theory in any G. topos. I.e. we can talk about "models" of a theory, etc. just by looking at the 2-category of G.

>>8273094
In case this all seems pointless (which if you were just working with SET, it would be), I'll give one immediate generalization that you get for free. Any poset P is a category, and we can give it the trivial topology. Sh(P) is a topos, and its internal logic is a generalization of the Kripke semantics for <W,P>, where W is the set of objects and P is the ordering by morphisms. The generalization is that we actually consider arbitrary functions between worlds, not just inclusions (though the traditional semantics comes out in the case that each restriction W0->W1 is injective).

>>8270945
Because it's a weird ontology that is useful insofar as having "stuff" to get your hands on but is miserably awkward at describing structure of any kind.

Consider the construction of the reals as cuts of Q, in turn as eq classes of Z, in turn eq classes of N, in turn built from the v.n. hierarchy. There are now all sorts of "accidental" membership relations all over the place that have nothing to do with the structure of R, Q, Z, or N. For example, Z alone has a bunch of data about ordered pairs in there now, and it is well posed to ask strange questions like "is {{{{},{},{{}}}},{{{}}}} a real number?" A lot of it just seems to rely on convention and nothing deep.

For example, if we use the usual encoding for pairs, take (0,1)={{0},{0,1}}={1,2}=3. I just proved that the ordinal 3 is the same as the ordered pair (0,1). This is clearly useless and preposterous, but all "structure" encoded with set theory will have to rely on these conventions.

Not to mention there are about 3 or 4 inequivalent ways to define ordered pairs in set theory. Set theory doesn't even come with a language to describe in what sense these might be "equivalent characterizations" of something.

Category theory on the other hand deals with all of this relationally. A product AxB is a product because it bears certain universal relationships to the sets A and B.

>>8273094

>>8273064

that sounds incredibly interesting, even though I barely understand anything about it.
What do I have to read and learn in order to understand all of that?

>>8273219
I am not >>8273064, so I can't speak to HoTT; nor am I CS oriented.

For toposes and classifying toposes, etc. there are a few main texts. The most accessible is Mac Lane & Moerdijk, and you can jump right in from Awodey.

Makkai and Reyes is really where theories got fleshed out, though if you'd like to get a sense of simpler algebraic theories in general categories, you might want to try "Toposes, Triples, and Theories". Johnstone's "Topos Theory" technically has almost all the basics for doing logic in toposes, but its not easy going (he's not the best at working out details or telling you which chapter some piece of terminology came from). Borceux's handbook (3rd I believe?) has a bit on locales and toposes, not the most thorough, but a good companion because he is excellent at exactly what Johnstone is bad at (narrative, listing where prior definitions and theorems came from, etc.).

For syntactic categories and stuff, this is really Olivia Caramello's bread and butter, and she has a bunch of handouts/short papers/slides on her websites that are nice supplementary materials.

>>8273219

Well, you need to know category theory first. Categories for the Working Mathematician is still a classic. That assumes that you have enough examples from different areas of math though; for something more basic you could try Schanuel's Conceptual Mathematics. Once you know CT you can get the basic idea.

>>8273219
Awodey also has some simple handouts on sheaf logic as S4, and I think it was his thesis that was on theories in general topoi, but I can't remember the names. Dig around his website and stuff and it will have a few "short papers" that might whet your appetite.

>>8273235
>>8273236
>>8273238
Thanks guys! I'll try to finish Awodey, though I'm struggling with it quite a bit learning it on my own and lacking formal university maths education.
Since topoi sound really cool, I guess I'm gonna go read Mac Lane and Moerdijk afterwards.