Hello,

 

I have a somewhat-working familiarity with set theory, and have recently been reading (naively) about category theory and type theory, each proposed as potential autonomous foundations for mathematics.

 

To someone who has a better-than-vague understanding of the three, what is the discrepancy or motivation for one over the other?

 

Why isn't first-order or higher order logic considered the "foundation"?

 

When considering set theory as a foundation, can all discussion generally be deferred to ZFC; for category theory, can it be deferred to the category Set or topoi; for type theory, can it be to homotopy/univalent type theory?

 

Thank you,

Sato

Edited November 9, 201411 yr by Sato

I have a somewhat-working familiarity with set theory, and have recently been reading (naively) about category theory and type theory, each proposed as potential autonomous foundations for mathematics.

I am not well versed in these foundational issues. So what I can tell you is...

 

When considering set theory as a foundation, can all discussion generally be deferred to ZFC

I don't know about all discussions, but by set theory one will often mean the ZFC. This is formulated using first order logic.

 

for category theory, can it be deferred to the category Set or topoi;

 

You cannot defer everything to the category of sets, though that maybe a useful example to have in mind. For sure we have categories for which the objects cannot be considered as sets.

 

Also don't confuse this with small categories. That is categories where the collections of objects and morphisms are sets and not just proper classes.

 

For topos theory we have categories that behave like sheaves of sets. My understanding is that we need small categories here.

 

 

for type theory, can it be to homotopy/univalent type theory?[/b]

I don't know type theory.

I'm sure I know substantially less than ajb about this but I do like the term 'kittygory' for 'small category'.