green numbers give full details.     |    back to list of philosophers     |     expand these ideas

### Ideas of E.J. Lemmon, by Text

#### [British, fl. 1960, Claremont College]

 1965 Beginning Logic
 p.104 13901 Predicate logic uses propositional connectives and variables, plus new introduction and elimination rules
 1.2 p.7 9511 We write the conditional 'if P (antecedent) then Q (consequent)' as P→Q
 1.2 p.7 9512 We write the 'negation' of P (not-P) as ¬
 1.2 p.11 9508 The sign |- may be read as 'therefore'
 1.3 p.19 9509 That proposition that both P and Q is their 'conjunction', written P∧Q
 1.3 p.19 9510 That proposition that either P or Q is their 'disjunction', written P∨Q
 1.4 p.29 9513 We write 'P if and only if Q' as P↔Q; it is also P iff Q, or (P→Q)∧(Q→P)
 1.5 p.34 9514 If A and B are 'interderivable' from one another we may write A -||- B
 1.5 p.39 9394 MPP: Given A and A→B, we may derive B
 1.5 p.39 9393 A: we may assume any proposition at any stage
 1.5 p.40 9398 ∧I: Given A and B, we may derive A∧B
 1.5 p.40 9402 RAA: If assuming A will prove B∧¬B, then derive ¬A
 1.5 p.40 9401 ∨E: Derive C from A∨B, if C can be derived both from A and from B
 1.5 p.40 9399 ∧E: Given A∧B, we may derive either A or B separately
 1.5 p.40 9397 CP: Given a proof of B from A as assumption, we may derive A→B
 1.5 p.40 9396 DN: Given A, we may derive ¬¬A
 1.5 p.40 9395 MTT: Given ¬B and A→B, we derive ¬A
 1.5 p.40 9400 ∨I: Given either A or B separately, we may derive A∨B
 2.1 p.44 9516 A 'well-formed formula' follows the rules for variables, ¬, →, ∧, ∨, and ↔
 2.1 p.47 9517 The 'scope' of a connective is the connective, the linked formulae, and the brackets
 2.2 p.50 9518 A 'theorem' is the conclusion of a provable sequent with zero assumptions
 2.2 p.53 9519 A 'substitution-instance' is a wff formed by consistent replacing variables with wffs
 2.2 p.60 9520 The paradoxes of material implication are P |- Q → P, and ¬P |- P → Q
 2.2 p.61 9522 'Modus ponendo tollens' (MPT) says P, ¬(P ∧ Q) |- ¬Q
 2.2 p.61 9521 'Modus tollendo ponens' (MTP) says ¬P, P ∨ Q |- Q
 2.2 p.62 9523 De Morgan's Laws make negated conjunctions/disjunctions into non-negated disjunctions/conjunctions
 2.2 p.62 9526 We can change conjunctions into negated conditionals with P→Q -||- ¬(P → ¬Q)
 2.2 p.62 9524 We can change conditionals into disjunctions with P→Q -||- ¬P ∨ Q
 2.2 p.62 9527 The Distributive Laws can rearrange a pair of conjunctions or disjunctions
 2.2 p.62 9525 We can change conditionals into negated conjunctions with P→Q -||- ¬(P ∧ ¬Q)
 2.3 p.68 9529 A wff is 'inconsistent' if all assignments to variables result in the value F
 2.3 p.68 9530 A wff is 'contingent' if produces at least one T and at least one F
 2.3 p.68 9528 A wff is a 'tautology' if all assignments to variables result in the value T
 2.3 p.69 9532 'Subcontrary' propositions are never both false, so that A∨B is a tautology
 2.3 p.69 9531 'Contrary' propositions are never both true, so that ¬(A∧B) is a tautology
 2.3 p.70 9534 Two propositions are 'equivalent' if they mirror one another's truth-value
 2.3 p.70 9535 'Contradictory' propositions always differ in truth-value
 2.3 p.70 9533 A 'implies' B if B is true whenever A is true (so that A→B is tautologous)
 2.4 p.80 9536 If any of the nine rules of propositional logic are applied to tautologies, the result is a tautology
 2.4 p.81 9537 Truth-tables are good for showing invalidity
 2.5 p.90 9539 Propositional logic is complete, since all of its tautologous sequents are derivable
 2.5 p.91 9538 A truth-table test is entirely mechanical, but this won't work for more complex logic
 3.1 p.96 13909 Write '(∀x)(...)' to mean 'take any x: then...', and '(∃x)(...)' to mean 'there is an x such that....'
 3.1 p.97 13910 Our notation uses 'predicate-letters' (for 'properties'), 'variables', 'proper names', 'connectives' and 'quantifiers'
 3.1 p.97 13900 'Some Frenchmen are generous' is rendered by (∃x)(Fx→Gx), and not with the conditional →
 3.1 p.98 13902 'Gm' says m has property G, and 'Pmn' says m has relation P to n
 3.2 p.104 13903 Universal elimination if you start with the universal, introduction if you want to end with it
 3.2 p.105 13904 Universal Elimination (UE) lets us infer that an object has F, from all things having F
 3.2 p.105 13905 If there is a finite domain and all objects have names, complex conjunctions can replace universal quantifiers
 3.2 p.106 13906 With finite named objects, we can generalise with &-Intro, but otherwise we need ∀-Intro
 3.3 p.111 13908 UE all-to-one; UI one-to-all; EI arbitrary-to-one; EE proof-to-one
 4.1 p.139 13911 The 'symbols' are bracket, connective, term, variable, predicate letter, reverse-E