You are here

First-order inference rule

26 July, 2019 - 12:03
Available under Creative Commons-ShareAlike 4.0 International License. Download for free at

The following are in addition to those of Propositional inference rules.

Table 6.4 Our first-order inference rules



If you know all of. . .

. . .then you can infer





y arbitrary (p. 99).





t is any term that is free to be replaced in φ.

Domain non-empty.




x.φ[tx] , where t is arbitrary

t is any term in φ that is free to be replaced.

Domain non-empty.





c is a new constant in the proof.

c does not occur in the proof's conclusion.


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 φ[vw] means the formula φ but with every appropriate (Note, p. 99) 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 ∃Elim either as the introduced witness c, or free anywhere else in the formula.

The usual way to introduce arbitrary variables is during ∀Elim (wjo later using it in ∃Elim).

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 quantifed in φ, and that x occurs free within that quantifer. 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.