Many applications of Kuratowski-Zorn Lemma exhibit a common principle, that I could best summarise as:
If one defines a structure by "nice" conditions, then Kuratowski-Zorn shows a maximal structure exists.
Here, "nice" conditions are roughly the ones of the form $\forall a,b,c ... : \ \phi$ where $\phi$ is a condition not involving any quantifiers, of some special form.
This is admittedly vague, and my question is precisely how can this be made precise and rigorous. I think the general principle is best shown by an example.
Suppose that you want to use K-Z Lemma to show that maximal ideals exist in any ring $A$ (commutative and with $1$). The natural thing is to consider the family of all ideals $\mathcal{I}$ (excluding $A$ itself) as family of sets partially ordered by inclusion, and then show that it satisfies the assumptions of K-Z Lemma --- once we do this, the Lemma ensures the existence of the sought maximal element.
Thus, it remains to show that $\mathcal{C} \subset \mathcal{I}$ is a chain, then it has an upper bound, and the only natural candidate for this upper bound is $\bigcup \mathcal{C}$. Note that until this point, we never mentioned what it means for a set $I$ to be a ideal. A possible (natural) definition could be:
- $I \cdot A \subset I$
- $I+I\subset I$
- $1 \not \in I$
but we can just as well write it as:
- $ (\forall a,b \in A) :\ (a \in I) \Rightarrow (a \cdot b \in I)$
- $ (\forall a,b \in A):\ (a,b \in I) \Rightarrow (a + b \in I)$
- $\neg (1 \in I)$
Now, the problem boils down to proving that the conditions 1,2,3 are preserved by arbitrary unions of pairwise comparable sets. Thus, let $M := \bigcup \mathcal{C}$, assume that one of the conditions holds for all $I \in \mathcal{C}$; we show that it holds for $I = M$. For condition 3., things are not very interesting, so let us restrict the attention to 1,2. Each of these conditions is of the form $(\forall a,b \in A) :\ (\square \in I) \Rightarrow (\triangle \in I)$. To prove this holds for $I = M$, we can proceed as follows: First fix $a,b \in A$. Then pick $I_0 \in \mathcal{C}$ sufficiently large that $\square \in I_0$ (if no such $I_0$ exists, then the implication is vacuously true!). Since the condition holds for $I = I_0$, $\triangle \in I_0$. But $I_0 \subset M$, so $\triangle \in M$. Since $a,b$ were chosen arbitrarily, condition holds.
The argument runs smoothly enough, and one could certainly argue that I am overcomplicating things. What pains me, however, is that I could have put anything (made up from $\cdot$,$+$ and the variables) in the place of $\square$ and $\triangle$ above, and the argument would remain unchanged. Thus a more general fact is true:
If a structure is defined by requiring that $S$ is such structure if and only if it satisfies any number of conditions of the form $(\forall a,b,\dots):\ (\square \in S) \Rightarrow (\triangle \in S)$, then there is a maximal such structure contained in $A$.
In principle, this is not a big problem, since one can always do the standard reasoning, paste in the appropriate place a verification that everything works fine when passing to the monotonous sum, and be done. Nevertheless, it does feel a little "unmathematical" to be repeating the same reasoning all over.
What interests me is: what is the most general "type" of conditions that can be used in the "standard" reasoning? (i.e.: How can one make the notion of "nice" from the top precise?) Can the above thoughts be turned into something rigorous?
Here is one answer.
A first order theory $T$ is called inductive if it consists of formulas of the form $$(\forall x_1) \dots (\forall x_k) (\exists y_1) \dots (\exists y_\ell) p$$ where $p$ is quantifier-free. If $M$ is a structure for the language of $T$, and $M$ is the union of a family of substructures $(B_i\mid i\in I)$, totally ordered by inclusion, such that each $B_i$ is a $T$-model, then $M$ is a $T$-model (exercise 3.4.b, Notes on Logic and Set Theory, P. T. Johnstone).
This includes your example of ideals in a ring, by considering the theory of $A$-modules. An example of a theory that cannot be expressed as an inductive theory is the theory of totally ordered sets with a greatest and least element, and indeed $\mathbb R=\bigcup_{n\in\mathbb N} [-n,n]$ shows that the union of such sets does not always have a greatest and least element.