While reading appendix A of John Harrison's "Handbook of Practical Logic and Automated Reasoning" a somewhat advanced theorem is appealed to as a prerequisite for characterizing when an inductive definition is well-formed. I don't understand why a much simpler formulation doesn't suffice, which in fact allows an every broader range of definitions:
Let Σ be any set of wffs in some logic. Let Thm(Σ) be the set of all theorems provable from Σ. For a given name σ, remove all theorems from this set that are not of the form ⌜α∈σ⌝ for some constant term α, producing a set of wffs M(σ), the set of theorems that simply attribute that some constant is a member of σ, or 'the membership theorems' for short. Then, given σ, define the set referred to by the name σ using the axiom schema: α∈σ ↔ ⌜α∈σ⌝∈M(σ).
On this treatment, Harrison's example of a malformed definition n∉E / ∴ n∈E, interpreted as Σ = {'n∉E→n∈E'}, is not malformed, but actually defines the universal set, such as ℕ if the context is number theory, etc.
Why isn't such an approach normally used to speak about inductive definitions? The above formulation is a little wordy, but it's basically as simple as saying "If you can prove it's in the set from these premises, it's in the set, even if you can also prove the opposite, but if you can't prove it's in the set from these premises, it isn't." I think I have always assumed that this syntactic characterization is the true spirit of inductive definitions, thus not understanding why a fuss is always made about showing that inductive definitions are a coherent form of definition..