This web page gives the official rigorous definition of the proof rules for first order logic. In particular it uses the syntactical substitution defined earlier to make precide the official proof rules of first order logic. It also relies on an earlier discussion of how to write a proof - either as a tree or as a structured list of statements. This makes precise the rules given in Definition 9.8 on page 122 of The Mathematics of Logic.
In the style of writing proofs as structured lists of formulas and subproofs, the official rules of first-order logic are
In the style of proof-trees (which some readers may prefer) these rules become
It is important to note that, whatever scheme is preferred, these proof rules are computable. That is, a computer program could be written to check that each step in a proof is valid according to the rules.