6.3 First-order inference rules

The following are in addition to those of propositional logic .

As usual, we use $$ as a meta-variable to range over first-order WFFs. Similarly, $t$ is a meta-variable for first-order terms, and $c$ is a meta-variable for domain constants.The notation $\text{[}vw\text{]}$ means the formula $$ but with every appropriate occurrence of $v$ replaced by $w$ .

As discussed in the lecture notes , a variable is arbitrary unless :

• A variable is not arbitrary if it is free in (an enclosing) premise.
• A variable is not arbitrary if it is free after applying $$ Elimeither as the introduced witness $c$ , or free anywhere else in the formula.

As a detail in $$ Elim and $$ Intro, the term $t$ must be free to replace the variable $x$ in $$ . This means that it is not the case that both $t$ contains a variable quantified in $$ , and that $x$ occurs free within that quantifier. In short, the bound variable names should be kept distinct from the free variable names.Also, only free occurrences $x$ get replaced. The restriction in $$ Elim on $c$ being new is similar.