Reference: first-order inference rules 2.18 2003/02/11 2006/02/09 14:41:06.218 US/Central John Greiner greiner@cs.rice.edu Phokion Kolaitis kolaitis@cse.ucsc.edu Moshe Vardi vardi@cs.rice.edu Matthias Felleisen matthias@ccs.neu.edu Ian Barland ian@cs.rice.edu John Greiner greiner@cs.rice.edu Inference rules for reasoning about first-order logic formulas. The following are in addition to those of propositional logic. Our first-order inference rules Abbreviation Name If you know all of… …then you can infer ∀Intro ∀-introduction φ y arbitrary. ∀x. φ[y↦x] ∀Elim ∀-elimination ∀x. φ t is any term that is free to be replaced in φ. Domain non-empty. φ [x↦t] ∃Intro ∃-introduction φ t is any term in φ that is free to be replaced. Domain non-empty. ∃x. φ[t↦x] , where t is arbitrary ∃Elim ∃-elimination ∃x. φ c is a new constant in the proof. c does not occur in the proof's conclusion. φ [x↦c] 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 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 (w/o 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 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.