structure for 'Formal Logic'    |     alphabetical list of themes    |     expand these ideas

4. Formal Logic / C. Predicate Calculus PC / 2. Tools of Predicate Calculus / c. Derivations rules of PC

[normal rules used in predicate logic reasoning]

6 ideas
If you pick an arbitrary triangle, things proved of it are true of all triangles [Euclid, by Lemmon]
Predicate logic uses propositional connectives and variables, plus new introduction and elimination rules [Lemmon]
Universal elimination if you start with the universal, introduction if you want to end with it [Lemmon]
Universal Elimination (UE) lets us infer that an object has F, from all things having F [Lemmon]
With finite named objects, we can generalise with &-Intro, but otherwise we need ∀-Intro [Lemmon]
UE all-to-one; UI one-to-all; EI arbitrary-to-one; EE proof-to-one [Lemmon]