\begin{definition}[Definition:Inductive Set]
{{mergeto|Definition:Infinite Successor Set}}
Let $S$ be a set of sets.
Then $S$ is '''inductive''' {{iff}}:
{{begin-axiom}}
{{axiom | n = 1
        | lc= $S$ contains the empty set:
        | q = 
        | m = \quad \O \in S
}}
{{axiom | n = 2
        | lc= $S$ is closed under the successor mapping:
        | q = \forall x
        | m = \paren {x \in S \implies x^+ \in S}
        | rc= where $x^+$ is the successor of $x$
}}
{{axiom | rc= That is, where $x^+ = x \cup \set x$
}}
{{end-axiom}}
\end{definition}