Examples from Kleene's Introduction to Metamathematics [1952] : Intro- and Elimination-rules Following Prof.Mummert suggestion about the correct application of Intro- and Elimination- rules for quantifiers [pag.98-99]:

look at examples 5 and 6 on page 149 of Kleene 1952.

Example 5. Given $A(x) \vdash B$ and $A(x) \vdash \lnot B$ with x held constant, then $\vdash \lnot A(x)$ and $\vdash \forall x \lnot A(x)$. Supply the formal details.
1) $A(x) \vdash B$
2) $A(x) \vdash \lnot B$
applying ($\lnot-I$) [i.e. if $\Gamma, A \vdash B$ and $\Gamma,A \vdash \lnot B$ then $\Gamma \vdash \lnot A$ with $\Gamma = \emptyset$ ] to 1 and 2 :
3) $\vdash \lnot A(x)$
then apply ($\forall$-I) to 3 :
4) $\vdash \forall \lnot xA(x)$.
Another proof :
1) $A(x) \vdash B$
2) $\vdash A(x) \rightarrow B$ --- from 1,($\rightarrow$-I)
3) $A(x) \vdash \lnot B$
4) $\vdash A(x) \rightarrow \lnot B$ --- from 3,($\rightarrow$-I)
5) $\vdash (A \rightarrow B) \rightarrow (A \rightarrow \lnot B) \rightarrow \lnot A$ --- Axiom 7
7) $\vdash \lnot A(x)$ --- from 2,5 and 4,6 with two applications of ($\rightarrow$-E)
8) $\vdash \forall \lnot xA(x)$ --- from 7,($\forall$-I).
Example 6. Given $A(x) \vdash^x B$ and $A(x) \vdash^x \lnot B$ with x not necessarly held constant, then $\vdash \lnot \forall x A(x)$. Supply the formal details.
 A: Example 6 is stated in term of $\vdash^x$.
Following the "intuitive meaning" of this relation, we would have :
from 1) $\forall xA(x) \vdash B$ --- with ($\rightarrow$-I)
and 2) $\forall xA(x) \vdash \lnot B$ --- with ($\rightarrow$-I)
and using Axiom 7 : $\vdash (A \rightarrow B) \rightarrow (A \rightarrow \lnot B) \rightarrow \lnot A$
3) $\vdash \lnot \forall xA(x)$ --- with two applications of ($\rightarrow$-E).
But in Kleene's system we have no formal rule that licenses "from $A(x) \vdash^x B$ to $\forall xA(x) \vdash B$".
The correct solution is :
1) $A(x) \vdash^x B$
2) $\forall xA(x)$ --- Assumption
3) $A(x)$ --- from 2, ($\forall$-E)
now, having derived $A(x)$, using the properties of $\vdash$ [rif pag.89] :
4) $\forall xA(x) \vdash^x B$
5) $\vdash \forall xA(x) \rightarrow B$ --- from 4, ($\rightarrow$)-I
6) $A(x) \vdash^x \lnot B$
in the same way :
10) $\vdash \forall xA(x) \rightarrow \lnot B$
now, from 5,10 and Axiom 7 :
12) $\vdash \lnot \forall xA(x)$ --- two applications of ($\rightarrow$)-E.
