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.