The following are in addition to those of Propositional inference rules.
|
Abbreviation |
Name |
If you know all of. . . |
. . .then you can infer |
|
∀Intro |
∀-introduction |
φ |
∀x.φ[y→x] |
|
y arbitrary (p. 99). |
|||
|
∀Elim |
∀-elimination |
∀x.φ |
φ[x→t] |
|
t is any term that is free to be replaced in φ. |
|||
|
Domain non-empty. |
|||
|
∃Intro |
∃-introduction |
φ |
∃x.φ[t→x] , where t is arbitrary |
|
t is any term in φ that is free to be replaced. |
|||
|
Domain non-empty. |
|||
|
∃Elim |
∃-elimination |
∃x.φ |
φ[x→c] |
|
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 φ[v→w] 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.
- 1662 reads
