structure for 'Formal Logic'    |     alphabetical list of themes    |     unexpand 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]
     Full Idea: Euclid begins proofs about all triangles with 'let ABC be a triangle', but ABC is not a proper name. It names an arbitrarily selected triangle, and if that has a property, then we can conclude that all triangles have the property.
     From: report of Euclid (Elements of Geometry [c.290 BCE]) by E.J. Lemmon - Beginning Logic 3.2
     A reaction: Lemmon adds the proviso that there must be no hidden assumptions about the triangle we have selected. You must generalise the properties too. Pick a triangle, any triangle, say one with three angles of 60 degrees; now generalise from it.
Predicate logic uses propositional connectives and variables, plus new introduction and elimination rules [Lemmon]
     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.
     From: E.J. Lemmon (Beginning Logic [1965])
     A reaction: This is Lemmon's natural deduction approach (invented by Gentzen), which is largely built on introduction and elimination rules.
Universal elimination if you start with the universal, introduction if you want to end with it [Lemmon]
     Full Idea: The elimination rule for the universal quantifier concerns the use of a universal proposition as a premiss to establish some conclusion, whilst the introduction rule concerns what is required by way of a premiss for a universal proposition as conclusion.
     From: E.J. Lemmon (Beginning Logic [1965], 3.2)
     A reaction: So if you start with the universal, you need to eliminate it, and if you start without it you need to introduce it.
With finite named objects, we can generalise with &-Intro, but otherwise we need ∀-Intro [Lemmon]
     Full Idea: If there are just three objects and each has F, then by an extension of &I we are sure everything has F. This is of no avail, however, if our universe is infinitely large or if not all objects have names. We need a new device, Universal Introduction, UI.
     From: E.J. Lemmon (Beginning Logic [1965], 3.2)
Universal Elimination (UE) lets us infer that an object has F, from all things having F [Lemmon]
     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.
     From: E.J. Lemmon (Beginning Logic [1965], 3.2)
UE all-to-one; UI one-to-all; EI arbitrary-to-one; EE proof-to-one [Lemmon]
     Full Idea: Univ Elim UE - if everything is F, then something is F; Univ Intro UI - if an arbitrary thing is F, everything is F; Exist Intro EI - if an arbitrary thing is F, something is F; Exist Elim EE - if a proof needed an object, there is one.
     From: E.J. Lemmon (Beginning Logic [1965], 3.3)
     A reaction: [My summary of Lemmon's four main rules for predicate calculus] This is the natural deduction approach, of trying to present the logic entirely in terms of introduction and elimination rules. See Bostock on that.