by Corry Shores
[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’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