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

- All the steps for propositional logic are allowed.
- Reflexivity: if $t$ is any term, then you may write down $(t=t)$.
- Symmetry: if $t,s$ are any terms and $(t=s)$ has been written down and is in scope then you may write down $(s=t)$.
- Transitivity: if $t,s,r$ are any terms and both $(t=s)$ and $(s=r)$ have been written down and are in scope then you may write down $(t=r)$.
- Substitution: given terms ${t}_{1},\dots ,{t}_{k},{s}_{1},\dots ,{s}_{k}$ variables ${v}_{1},\dots ,{v}_{k}$, and a formula $\theta $, let $S:\left\{{v}_{1},\dots ,{v}_{k}\right\}\to {\mathrm{TERM}}_{L}$ be the substition ${v}_{i}\mapsto {s}_{i}$, and $T:\left\{{v}_{1},\dots ,{v}_{k}\right\}\to {\mathrm{TERM}}_{L}$ be the substition ${v}_{i}\mapsto {t}_{i}$ and suppose $S\left(\theta \right),T\left(\theta \right)$ are both valid. Then if all of $({t}_{1}={s}_{1})$, $({t}_{2}={s}_{2})$, $\dots $, $({t}_{k}={s}_{k})$, and $T\left(\theta \right)$ have been written down are are in scope then you may write down $S\left(\theta \right)$.
- ∃-Elimination: given $\varphi ,\sigma $ and variables $u,v$, supppose $u$ does not occur free in $\sigma $,$\varphi $, nor in any formula which has already been written down and is in scope, and suppose the statement $v\varphi $ has been written down and is in scope. Suppose further that the substitution $S\left(\varphi \right)$ is valid where $S:v\mapsto u$ has $dom\left(S\right)=\left\{v\right\}$, and in a subproof you may write down $\sigma $ from additional assumption $S\left(\varphi \right)$; then you may also write down $\sigma $ immediately after this subproof.
- ∃-Introduction: given $\varphi $, a variable $v$ and a term $t$, let the substitution $S$ be $S:v\mapsto t$ with $dom\left(S\right)=\left\{v\right\}$, and $S\left(\varphi \right)$ is valid, then if $S\left(\varphi \right)$ has already been written down and is in scope, then you may write down $v\varphi $.
- ∀-Elimination: given $\varphi $, a variable $v$ and a term $t$, let the substitution $S$ be $S:v\mapsto t$ with $dom\left(S\right)=\left\{v\right\}$, and $S\left(\varphi \right)$ is valid, then if $\forall v\varphi $ has already been written down and is in scope, then you may write down $S\left(\varphi \right)$.
- ∀-Introduction: given $\varphi $ and variables $u,v$, if $u$ does not occur free in any formula in ${\Sigma}_{0}$ and the substitution $S\left(\varphi \right)$ is valid where $S:v\mapsto u$ has $dom\left(S\right)=\left\{v\right\}$, then if in a subproof with no additional assumption you may deduce $S\left(\varphi \right)$ then you may write down $\forall v\varphi $ immediately after the subproof.

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

- All the steps for propositional logic given on an previous web page are allowed.
- Reflexivity: if $t$ is any term, then the step $\frac{\text{}}{{\Sigma}_{0}\u22a2(t=t)}$ is allowed.
- Symmetry: if $t,s$ are any terms, then the step $\frac{{\Sigma}_{0}\u22a2(t=s)}{{\Sigma}_{0}\u22a2(s=t)}$ is allowed.
- Transitivity: if $t,s,r$ are any terms, then the step $\frac{{\Sigma}_{0}\u22a2(t=s){\Sigma}_{0}\u22a2(s=r)}{{\Sigma}_{0}\u22a2(t=r)}$ is allowed.
- Substitution: given terms ${t}_{1},\dots ,{t}_{k},{s}_{1},\dots ,{s}_{k}$ variables ${v}_{1},\dots ,{v}_{k}$, and a formula $\theta $, let $S:{\left\{v\right\}}_{1},\dots ,{v}_{k}\to {\mathrm{TERM}}_{L}$ be the substition ${v}_{i}\mapsto {s}_{i}$, and $T:{\left\{v\right\}}_{1},\dots ,{v}_{k}\to {\mathrm{TERM}}_{L}$ be the substition ${v}_{i}\mapsto {t}_{i}$. Then the step $\frac{{\Sigma}_{0}\u22a2({t}_{1}={s}_{1}){\Sigma}_{0}\u22a2({t}_{2}={s}_{2})\dots {\Sigma}_{0}\u22a2({t}_{k}={s}_{k}){\Sigma}_{0}\u22a2T\left(\theta \right)}{{\Sigma}_{0}\u22a2S\left(\theta \right)}$ is allowed, provided these substitutions are valid.
- ∃-Elimination: given ${\Sigma}_{0},\varphi ,\sigma $ and variables $u,v$, if $u$ does not occur free in $\sigma $, $\varphi $, nor in any formula in ${\Sigma}_{0}$ and the substitution $S\left(\varphi \right)$ is valid where $S:v\mapsto u$ has $dom\left(S\right)=\left\{v\right\}$, then the step $\frac{{\Sigma}_{0},S\left(\varphi \right)\u22a2\sigma}{{\Sigma}_{0},v\varphi \u22a2\sigma}$ is allowed.
- ∃-Introduction: given ${\Sigma}_{0},\varphi $, a variable $v$ and a term $t$, let the substitution $S$ be $S:v\mapsto t$ with $dom\left(S\right)=\left\{v\right\}$, and $S\left(\varphi \right)$ valid, then the step $\frac{{\Sigma}_{0}\u22a2S\left(\varphi \right)}{{\Sigma}_{0}\u22a2v\varphi}$ is allowed.
- ∀-Elimination: given ${\Sigma}_{0},\varphi $, a variable $v$ and a term $t$, let the substitution $S$ be $S:v\mapsto t$ with $dom\left(S\right)=\left\{v\right\}$ and $S\left(\varphi \right)$ valid, then the step $\frac{{\Sigma}_{0}\u22a2\forall v\varphi}{{\Sigma}_{0}\u22a2S\left(\varphi \right)}$ is allowed.
- ∀-Introduction: given ${\Sigma}_{0},\varphi $ and variables $u,v$, if $u$ does not occur free in any formula in ${\Sigma}_{0}$ and the substitution $S\left(\varphi \right)$ is valid where $S:v\mapsto u$ has $dom\left(S\right)=\left\{v\right\}$, then the step $\frac{{\Sigma}_{0}\u22a2S\left(\varphi \right)}{{\Sigma}_{0}\u22a2\forall v\varphi}$ is allowed.

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.