I am reading A Friendly Introduction to Mathematical Logic by Christopher Leary and Lars Kristiansen. The authors define **rules of inference of type (QR)**:

**Definition.** Suppose that the variable $x$ is not free in the formula $psi$. Then both of the following are **rules of inference of type (QR)**:

$$left( { psi to phi }, psi to left( forall xphi right) right)$$

$$left( { phi to psi }, left( exists xphiright) to psi right)$$

The authors write the following as a motivation which is intuitive but I cannot seem to relate the motivation and the definition:

The motivation behind our quantifier rules is very simple. Suppose, without

making any particular assumptions about x, that you were able to prove

“x is an ambitious aardvark.” Then it seems reasonable to claim that you

have proved “(∀x)x is an ambitious aardvark.” Dually, if you were able

to prove the Riemann Hypothesis from the assumption that “x is a bossy

bullfrog,” then from the assumption “(∃x)x is a bossy bullfrog,” you should

still be able to prove the Riemann Hypothesis.

This is intuitive but how does all this motivate the definition? Also, can someone explain the requirement of $x$ not being free in $psi$ in the definition?