more from this thinker     |     more from this text

---

Single Idea 13904

[filed under theme 4. Formal Logic / C. Predicate Calculus PC / 2. Tools of Predicate Calculus / c. Derivations rules of PC ]

Full Idea

Our rule of universal quantifier elimination (UE) lets us infer that any particular object has F from the premiss that all things have F. It is a natural extension of &E (and-elimination), as universal propositions generally affirm a complex conjunction.

Gist of Idea

Universal Elimination (UE) lets us infer that an object has F, from all things having F

Source

E.J. Lemmon (Beginning Logic [1965], 3.2)

Book Ref

Lemmon,E.J.: 'Beginning Logic' [Nelson 1979], p.105

---

The 6 ideas with the same theme [normal rules used in predicate logic reasoning]:

13907

If you pick an arbitrary triangle, things proved of it are true of all triangles [Euclid, by Lemmon]

13901

Predicate logic uses propositional connectives and variables, plus new introduction and elimination rules [Lemmon]

13903

Universal elimination if you start with the universal, introduction if you want to end with it [Lemmon]

13904

Universal Elimination (UE) lets us infer that an object has F, from all things having F [Lemmon]

13906

With finite named objects, we can generalise with &-Intro, but otherwise we need ∀-Intro [Lemmon]

13908

UE all-to-one; UI one-to-all; EI arbitrary-to-one; EE proof-to-one [Lemmon]