Hello again math forumites. I have returned with yet another exciting, yet possibly poorly-worded set theory question.
I have been trying in my spare time to develop a solid understanding of the essential basics of logic and set theory. I've had a small amount of graduate coursework in set theory (my field is computer science), but most of my math work is autodidactic. Eventually, I want to understand the concepts well enough that I could instruct others. I think it was Einstein who said something like: you never truly understand something until you can explain it to a child of six. Or maybe that's a misquote. Anyway, here's my question...
What are the minimal assumptions necessary in order to construct and assess the consistency (as best as one possibly can) of the majority of mathematics? AFAIK, the only two foundational bases for math are set theory and topoi theory, and I'm much more familiar with set theory, so I'll start there. Here's what I know we need:
1) One undefinable concept/object (set)
2) One undefinable binary predicate (membership)
3) Five axioms (extensionality, pairing, union, power set, induction)
4) One axiom schema (separation)
With the exception of logic theory (which is my the crux of my question, below), the above covers pretty much everything in "normal" math. You can strengthen these by adding choice, make metatheory simpler by adding regularity, and improve the schema of separation to the stronger version (replacement) to make some proofs simpler and to allow investigation into large cardinal theory; but these are not needed for the founding of most of applied mathematics.
Anyway, the one thing I left out above is logic theory...and this is where things get confusing. Numerous references, including Friedman, who I was lucky enough to have as an instructor in one case, and books I have read, have commented that the "bootstrapping" (something I actually understand well) between logic and set theory is not an argument of circular reasoning. The basic description seems to run like this:
A) You start with intuitive logic.
B) From this you can describe proofs in set theory, and show how set theory implies the existence of things that can be used to model objects like functions.
C) Since set theory is strong enough to model the discrete math of logic, you can prove things about formal logic by using set theory and those intuitive logical principles. This gives us a more "formal" logic.
D) Today we describe set theory itself by using this formal logic.
Therefore, we don't have a logic --> set theory --> logic circle. It's more of, informal logic --> set theory --> formalization of logic, I guess.
Now, I can buy the fact that just because we write the axioms of set theory in first-order logic (FOL) does not imply that FOL need "come first". I mean, if I write the axioms in English, that doesn't mean English is needed for the axioms; it's just the language I'm using to communicate.
What I can't shake is the suspicion that some level of intuitionistic logic must be combined with set theory before one can prove anything at all, and thus, there are additional assumptions being made in addition to 1-4 above. I have not seen these assumptions spelled out anywhere, probably because most mathematicians don't really care when this starts drifting into epistemological stuff.
For example, it seems rather clear to me that one needs to assume, in addition to 1-4 above, the validity of a logical inference rule like modus ponens. Is this true?
If so, what else must we assume about logic before we can describe mathematics with set theory (and by its inclusion, formal logic itself)?
If not, why not? I mean, it seems like one could come up with a faulty inference rule which is capable of asserting its own existence, which would mean 1-4 are not a complete set of assumptions (unless maybe there is some consistency measure that determines which inference rules are or are not faulty)?
(Note: I know much of the lingo above uses "model", "truth", etc. in a loose and probable highly-irregular manner, but keep in mind I'm talking about assumptions of informal logic needed to jump-start set theory into proving things about formal logic.)
Thanks in advance!