A Simpler Characterization of Inductive Definitions? 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..
 A: Inductive definitions are about truth rather than provability, and the sort of proof-based definition you are talking about would break on many inductive definitions. Unfortunately, it is hard to give truly elementary examples of this; the simplest examples, such as the definition of the natural numbers or the definition of the set of LISP programs, don't have the problem.  But when we start looking at inductively defined sets whose members are "infinite objects" like functions, some particular objects may end up inside the inductively defined set even though we cannot prove that they do. 
One place where this happens is the inductive definition of the set of all partial computable functions on $\mathbb{N}$. One clause of this definition is:


*

*If $f(x,y)$ is a partial computable function and $f(x,y)$ is defined for all $x$ and $y$ then the function $g(y) = (\mu x)[f(x,y) = 0]$ is partial computable


I bolded the key phrase there: the clause does not apply to all functions in the set, only to those that happen to be total. But at the same time the clause does not require us to prove that the function is total, it just has to be total. This sort of "restricted" clause appears in many other inductive definitions that are used in mathematical logic.
Another kind of example is in the inductive definition of the closure $C$ of a set $X$ in a metric space:


*

*Every point of $X$ is in $C$

*If there is a sequence of points in $C$ converging to a point $z$ then $z$ is in $C$


This is again a sound inductive definition. But it is not obvious even how we would come up with a set of terms for all the points of an arbitrary metric space in order to start trying to worry about whether a formal system is able to prove that some point is in the closure of a set. 
