Theory of definitions I am reading "Introduction to Logic" by P Suppes at the moment. In the Chapter 8 - Theory of definitions of it, I 've some confusion, actually about the Conditional Definition. The brief explanation is also given in the book "Axiomatic Set Theory" by the same author. 
Suppes tells - A definition must follow Criteria of Eliminability and Criteria of Non-Creativity. In the book He also writes that it is the classical problem to provide restrictions to definitions such that it follow these two criteria. (You can find more details in the book .. - Google Books..) Here I'm confused in the matter of Conditional Definitions.
RULES FOR CONDITIONAL DEFINITIONS OF OPERATION SYMBOLS. An
implication $C$ introducing a new operation symbol $O$ is a conditional
definition in a theory if and only if $C$ is of the form 

$H \Longrightarrow [O(v_1, v_2, ... , v_n)=w \Longleftrightarrow S]$

.and the following restrictions are satisfied: (i) the variable $w$ is not free
in $H$, (ii) the variables $v_1, v_2,... , v_n, w$ are distinct, (iii) $S$ has no free
variables other than $v_1, v_2, ... , v_n, w$, (iv) $S$ and $H$ are formulas in which
the only non-logical constants are primitive symbols and previously defined
symbols of the theory, and (v) the formula $H \Longrightarrow (\exists!w)S$ is derivable from
the. axioms and preceding definitions of the theory.
Here The reason behind last four restrictions are well explained in the book, though not directly. But What is the reason behind the first restriction. Why is $w$ is bounded in $H$. What if it is free in $H$ ? Help me.
 A: Informally, we can say that the correct interpretation is in the management of "implicit" quantifiers.
Consider the example regarding the definition of the operation symbol $|$ ("division") :

$v_2 \ne 0 \rightarrow (v_1|v_2 = w \leftrightarrow v_1=v_2 w)$

provided that we have : $v_2 \ne 0 \rightarrow \exists ! w (v_1=v_2 w)$.
This must be read as "fully" quantified :

(*) $ \ \forall v_1 \forall v_2 \exists w [v_2 \ne 0 \rightarrow (v_1|v_2 = w \leftrightarrow v_1=v_2 w)]$.

We have that :

$\vdash ∃w(α → β) ↔ (α → ∃wβ)$, provided that $w \notin FV(\alpha)$.

Thus, we can use it to "rewrite (*) as :

$\forall v_1 \forall v_2 [v_2 \ne 0 \rightarrow \exists w (v_1|v_2 = w \leftrightarrow v_1=v_2 w)]$.

See the formal proof in :


*

*George Tourlakis, Lectures in Logic and Set Theory. Volume 1 : Mathematical Logic (2003), page 116.



The proviso : $w$ not free in $H$ is related to the necessity of avoiding a fallacy.
Consider an example regarding the natural numbers and consider the "silly" formula :

$w > 0 \rightarrow w < 0$.

If we interpret it into the domain $\mathbb N$ of natural numbers, we have that $0 > 0 \rightarrow 0 < 0$ is true (because f $\rightarrow$ f is t), and thus in $\mathbb N$ we have that the formula :

$\exists w(w>0 \rightarrow w<0)$ 

is (useless but) true.
The fallacy arises if we apply the above equivalence : $\vdash ∃w(α → β) ↔ (α → ∃wβ)$ disregarding the proviso : $w$ not free in $\alpha$.
Now the new formula is :

$w>0 \rightarrow \exists w(w<0)$ 

and it is not true in $\mathbb N$. 
For sure $\exists w(w<0)$ is false, but we can assign to the free variable $w$ in the antecedent the value $1$, and $1 > 0$ is true : thus (t $\rightarrow$ f is f), we have derived incorrectly a false conclusion from a true premise.
Conclusion : the proviso : $w$ not free in $H$ is needed.
