"Reaching an obvious truth" (such as $p\to p$ ro $1=1$) is a valif method of proof if the steps used in reaching this obvious truth are equivalence transforms. That is, if your argument goes like
$A_1$ is equivalent to $A_2$, which is equivalent to $A_3$, $\ldots$, which is equivalent to $A_n$, which is a tautology
then you have proved $A_1$. However, you must be careful that not a single "is equivalent" step turns out to be only an "implies" step.
On the other hand, we do not even need equivalence, we only need one direction - the backward one. Therefore it is often better to write up a proof in the other direction:
We have the tautology $A_n$. This implies $A_{n-1}$. $\ldots$ This implies $A_3$. This implies $A_2$. This implies $A_1$, as desired.
The "from $A_1$ to $A_n$" method may be best suited for discovering a proof, but "from $A_n$ to $A_1$" (which may then be a direct proof) is best suited for presenting a proof (and at the same time to discover gaps in the proof because it becomes easier to spot steps that fail to be equivalences).
The ruleset given by the book is not incomplete. The example derivation you give holds up to scrutiny as well. You get (seemingly) paradoxical conclusions because restriction (iv) does not actually hold in any of your examples.
In your first example, the formula $S$ denotes the following: "$v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2$". So restriction (iv) is not satisfied unless the following is a theorem of the theory under consideration:
$$\exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
which, since $v_1,v_2$ are distinct free variables, holds precisely if
$$\forall v_1. \forall v_2. \exists! w. v_2 \text{ is a function } \wedge \langle v_1,w \rangle \in v_2 $$
is a theorem of your theory as well. Needless to say, this latter statement is very much not a theorem of any reasonable set theory. In particular it would imply "$\forall v. v \text{ is a function }$" by itself.
In your second example, the formula $S$ denotes the following: "$\text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w)$". As above, restriction (iv) is not satisfied unless the following is a theorem of the theory under consideration:
$$ \forall v_1. \forall v_2. \exists! w. \text{isAdult}(v_1) \wedge \text{isAdult}(v_2) \wedge \text{parentsOf}(v_1,v_2,w) \wedge \text{isSingleChild}(w) $$
But if the sentence given above is a theorem of your theory, then you can already prove (directly, starting from the sentence above as a premise, and using $\forall E$, $\wedge E$ and $\forall I$) that $\forall v_1. \text{isAdult}(v_1)$ is a theorem of your theory.
Best Answer
It's not a very clear-cut line. There's also a complication, because mathematicians often use certain styles of language in a formal proof, making the proof sound more formal-in-the-colloquial-English-sense. They do this to signal "this is a formal-in-your-sense proof". The converse is also true.
Here's an informal intensional definition:
(The definition of "nothing" is flexible, depending on the level of the proof. A formal proof aimed at world-class mathematicians may miss out more details than a first-year undergraduate formal proof, which is not allowed to miss out many details at all.)
One may use words whose meaning follows only from context, as long as it's clear what the meaning is; that's not hiding anything. A proof can skip out details and still be formal, as long as it tells you how to complete the details: that's hiding stuff but making it clear that the stuff is a) hidden, and b) easy to recover.
Here's an informal extensional definition.
A proof which leaves large chunks to the reader is informal: it hides large amounts of detail. A definition which misses out some annoying special cases (perhaps to make the statement more slick) is informal. A proof which pedantically goes over every statement is formal. A proof in which every statement clearly follows from earlier statements or from axioms/hypotheses is formal.