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

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 $θ$ , let $S : \{v_{1} \dots v_{k}\} \to {TERM}_{L}$ be the substition $v_{i} \mapsto s_{i}$ , and $T : \{v_{1} \dots v_{k}\} \to {TERM}_{L}$ be the substition $v_{i} \mapsto t_{i}$ and suppose $S (θ), T (θ)$ are both valid. Then if all of $(t_{1} = s_{1})$ , $(t_{2} = s_{2})$ , $\dots$ , $(t_{k} = s_{k})$ , and $T (θ)$ have been written down are are in scope then you may write down $S (θ)$ .
∃-Elimination: given $ϕ, σ$ and variables $u, v$ , supppose $u$ does not occur free in $σ$ , $ϕ$ , nor in any formula which has already been written down and is in scope, and suppose the statement $v ϕ$ has been written down and is in scope. Suppose further that the substitution $S (ϕ)$ is valid where $S : v \mapsto u$ has $dom (S) = \{v\}$ , and in a subproof you may write down $σ$ from additional assumption $S (ϕ)$ ; then you may also write down $σ$ immediately after this subproof.
∃-Introduction: given $ϕ$ , a variable $v$ and a term $t$ , let the substitution $S$ be $S : v \mapsto t$ with $dom (S) = \{v\}$ , and $S (ϕ)$ is valid, then if $S (ϕ)$ has already been written down and is in scope, then you may write down $v ϕ$ .
∀-Elimination: given $ϕ$ , a variable $v$ and a term $t$ , let the substitution $S$ be $S : v \mapsto t$ with $dom (S) = \{v\}$ , and $S (ϕ)$ is valid, then if $\forall v ϕ$ has already been written down and is in scope, then you may write down $S (ϕ)$ .
∀-Introduction: given $ϕ$ and variables $u, v$ , if $u$ does not occur free in any formula in $Σ_{0}$ and the substitution $S (ϕ)$ is valid where $S : v \mapsto u$ has $dom (S) = \{v\}$ , then if in a subproof with no additional assumption you may deduce $S (ϕ)$ then you may write down $\forall v ϕ$ immediately after the subproof.

3. Proof rules for proofs-as-trees

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{}{Σ_{0} ⊢ (t = t)}$ is allowed.
Symmetry: if $t, s$ are any terms, then the step $\frac{Σ_{0} ⊢ (t = s)}{Σ_{0} ⊢ (s = t)}$ is allowed.
Transitivity: if $t, s, r$ are any terms, then the step $\frac{Σ_{0} ⊢ (t = s) Σ_{0} ⊢ (s = r)}{Σ_{0} ⊢ (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 $θ$ , let $S : {\{v\}}_{1}, \dots, v_{k} \to {TERM}_{L}$ be the substition $v_{i} \mapsto s_{i}$ , and $T : {\{v\}}_{1}, \dots, v_{k} \to {TERM}_{L}$ be the substition $v_{i} \mapsto t_{i}$ . Then the step $\frac{Σ_{0} ⊢ (t_{1} = s_{1}) Σ_{0} ⊢ (t_{2} = s_{2}) \dots Σ_{0} ⊢ (t_{k} = s_{k}) Σ_{0} ⊢ T (θ)}{Σ_{0} ⊢ S (θ)}$ is allowed, provided these substitutions are valid.
∃-Elimination: given $Σ_{0}, ϕ, σ$ and variables $u, v$ , if $u$ does not occur free in $σ$ , $ϕ$ , nor in any formula in $Σ_{0}$ and the substitution $S (ϕ)$ is valid where $S : v \mapsto u$ has $dom (S) = \{v\}$ , then the step $\frac{Σ_{0}, S (ϕ) ⊢ σ}{Σ_{0}, v ϕ ⊢ σ}$ is allowed.
∃-Introduction: given $Σ_{0}, ϕ$ , a variable $v$ and a term $t$ , let the substitution $S$ be $S : v \mapsto t$ with $dom (S) = \{v\}$ , and $S (ϕ)$ valid, then the step $\frac{Σ_{0} ⊢ S (ϕ)}{Σ_{0} ⊢ v ϕ}$ is allowed.
∀-Elimination: given $Σ_{0}, ϕ$ , a variable $v$ and a term $t$ , let the substitution $S$ be $S : v \mapsto t$ with $dom (S) = \{v\}$ and $S (ϕ)$ valid, then the step $\frac{Σ_{0} ⊢ \forall v ϕ}{Σ_{0} ⊢ S (ϕ)}$ is allowed.
∀-Introduction: given $Σ_{0}, ϕ$ and variables $u, v$ , if $u$ does not occur free in any formula in $Σ_{0}$ and the substitution $S (ϕ)$ is valid where $S : v \mapsto u$ has $dom (S) = \{v\}$ , then the step $\frac{Σ_{0} ⊢ S (ϕ)}{Σ_{0} ⊢ \forall v ϕ}$ is allowed.

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.