Correct interpretation of Kleene (Intro to Metamathematics) symbol $\vdash^x$ in Predicate Calculus

Question

Rif. S.C.Kleene, IM (1952) : which is the correct interpretation (or the "modern equivalent") of the "x" used as exponent of the "turnstile" as in:

$$A(x) \vdash^x \forall xA(x)$$

[see Derived Rules (Th.2, pag.98)] ?

Is it similar to Principia Mathematica usage of → (original "horseshoe") with "x" subscripted to indicate universally quantified variables ?

If so, the "implicit" universal quantifier has as his scope the Assumption only or all the context of the proof ?

There are some related examples at pag.149 [Examples 2 to 4]. I think that they are Kleene's version of similar examples of wrong application of quantifier rules in Nat Deduction.

$$x=0$$ (Assumption)

$$\forall xx=0$$ ($\forall$-Intro, illegal)

$$x=0 → \forall xx=0$$ (→Intro, discharging the Assumption)

$$\forall x(x=0 → \forall xx=0)$$ ($\forall$-Intro: at this step the Ass has been discharged)

$$0=0 → \forall xx=0 $$ ($\forall$-Elim).

The first occurrence of forall-Intro is illegal, because the assumption x=0 depends on itself.

Answer 1

There's some text on it, right above, and in, Theorem 2:

The variable "x" written as superscript on the symbol "$\vdash$" in two of the rules is to mark the application of Rule 9 or 12 with respect to x in constructing the resulting deduction.

---

For the predicate calculus (or full number-theoretic system), all the rules hold, provided that in each subsidiary deduction the free variables are held constant for the assumption formula to be discharged.

Where "Rule 9 and 12" come from p.82:

$$\begin{align} 9.&&\frac{C\supset A(x)}{C\supset \forall x A(x).}\\ 12.&&\frac{A(x) \supset C}{\exists x A(x) \supset C.} \end{align}$$

---

Now, what does this mean? The $\vdash^x$ notation basically conveys that $x$ is no longer allowed to occur in any "discharged assumption" (introduced on p.94). As such, it is not but the counterpart of the "freeness" condition that is present in rules 9 and 12.

It would therefore seem that the scope of the implicit universal quantification is the collection of all assumptions done in the proof (in that every assumption is implicitly quantified over $x$, whether or not this makes any difference or not).

(But the language is convoluted, so I'm not entirely certain.)