PHIL 250: Introduction to Symbolic Logic

tennant.9@osu.edu

---

Choose Destination My web-page Teaching PHIL 250 PHIL 650 Basic concepts and techniques Truth tables Universal-Introduction Universal-Elimination Existential-Introduction Existential-Elimination Negation-Introduction Negation-Elimination Conjunction-Introduction Conjunction-Elimination Disjunction-Introduction Disjunction-Elimination Conditional-Introduction Conditional-Elimination Absurdity rule Classical reductio Double negation elimination Law of Excluded Middle Dilemma

---

ELIMINATION RULE FOR THE UNIVERSAL QUANTIFIER (∀E)

---

∀xF(x)

_________

F(t)

Explanation in words: One is permitted to infer from a universally generalized premiss ∀xF(x) any instance F(t). By taking the indicated step of universal elimination, one thereby rests the conclusion F(t) on the same assumptions on which the universally generalized premiss ∀xF(x) above the line rested.

An instance F(t) is obtained by taking for t any (denoting) term, and substituting it for every free occurrence of the variable x in the formula F(x). In `logically perfect' languages, for which it is assumed (in the `background') that every term denotes, the rule is uncomplicated, as above. But in languages in which this background assumption is not made, one can require a further existential premiss ∃x(x=t) (often abbreviated as ∃!t) alongside the major premiss ∀xF(x).

Compare the corresponding introduction rule for ∀

---

[¬I] [∧I] [∨I] [→I] [∀I] [∃I]
[¬E] [∧E] [∨E] [→E] [∀E] [∃E]
[EFQ]
[LEM] [Dil] [CR] [DNE]

---