Substitution and the rules for first order logic

1. Introduction

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.

2. Proof rules for proofs-as-structured-lists

In the style of writing proofs as structured lists of formulas and subproofs, the official rules of first-order logic are

3. Proof rules for proofs-as-trees

In the style of proof-trees (which some readers may prefer) these rules become

4. Remarks

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.