Theory of definitions

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.