27 Jul 2016

Rules and Strategies for Logic Proofs (Alger, Nolt)

 

by Corry Shores

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

 

[Central Entry Directory]

[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)

 

5.5.1 z2a15.5.1 z2a25.5.1 z2a35.5.1 z2a45.5.1 z2a55.5.1 z2a6

(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.

No comments:

Post a comment