So I finished the set theory lecture a while ago (and read a bit on wikipedia). I got a few questions left, if anyone wants to help. (I got the sense that there are actually a few different models which work slightly differently, so this is about ZFC).
First (this was not really explored in the lecture, I just tried to gather it from thinking & the internet), do I understand it correctly that
ℕ =: ω = {0, 1, 2, ...}
aka the natural numbers and the smallest infinite ordinal. Then the next "bigger" ordinals are
ω+ = ω ∪ {ω} = {0, 1, 2, ..., ω}
ω++ = {0, 1, 2, ..., ω, ω+}
...
and there exists
α := ω ∪ {ω, ω+, ω++, ...} = {0, 1, 2, ..., ω, ω+, ω++, ...}
and then
α+ = α ∪ {α} = {0, 1, 2, ..., ω, ω+, ω++, ... α}
α++ = {0, 1, 2, ..., ω, ω+, ω++, ... α, α+}
...
and there exists
β := {0, 1, 2, ..., ω, ω+, ω++, ... α, α+, α++, ...}
and
γ := {0, 1, 2, ..., ω, ω+, ω++, ... α, α+, α++, ..., β, β+, β++, ...}
and then you can play that game forever and can keep getting ordinals that way, and the ordinal which is the union of all such ordinals is ω1, which is kind of like ℕ x ℕ and therefore still countable in the same way (but the first non-recursive ordinal), so it's still ω1 ~ ℕ and then there exist ω1+, ω1++, ω1+++, ω1 ∪ {ω1, ω1+, ω1++, ...} := Ψ and Ψ+, Ψ++, ω1 ∪ {Ψ, Ψ+, Ψ++}, and this can be done arbitrarily often again, until we get something which is kind of like ℕ x ℕ x ℕ which is still countable, let's call it Φ and then building from Φ you could construct something like ℕ x ℕ x ℕ x ℕ which would still be countable, and if you do that arbitrarily often, then you have the union of all such ordinals, which is also the union of all countable ordinals and is kind of like ℕ x ℕ x ℕ x ℕ ... and called ω0 and the first uncountable ordinal. Is that all correct?
(It's pretty weird. I like it. If it actually works that way.)
This is a pretty good summary, yes. You have to be a bit careful with the first uncountable ordinal, in that pretty much any union you can physically write down is going to be smaller than that ("union of all countables" works fine of course). Other than that, yes, you have the idea.
More general picture:
It is important to remember that set theory is not trying to be a 100% precise description of the mathematical world. Maybe that is what the original set theorists wanted, but the reality is that that's not feasible. Instead, set theory is trying to write down a decent approximation of what we believe the mathematical world to be. This, silver, is where your mild confusion arises, I believe.
As logicians, we write down some number of axioms that we believe should hold in mathematics (Foundation is a great example - we take it as an axiom because, as mathematicians, we do not want to deal with sets that might be infinitely nested or horribly ugly in other ways. It is a statement of our belief that mathematics should be well-founded on a nice clean basis without infinite recursions. But you don't
have to take Foundation - indeed, I believe - though don't fully understand - that computer scientists often like to use set theory without Foundation, because it suits their theoretical basis somehow.). But we do not expect - indeed we know that it is impossible - to write down a set of axioms that covers absolutely every facet of possibility.
At this point you need some grounding in Logic/Model Theory, The idea is: we have written down some axioms. But since our axioms are not complete (and indeed they cannot be), there are bound to be lots of different structures that satisfy those axioms. In other words, there are lots of "models of ZFC" (or at least we believe that there should be). Here, "model of ZFC" means "collection of things/sets that satisfies all the axioms". There might well be lots of different models of ZFC, and we want to believe that the "true" mathematical world is one of those models - but we don't know which one.
So, to your questions, if you ask "does a set with *some weird property* exist?", if it's not proven or disproven by the axioms, the answer will be:
"Some models of ZFC contains such a set, and some do not." We haven't decided yet, as mathematicians, which of the various models of ZFC is the "right" one - if we ever do, that would be tantamount to adding an additional axiom. (For instance we might take GCH as an axiom - though this is unlikely to happen any time soon.).
This goes into the scope of some slightly deeper theory (can send you some notes on that if you like, silver). Foundation is once again a good example. It is proven that the axiom of Foundation is independent of the other axioms (excluding Choice). How do we prove this? "Easy". We write down two structures. One of them satisfies all of the axioms including Foundation (still ignoring Choice), and one satisfies all of the axioms except it DOESN'T satisfy Foundation.
So, if we decided we weren't sure about the Axiom of Foundation any more, then we would have at least two possible models of Set Theory - and we'd have to accept both as equally valid (though one contains some infinitely nested sets, and the other doesn't).
No idea whether this makes things clearer. Anyhoo, general abstract chat over, wanted to reply to some quotes:
Second, if this is all grounded in this set language and can all be done formally, why aren't all mathematical theorems just provable or disprovable through some software which handles First-order logic?
Even if computers were any good at producing proofs (they're not) - there's the issue that not every mathematical idea can be expressed in first-order - even when you use all the power of set theory.
Third, is this in any way applicable beyond providing a generally better understanding of maths? (Not saying this wouldn't be enough reason to study it.)Depending on how you view it, it's more an exercise in its own right - though the understanding of infinite cardinals is VERY useful mathematically.
And fourth, I'm a bit confused about the whole principle of axioms. If the idea is that they give you ways to construct new sets, and your universe always contains exactly all sets which can be constructed this way, doesn't the axiom of foundation (which was the only one introduced which said something doesn't exist) just assert something that must be true anyway (since otherwise it is inconsistent with the other axioms), but for which no-one found a proof (and presumably there is none?) If so, that seems more like a theory that everyone beliefs in rather than an axiom to me, because it's asserting something rather than defining it, and because introducing it doesn't change the universe.
I've alluded to this above. The bit in italics is probably your biggest stumbling block. The important thing is that the axioms lay out some rules for what sets SHOULD look like (we should have all of these sets, but not these ones, etc), but it doesn't lay out every POSSIBLE rule. The axioms leave room for some uncertainty about which things are sets and which aren't.
And 4.5, isn't the power set axiom implied by the replacement scheme? It seemed as if otherwise the axioms were meant to have as little redundancy as possible, so that seems odd.
I don't think this is true.
Responses in bold.
There are models of ZF(C) without the power set axiom, which are actually some of the more populary axiom systems known as ZF(C)^{-}.
Unless you're using quite an unusual terminology, ZF^- is typically ZF without Foundation - removing Powerset is not a familiar idea to me.
In each individual model, yes it does. However, there are models where it does, and models where it doesn't.
Consider for example the theory consisting only of the axiom "Empty sets exists". The model consisting only of a single set is a model of that, but so is any model of ZFC.
This is a good way to put it.
Oh yes, I was assuming that. Isn't that the point of the axiom system, to regulate exactly which sets exist?
It gives you some of the rules, but it CANNOT regulate it entirely. There will always be some things which may or may not exist as sets - at that point it is up to your philosophy to decide which
Okay, so the claim of the axioms is not "these are the sets that exist," but "these are some sets that exist" and then the axiom of foundation says "these are some sets that don't exist," and every set that can't be constructed from the axiom and doesn't contradict the axiom of foundation is up for debate?
This seems like a good description.
Note that there is no statement like "this sets exists" in the language of set theory, only "a set with this property exists". (For example "the empty set exists" is not a set-theoretic statement. "There is a set x such that no set y is an element x" is.)
Hmm. In the presence of the Extensionality Axiom, this distinction is pretty much negligible. The Empty Set is unique by extensionality, as are many of the other sets given by axioms like Union/Pairs/Comprehension.