A problem with the Gen-rule in Kleene's Mathematical Logic
I refer to Stephen Cole Kleene, Mathematical Logic (1967 - Dover reprint : 2002).
At pag.118 he introduces the Derived Rules for quantifiers in Predicate Calculus, beginning with $\forall$-intro : if $\Gamma\vdash A(x)$ then $\Gamma\vdash \forall x A(x)$ , provided that x is not free in $\Gamma$.
At pag.119 he comments on the necessity of the proviso:
Except for this proviso, Example 13.3 [pag.58] would apply and give $"A(x)\vdash\forall xA(x)"$. That however does not hold; for then [...] we would have $"A(x) ⊨ \forall xA(x)"$; and this is not the case.
But in Intro to Metamathematics [1952] Kleene uses as Derived Rule a $\forall$-intro in the form : $"A(x) / \forall xA(x)"$.
Why this does not cause him troubles in IM ?
Solution 1:
First, a disclaimer. The key point to keep in mind is that Kleene 1952 was written by Kleene. Like much of his other writing, it is full of information and very carefully presented, but it requires substantial effort to unpack the information from its dense and formalistic arrangement. In particular, Kleene 1952 is written in the "classic" style which intends for the book to be read continuously from the beginning, rather than a more "modern" style in which the author expects the reader may randomly start reading at the statement of a theorem. At this point in time, I would view the study of Kleene 1952 are more about the history of mathematics, because modern presentations are more clear and use current terminology. Anyone who does want to learn from Kleene's books should expect the need to start on page 1 and work in a continuous way through the book, rather than trying to jump to particular theorems or compare Kleene directly to modern books.
With that said:
In general, there is always an issue with the relationship between $A(x)$ and $(\forall x) A(x)$ in first order logic. The real issue is how to understand the use of $A(x)$ as an assumption when $x$ is free in $A$. There are two approaches, using Kleene's terminology (Kleene 1952 p. 148, "Interpetation of formulas with free variables"; Kleene 1967 pp. 103-105):
The generality interpretation: assuming $A(x)$ is the same as assuming $(\forall x)A(x)$. This is the approach that Kleene takes in 1952.
The conditional interpretation: the axiom $A(x)$ merely means that some $x$ satisfies $A$, not that all $x$ do. For example, this is the approach used by Enderton, A Mathematical Introduction to Logic, 2001, and it is the approach Kleene emphasized more in 1967.
When an author sets up a deduction system for first-order logic, there are three interrelated theorems:
The soundness and completeness theorem: If $\phi \models \psi$ if and only if $\phi \vdash \psi$
The deduction theorem (which is also the $\to$ introduction rule): If $\phi \vdash \psi$ then $\vdash \phi \to \psi$
The $\forall$ introduction rule: $\phi \vdash (\forall x)\phi$
These are correct without further hypotheses when $\phi$ and $\psi$ are sentences, but when they may have free variables there are several approaches, which add various restrictions to (1), (2), and (3). The exact restrictions will depend very much on whether the author wants to use the generality interpretation or the conditional interpretation. One author may restrict the statement of (1), while another may restrict (2) or (3).
For example, Enderton 2001 (page 117) states the deduction theorem in a very restricted way:
If $\Gamma \vdash \phi$ and $x$ does not occur free in any formula of $\Gamma$, then $\Gamma \vdash (\forall x)\phi$
In his 1967 book, Kleene sticks closer to the conditional interpretation; in his 1952 book, he sticks closer to the generality interpretation. But, in each case, he spends time explaining that there is a difference. From my perspective, it appears that Kleene did not seem to want to commit to either one, because he saw both as useful reflections of techniques in natural-language reasoning.
The distinction between the generality interpretation and the conditional interpretation pervades the entire literature on first-order logic. For example, books on model theory often seem to assume the conditional interpretation without comment, while books on universal algebra often seem to assume the generality interpretation without comment. To proceed formally it is necessary to take the entire deductive apparatus (results 1, 2, and 3 above) from a single book, rather than trying to splice together results from books that may take incompatible approaches. I believe that this is the reason for the disparity of results in the question: they are taken from different books that do not make the same choices about how to set up the deductive system.
As to the notation $\phi \vDash^x \psi$, Kleene 1967 defines it on page 106: basically, $\phi \vDash^x \psi$ means that $(\forall x)\phi \vDash \psi$ in the usual sense.
Solution 2:
$\forall$-introduction means 'if $\vdash A(x)$ then $\vdash \forall A(x)$' (that is, if you prove $A(x)$ without any assumption, then $\forall x A(x)$ is a theorem.) It is not equivalent to $A(x)\vdash \forall x A(x)$.
I think $A(x)/\forall x A(x)$ exactly means $$ \begin{array}{c} \vdash A(x)\\ \overline{\vdash\forall x A(x)} \end{array} $$
But I do not read this book so I do not certain it.