[jtc1983]

Use of the phrase "not-necessarily-all-that-well-founded" is unfortunate since standard set theory studies the properties of extensional, well-founded objects in general. Though clearly you didn't have the technical understanding of well-foundedness in mind. Just might confuse ppl because there is a branch of set theory called "non-well-founded set theory" that is perfectly respectable -- I.e., and "well-founded" in the sense you intend -- but not about the same objects studied in the standard context.

I believe what you have in mind regarding set theory as "not ideal for 'foundations'" (why is the word foundations in quote, btw?) is that there is a recent push to reexamine the prospects more intensional foundations based on type theory. The most promising and currently fashionable version of this push is Homotopy Type Theory (HoTT), which has been given press and prestige from the IAS at Princeton and interest from Fields Medalist Vladimir Vovodsky (sp?). There are plausible reasons given, though often polemical, for preferring some sort of type theoretical or category theoretical foundations over set theoretical ones. Perhaps most importantly, for readers of HN, the comparatively easy formalization into computer-checkable proof and computer-assisted proof (look up, for instance, Coq).

That said, there is a long way to go before HoTT (or something like it) displaces traditional foundations and set theory. For one thing, there is no obvious axiomatization or way to confirm that HoTT is a suitable foundation for extant non-foundational mathematics. For one thing, standard type theory (MLTT) plus Vovodsky's univalence axiom is proof-theoretically equivalent to a subsystem of analysis. I would guess that, for instance, you can't prove that all Borel sets are measurable using MLTT plus univalence (but this is totally speculative and I would appreciate being corrected).

Last -- I suspect the only mathematicians who find set theory proofs beautiful are set theorists. Most other mathematicians don't really give af about set theory.

[lomnakkus]

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?

[jtc1983]

Looking at TAPL, it seems like a good text coming at things from the theoretical computer science angle. I'm unsure how exactly to branch out from there, since my own background is more in math logic. So prob best to take my recommendations with that in mind (I think there's a ton of work in CS in the last 20 years that I'm just totally unfamiliar with).

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.

[lomnakkus]

FWIW, I've only had a pretty basic intro to math meta-theory, and I think my most "advanced" course in that direction was about Point Set Topology (+ some discrete math courses, but that's par for the CS course).

If one is a mathematician, I think it's entirely reasonable to just "trust" your basic axioms of your "sub-field", but OTOH I can really understand the worry that the rug is going to get pulled out from under you... which is a pretty remote worry given the complexity of math nowadays.

Anyway, thank you for taking the time for that response.

[jtc1983]

Whoops -- Lambek and Scott is 1986. My apologies