## 27 Jul 2016

### Rules and Strategies for Logic Proofs (Alger, Nolt)

[Search Blog Here. Index-tags are found on the bottom of the left column.]

[Logic & Semantics, Entry Directory]

Rules and Strategies for Logic Proofs

(Agler, Nolt)

David Agler

Symbolic Logic

Agler’s PD+ (11 Int-Elim Propositional Derivation Rules plus Additional Rules)

(Agler 242-244)

Agler’s Proof Strategies

SP#1(E+): First, eliminate any conjunctions with ‘∧E,’ disjunctions with DS or ‘∨E,’ conditionals with ‘→E’ or MT, and biconditionals with ‘↔E.’ Then, if necessary, use any introduction rules to reach the desired conclusion.

SP#2(B): First, work backward from the conclusion using introduction rules (e.g., ‘∧I,’‘∨I,’‘→I,’‘↔I’). Then, use SP#1(E).

SP#3(EQ+): Use DeM on any negated disjunctions or negated conjunctions, and then use SP#1(E). Use IMP on negated conditionals, then use DeM, and then use SP#1(E).

SA#1(P,¬Q): If the conclusion is an atomic proposition (or a negated proposition), assume the negation of the proposition (or the non-negated form of the negated proposition), derive a contradiction, and then use ‘¬I’ or ‘¬E.’

SA#2(→): If the conclusion is a conditional, assume the antecedent, derive the consequent, and use ‘→I.’

SA#3(∧): If the conclusion is a conjunction, you will need two steps. First, assume the negation of one of the conjuncts, derive a contradiction, and then use ‘¬I’ or ‘¬E.’ Second, in a separate subproof, assume the negation of the other conjunct, derive a contradiction, and then use ‘¬I’ or ‘¬E.’ From this point, a use of ‘∧I’ will solve the proof.

SA#4(∨): If the conclusion is a disjunction, assume the negation of the whole disjunction, derive a contradiction, and then use ‘¬I’ or ‘¬E.’

(Agler 199; 216)

Agler’s Quantification Rules

 Universal Elimination (∀E) From any universally quantified proposition ‘(∀x)P,’ we can derive a substitution instance ‘P(a/x)’ in which all bound variables are consistently replaced with any individual constant (name). (∀x)P P(a/x) ∀E

 Existential Introduction (∃Ι) From any possible substitution instance ‘P(a/x),’ an existentially quantified proposition ‘(∃x)P’ can be derived by consistently replacing at least one individual constant (name) with an existentially quantified variable. P(a/x) (∃x)P ∃I

 Universal Introduction (∀Ι) A universally quantified proposition ‘(∀x)P’ can be derived from a possible substitution instance ‘P(a/x)’ provided (1) ‘a’ does not occur as a premise or as an assumption in an open subproof, and (2) ‘a’ does not occur in ‘(∀x)P.’ P(a/x)(∀x)P ∀I

 Existential Elimination (∃E) From an existentially quantified expression ‘(∃x)P,’ an expression ‘Q’ can be derived from the derivation of an assumed substitution instance ‘P(a/x)’ of ‘(∃x)P’ provided (1) the individuating constant ‘a’ does not occur in any premise or in an active proof (or subproof) prior to its arbitrary introduction in the assumption ‘P(a/x),’ and (2) the individuating constant ‘a’ does not occur in proposition ‘Q’ discharged from the subproof. (∃x)P    | P(a/x)    | .    | .    | .    | Q Q ∃E
(Agler 357-358 See Symbolic Logic section 8.1)

Agler’s Additional Strategic Rules for Quantification

SQ#1(∀E): When using (∀E), the choice of substitution instances ‘P(a/x)’ should be guided by the individual constants (names) already occurring in the proof and any individual constants (names) occurring in the conclusion.
(Agler 328)

SQ#2(∃I): When using (∃I), aim at deriving a substitution instance ‘P(a/x)’ such that a use of (∃I) will result in the desired conclusion. (In other words, if the ultimate goal is to derive ‘(∃x)Px,’ aim to derive a substitution instance of ‘(∃x)Px,’ like ‘Pa,’ ‘Pb,’ ‘Pr,’ so that a use of (∃I) will result in ‘(∃x)Px.’)

SQ#3(∀I): When the goal proposition is a universally quantified proposition ‘(∀x)P,’ derive a substitution instance ‘P(a/x)’ such that a use of (∀I) will result in the desired conclusion.

SQ#4(∃E) Generally, when deciding upon a substitution instance ‘P(a/x)’ to assume for a use of (∃E), choose one that is foreign to the proof.

(Agler 358)

John Nolt

Logics

Nolt’s 10 Rules of Inference

 ~E Negation Elimination (Double Negation) From ~~Φ, infer Φ. ~I Negation Introduction (Reductio ad Absurdum, Indirect Proof Given a hypothetical derivation of any formula of the form (Ψ & ~Ψ) from Φ, end the derivation and infer ~Φ. &E Conjunction Elimination (Simplification) From (Φ & Ψ), infer either Φ or Ψ. &I Conjunction Introduction (Conjunction) From Φ and Ψ, infer (Φ & Ψ). ∨E Disjunction Elimination (Constructive Dilemma) From (Φ ∨ Ψ), (Φ→ Θ), and (Ψ→ Θ), infer Θ. ∨I Disjunction Introduction (Addition) From Φ, infer either (Φ ∨ Ψ) or (Ψ ∨ Φ). ~E Conditional Elimination (Modus Ponens) Given (Φ→ Ψ) and Φ, infer Ψ. →I Conditional Introduction (Conditional Proof) Given a hypothetical derivation of Ψ from Φ, end the derivation and infer (Φ→ Ψ). ↔E Biconditional Elimination From (Φ ↔ Ψ), infer either(Φ→Ψ) or (Ψ→Φ). ↔I Biconditional Introduction From (Φ→ Ψ ) and (Ψ→Φ), infer (Φ ↔ Ψ).

(Nolt 102)

Nolt’s Important Derived Rules

 MT Modus Tollens From Φ → Ψ and ~Ψ, infer ~Φ. CP Contraposition From Φ → Ψ, infer ~Ψ → ~Φ. ↔MP Biconditional Modus Ponens From Φ ↔ Ψ and Φ, infer Ψ. And fromΦ ↔ Ψ and Ψ, infer Φ. ↔MT Biconditional Modus Tollens From Φ ↔ Ψ and ~Ψ, infer ~Φ. And fromΦ ↔ Ψ and ~Φ, infer ~Ψ. DS Disjunctive Syllogism From Φ ∨ Ψ and ~Φ, infer Ψ. And from Φ ∨ Ψ and ~Ψ, infer Φ. HS Hypothetical Syllogism From Φ → Ψ and Ψ → Θ, infer Φ → Θ. DN Double Negation From Φ, infer ~~Φ. DM DeMorgan’s Law’s From ~(Φ ∨ Ψ), infer~Φ & ~Ψ. From ~Φ & ~Ψ, infer ~(Φ ∨ Ψ). From ~(Φ & Ψ), infer ~Φ ∨ ~Ψ. From ~Φ ∨ ~Ψ, infer ~(Φ & Ψ). From Φ ∨ Ψ, infer ~(~Φ & ~Ψ). From ~(~Φ & ~Ψ), infer Φ ∨ Ψ. From Φ & Ψ, infer ~(~Φ ∨ ~Ψ). From ~(~Φ ∨ ~Ψ), infer Φ & Ψ. COM Commutation From Φ & Ψ, infer Ψ & Φ. From Φ ∨ Ψ, infer Ψ ∨ Φ. ASSOC Association From(Φ & Ψ) & Θ, inferΦ & (Ψ & Θ).FromΦ & (Ψ & Θ), infer(Φ & Ψ) & Θ.From(Φ ∨ Ψ) ∨ Θ, inferΦ ∨ (Ψ ∨ Θ).From Φ ∨ (Ψ ∨ Θ), infer(Φ ∨ Ψ) ∨ Θ. DIST Distribution From(Φ & Ψ) ∨ Θ, infer(Φ ∨ Θ) & (Ψ ∨ Θ).From(Φ ∨ Θ) & (Ψ ∨ Θ), infer(Φ & Ψ) ∨ Θ.From(Φ ∨ Ψ) & Θ, infer(Φ & Θ) ∨ (Ψ & Θ).From(Φ & Θ) ∨ (Ψ & Θ), infer(Φ ∨ Ψ) & Θ. MI Material Implication From Φ → Ψ, infer ~Φ ∨ Ψ. From ~Φ ∨ Ψ, infer Φ → Ψ. From Φ → Ψ, infer ~(Φ & ~Ψ). From ~(Φ & ~Ψ), infer Φ → Ψ. EFQ Ex Falso Quodlibet From Φ and ~Φ, infer any formula Ψ.

(Nolt 102)

Nolt’s Proof Strategies

 If the conclusion or subconclusion you are trying to prove is of the form: Then try this strategy: ~Φ Hypothesize Φ and work toward a subconclusion of the form Ψ & ~Ψ in order to obtain ~Φ by~I. Φ & Ψ Prove the subconclusions Φ and Ψ separately and then join them by &I. Φ ∨ Ψ If either Φ or Ψ is a premise, simply apply ∨I to obtain Φ ∨ Ψ. Otherwise, if there is a disjunctive premise Θ ∨ Δ, try proving the two conditionals Θ → (Φ ∨ Ψ) and Δ → ( Φ ∨ Ψ) as subconclusions and then using ∨E to obtain Φ ∨ Ψ. If neither of these strategies works, then hypothesize ~(Φ ∨ Ψ) and work toward a subconclusion of the form Θ & ~Θ in order to obtain Φ ∨ Ψ by ~I and~ E. Φ → Ψ Hypothesize Φ and work toward the subconclusion Ψ in order to obtain the conditional by →I. Φ ↔ Ψ Prove the subconclusions Φ → Ψ and Ψ → Φ; then use ↔I to obtain Φ ↔ Ψ.

(Nolt 99)

Nolt’s Quantifier Rules

 ∃I Existential Introduction Let Φ be any formula containing some name α and Φβ/α be the result of replacing at least one occurrence of α in Φ by some variable β not already in Φ. Then from Φ infer ∃βΦβ/α. ∃E Existential Elimination Let ∃βΦ be any existential formula, Ψ any formula, and α any name that occurs neither in Φ nor in Ψ. And let Φα/β be the result of replacing all occurrences of the variable β in Φ by α. Then, given a derivation of Ψ from the hypothesis Φα/β, end the hypothetical derivation and from ∃βΦ infer Ψ, provided that α does not occur in any other hypothesis whose hypothetical derivation has not ended or in any assumption. ∀E Universal Elimination Let ∀βΦ be any universally quantified formula and Φα/β be the result of replacing all occurrences of the variable β in Φ by some name α. Then from ∀βΦ infer Φα/β. ∀I Universal Introduction Let Φ be a formula containing a name α, and let Φβ/α be the result of replacing all occurrences of α in Φ by some variable β not already in Φ. Then from Φ infer ∀β Φβ/α, provided that α does not occur in any hypothesis whose hypothetical derivation has not yet ended or in any assumption.

(Nolt 225, 229, 233, 236)

Nolt’s Quantifier Exchange Rules (QE)

 From ∀βΦ, infer ~∃β~Φ. From ∃βΦ, infer ~∀β~Φ. From ~∀βΦ, infer ∃β~Φ. From ~∃βΦ, infer ∀β~Φ. From ∀β~Φ, infer ~∃βΦ. From ∃β~Φ, infer ~∀βΦ. From ~∀β~Φ, infer ∃βΦ. From ~∃β~Φ, infer ∀βΦ.

(Nolt 238)

Quantifier Proof Strategies

 If the conclusion or subconclusion you are trying to prove is of the form: Then try this strategy: ∃βΦ Work toward a subconclusion of the form Φα/β, where α is a name that does not occur in Φ, in order to obtain ∃βΦ by ∃I. If there is an existential premise, it is likely that the subconclusion Φα/β will have to be derived hypothetically after a representative instance of this premise has been hypothesized for ∃E. In that case, to avoid misusing ∃E, obtain ∃βΦ by ∃I before ending the hypothetical derivation with ∃E. If all else fails, hypothesize ~∃βΦ and work toward a subconclusion of the form Θ & ~Θ in order to obtain ∃βΦ by ~I and ~E. ∀βΦ Work toward a subconclusion of the form Φα/β, where α is a name that does not occur in Φ or in any assumption or hypothesis whose hypothetical derivation has not yet ended, in order to obtain ∀βΦ by ∀I. If there are universal premises, it is likely that some or all of them will have to be instantiated with a by ∀E before this can be done.

(Nolt 239)

Nolt’s Rules for Identity

 =I Identity Introduction Where α is any name, assert α = α. = E Identity Elimination From a premise of the form α = β and a formula Φ containing either α or β, infer any formula which results from replacing one or more occurrences of either of these names by the other in Φ.

(Nolt 241-242)

Nolt’s Leibnizian Modal Logic Rules

 DUAL Duality From either ◊Φ and ~□~Φ, infer the other; from either □Φ and ~◊~Φ, infer the other. K K rule From □(Φ → Ψ), infer (□Φ → □Ψ). T T rule From □Φ, infer Φ. S4 S4 rule From □Φ, infer □□Φ B Brouwer rule From Φ, infer□◊Φ. N Necessitation If Φ has previously been proven as a theorem, then any formula of the form □Φ may be introduced at any line of a proof. □= Necessity of identity From α = β, infer□α = β.

(Nolt 328)

 Free Logic Quantification Inference Rules Free Existential Introduction (F∃I) Let Φ be any formula containing some name α and Φβ/α be the result of replacing at least one occurrence of α in Φ by some variable β not already in Φ. Then from Φ and ∃x x = α infer ∃βΦβ/α. Free Existential Elimination (F∃E) Let ∃βΦ be any existential formula, Ψ any formula, and α any name that occurs neither in Φ nor in Ψ. And let Φα/β be the result of replacing all occurrences of the variable β in Φ by α. Then, given a derivation of Ψ from the hypothesis Φα/β & ∃x x = α, end the hypothetical derivation and from ∃βΦ infer Ψ, provided that α does not occur in any other hypothesis whose hypothetical derivation has not ended or in any assumption. Free Universal Introduction (F∀I) Let Φ be a formula containing a name α, and let Φβ/α be the result of replacing all occurrences of α in Φ by some variable β not already in Φ. Then given a derivation of Φ from the hypothesis ∃x x = α, end the hypothetical derivation and infer ∀βΦβ/α, provided that α does not occur in any other hypothesis whose hypothetical derivation has not yet ended or in any assumption. Free Universal Elimination (F∀E) Let ∀βΦ be any universally quantified formula and Φα/β be the result of replacing all occurrences of the variable β in Φ for some name α. Then from ∀βΦ and ∃x x = α infer Φα/β.

(Nolt 403, see section 15.1)

From:

Agler, David. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman &; Littlefield, 2013.

Nolt, John. Logics. Belmont, CA: Wadsworth, 1997.