|
|
|
|
|
|
by lomnakkus
3265 days ago
|
|
|
Ok, I'm clearly lacking in fundamentals here. I've seen HoTT seem receiving quite a bit of attention, but after reading a few papers and texts it seems that it's just out of reach without additional introductory material. I got about 50% though TAPL, if that's any indication of (my lack of) sophistication in type theory. I really should pick that up... Any recommendations for introductory texts? As a practical matter, what do the mathematicians who don't give AF about set theory (as you say) do? Just assume other axioms that "do enough" adn then go from there? |
|
|
You could check out Lambek and Scott (1970s), which is excellent. Also Girard (citation for this one was in TAPL). I also think Martin Lof himself is pretty good for the feel of things, but he has always seemed kind of cryptic and mystical to me. There are also some good videos on YouTube that Steve Awodey (CMU) recorded for more intro/motivation. I'd also add Vovodsky's three Bernays lectures on YouTube for the general idea of using typed lambda calculus vs set theory as foundations.
Sociologically, my impression is that most mathematicians trust that the usual axioms of set theory are consistent and safely ignore them. So, yes -- they choose axioms in their own field that are known to be derivable in set theory. Even in intro Analysis textbooks, where the role of set theoretic axioms themselves can be pretty easily extracted from the construction of the reals, I don't think you'd see set theoretic axioms explicitly appealed to (might be wrong about this). In constructive mathematics, it ends up mattering where Choice is used I guess. And it matters how these uses can be "constructivized." But constructive analysis is primarily motivated by foundational considerations. So it is not really an example of ordinary mathematics. Some axioms, like Regularity, are almost never even implicitly used outside of set theory itself except in very specific cases.
Most every case where there is a question of whether a given bit of mathematics is derivable from the usual axioms of set theory arise only within set theory itself (CH, measurability of projective sets of reals, etc), and so such questions are easy to ignore for the vast majority of mathematicians. They simply don't care that much about logic and set theory aside from "just working" under the hood, as it were.