more from this thinker     |     more from this text


Single Idea 13901

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

Full Idea

In predicate calculus we take over the propositional connectives and propositional variables - but we need additional rules for handling quantifiers: four rules, an introduction and elimination rule for the universal and existential quantifiers.

Gist of Idea

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

Source

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

Book Ref

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


A Reaction

This is Lemmon's natural deduction approach (invented by Gentzen), which is largely built on introduction and elimination rules.


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

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]