Can pure first-order logic be axiomatized by a recursive list of statements? If every line of a proof must be a statement and not simply a wff, does some recursive set of axioms entail all the statements valid in pure first-order logic? I am guessing a joke answer is “Yes, because the set of all statements valid in pure first-order logic is recursively enumerable, and a theorem of Craig says that there is a recursive axiomatization of any theory with a recursively enumerable axiomatization.” But I want a practical list of axioms I can actually write down.
I should note that I am asking this question because I am trying to sidestep a problem I am having understanding Endertonʼs notion of proof. Specifically, I genuinely do not know what it means for a wff that is not a statement to be an axiom or an intermediate line in a proof.
 A: This my first attempt to answer a question, so I'll do my best.
First of all, it is important to understand what a free variable in a formula stands for.
When we are talking about axioms (as Enderton does) we are talking about a set of formula that, by means of derivating rules, can give us new formulas. These axioms, however, are stated using metavariables. For example, $\varphi \rightarrow (\psi \rightarrow \chi) \rightarrow ((\varphi\rightarrow\psi) \rightarrow (\varphi\rightarrow\psi))$. These metavariables stand for other formulas that can be "plugged in" in order for you to have new instances of the same axiom.
When introducing the notion of proof, the idea is that any new formula is either derived by application of Modus ponens to an already derived formula, or an instance of the axiom or derived by use of any of the derivation rules. When saying that a wff that is not an statement is an axiom, you are instantiating one of the axioms, but plugging in variables which are not quantified. This, in principle, would not be a problem: you can operate with open formulas, however some caution is needed.
There is one axiom that tells that one can close a formula that has free variables by adding a universal quantificator for eachfree variable existing in the formula. Thus, if during your proof you get to a formula,say, $\vdash\varphi(x,y)$, where $x,y$ are free variables, then it is possible to close this formula by adding one universal quantificator for each variable in order of appearance, that is $\vdash\forall y \forall x \varphi(x,y)$. Hence, having a formula that is not a statement as an axiom or a line in a proof just means that there is an instance of a formula that has not yet closed.
