Some questions about presentation of First-Order Logic in a book by Raymond Smullyan I'm re-reading Raymond Smullyan, First Order-Logic (1968 - Dover reprint).
It's a wonderful booklet (I liked it very much), but a little bit terse.
It uses the distinction between individual variables (to be used "bound") and individual parameters (to be used "free") [pag.43].
Question 1) I think that this (now) uncommon usage dates back to Hilbert & Bernays' Grundlagen der Mathematik (1934) : is it true ?
The book uses concepts of f-o semantic quite similar to current "model theory" ones, like first order valuation; but, if I'm right, he do not introduce a concept of "logical consequence" (for f-o logic; he uses only truth-functional consequence - pag.12).
Question 2) Why this concept is missing ? It is also missing form J.L.Bell & A.B.Slomson, Models and Ultraproducts (1969): when "logical consequence" has become standard in textbooks exposition of f-o logic ?
He uses the concept of formula with constants in $U$ (or $U$-formulas), where $U$ is a non-empty set called universe of individuals [pag.46]. He substitute individuals for free variables [i.e.$F(k/x)$ for any $k \in U$].
Question 3) May we say that should be better to use names for individuals (like the numeral $\overline{n}$ for $n$) so that, for any $k \in U$, we can make the substitution $F(\overline{k}/x)$ ?
Thanks a lot.
 A: Ad qn 1: This usage, typographically distinguishing free variables (parameters) from bound variables is certainly also in Gentzen's doctoral thesis, published in 1934. I don't know which way round the influence, in any, was between  Bernays and his (nominal) student Gentzen here. The usage is inherited by Dag Prawitz's hugely influential Natural Deduction of 1965, and  the usage in fact then remains not uncommon in those whose logical work is more proof-theoretically orientated.
Ad qn 2 I don't think anything deep is going on here. Chap. 1 on prop. logic has already explored the relations between $A$'s being a logical consequence of the set $X$, the unsatisfiability of the set $X, \neg A$, (via compactness) the unsatisfiability of a finite subset of $X, \neg A$, and the deducibility of $A$ from $X$. Maybe Smullyan didn't think he needed to go through all this again in the first-order case: it is enough to talk about the (un)satisfiability of sets of wffs, compactness, and deducibility again. But yes, perhaps surprising not to define outright logical consequence for first-order wffs.
Ad qn 3 No we can't say that. The point is that the number of elements in the universe can outstrip the number of names -- for names (or terms more generally) are denumerable for Smullyan, but the elements of the universe U might be uncountable, so there are nameless elements.
