Start with an intuitive notion of a set like “a set can contain things like atoms, cars, every real number, or any other set, even itself”.
Logical and semantic paradoxes arise.
There are several ways to fix those paradoxes, by putting constraints on how to build sets. This has the side effect of forcing us to rethink the whole theory under a new framework, which is that of a more formal system.
From there “usual” properties of sets can be derived again in a more sane manner:
Since isomorphism and equipotence (or cardinality) are very useful concepts in a lot of more advanced domains, it makes sense for me to learn them from set theory which is the most basic theory in which they occur.
In the next sections I will focus on the problems that needs to be solved instead of collecting small results.
Pretty much every maths textbook comes up with an informal framework in which to develop its theory (symbols, logic rules, and simplified version of other required theories). Usually, the framework is made of tools such as propositional calculus combined with a few predicates as well as postulates stated in plain english. Then by applying some kind of modus ponens — which basically states that if I know that “P entails Q” is true and that “P” is true then “Q” is true — I can more of less easily derive interesting resultst from the postulates with the advantage of not having to write 12000 lines proofs.
Without axioms we have no base cases for our theorems. A theorem is derived from something, this something being either another theorem or an axiom, which cannot be derived.
Definitions are just shortcuts, they bring nothing new to the table.
Lemmas and corollaries are specific cases of theorems. A lemmas is a helper theorem for a more complex proof. A corollary is a theorem that almost immediately follows a more central one.
In set theory books, axioms are usually written in plain human sentences. But theorems are almost always written in terms of predicate calculus with a single predicate: \(\in\).
This means that at some point in the derivation process we go from plain sentences to some form of predicate calculus. An ideal formal proof would never begin with a plain english axiom. Instead, it would encode this axiom in the same formal language as theorems.
For instance one axiom that is usually stated in plain english is this one (you don’t need to understand it): \( \forall A \, \exists B \, \forall x \, (x \in B \leftrightarrow (x \in A \wedge \varphi(x))) \) for any property \(\varphi(x)\)
The reason why most books don’t do that is that this requires to actually choose and argue for a specific formal logic framework, which isn’t the main goal here. It is more relevant to have axioms that reflect the conceptual problems they are meant to solve and then to wonder how they would translate in say, classical or non-classical logics.
From there those books usually provide some kind of basic, informal logic framework to work with, hence why we can go from plain english axioms to theorems written in an informal predicate calculus. The trick is in the word informal, which really means convingly enough here.
More practically, authors avoid answering questions like what’s the difference between “P is true” and “P” is true.
Past logic, advanced maths books usually do the exact same thing with set theory or natural numbers, glossing over them only in an informal way. You job as a reader is to read these chapters and to ask yourself “do I feel confident enough that all of this stands on its feet”. There are many cases where it is sufficient to be aware of the wobbly parts. It is also unrealistic to learn all of the ramifications of a theory.
But anyway, more on logic here.
ps: I usually write postulate instead of axiom.