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.)
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?
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.)
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.
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.