Agler (5.6) Symbolic Logic: Syntax, Semantics, and Proof, "Additional Derivation Strategies", summary

 

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

[Central Entry Directory]
[Logic & Semantics, Entry Directory]
[David Agler, entry directory]
[Agler’s Symbolic Logic, entry directory]

[The following is summary. Boldface (except for metavariables) and bracketed commentary are my own. Please forgive my typos, as proofreading is incomplete. I highly recommend Agler’s excellent book. It is one of the best introductions to logic I have come across.]

 

 

 

Summary of

 

David W. Agler

 

Symbolic Logic: Syntax, Semantics, and Proof

 

Ch.5: Propositional Logic Derivations

5.6 Additional Derivation Strategies

 

 

 

Brief summary:

After revising our strategic rules for proof solving, they are in their entirety the following [the first three being this section’s modifications]:

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)

 

 

 

Summary

 

5.6 Additional Derivation Strategies

 

Since we previously added six new derivation rules, we will need to revise our proof strategies to accommodate them (Agler 116). Agler lists them first, then we proceed through them individually:

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

(Agler 216)

 

To illustrate the first rule, he has us consider

P→Q, ¬Q, P∨R, R→W ⊢ W

[Recall the rule: “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” (216).] Let us set it up.

SP#1(E+) tells us to make as many eliminations as possible. As we can see, we can use MT using lines 1 and 2.

And then now we can use DS using lines 3 and 5.

And finally we can use conditional elimination to obtain our goal proposition.

 

Agler shows another proof that demonstrates this first revised rule.

(P∧M)∧(¬Q∨R), P→L, P↔T, ¬R∧W ⊢ (L∧T)∧¬Q

(Agler 217)

First we set it up.

We have some conjunctions that will allow us to derive simpler propositions through elimination. And perhaps this will give us parts to make other sorts of eliminations. Since out goal proposition is made of conjunctions, we can try to build it back up using conjunction introduction. We might start by using elimination on the first line.

And we can use it again on the fourth line.

We see also that we can use conjunction elimination on our derived line 5.

That is all the conjunctions. But we see now that we can make other eliminations. We can use conditional elimination on line 2.

And we can use biconditional elimination on line 3.

And finally, we can use disjunctive syllogism on line 6.

This gives us all the parts we need to build up our goal proposition. So we do the nested conjunction first.

And we complete it in this way.

(Agler 218)

 

Recall the third strategic rule

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

(Agler 218)

 

To illustrate, he has us consider this argument:

¬[P∨(R∨M)], ¬M→T ⊢ T

(Agler 218)

Let us set it up.

We can see in the first line that we can apply De Morgan’s Law.

This gives us a conjunction that can be decomposed.

We can now use De Morgan’s Law on line 5.

Now with line 7, we can derive our goal proposition.

(Agler 219)

 

 

5.6.1 Sample Problem

 

Agler will now give a complicated example using a few nested assumptions to show an instance where we would make multiple uses of the rules.

⊢ [P→(Q→R)]→[(¬Q→¬P)→(P→R)]

(Agler 219)

 

Now, let us look at all our strategic rules together.

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)

We do not have any propositions, so we need to begin with an assumption. The question is, which assumption rule should we use? As we can see, we use SA#2(→), “If the conclusion is a conditional, assume the antecedent, derive the consequent, and use ‘→I.’”

So let us set it up by assuming the antecedent.

Now, at this point we cannot make any further eliminations. [One operation we might perform is IMP to get ¬P∨(Q→R). Agler does not take this route, perhaps because it is either inefficient or ineffectual.] One option we have at this point is to make a second assumption. Recall that the point of this assumption is to derive the consequent of the goal proposition. That consequent is:

(¬Q→¬P)→(P→R)

To obtain this, we could assume the antecedent.

Now again, no elimination rules apply to this formula. We recall that we want to finally derive the consequent of this subgoal proposition, so we want to derive P→R. One option would be to assume P with hopes to derive R.

The question is now, how can we derive R? We see that we can use implication elimination on line 1 and 3 to obtain Q→R. After that we would just need a way to derive Q. So let us do that.

Since we have P, that means we could use Modus Tolens to get Q, but we have to work through some double negations. Let us derive a doubly negated P from line 3.

Then with Modus Tolens we can get a doubly negated Q from line 2.

From this we can derive Q.

Which we needed to derive R in line 4.

And we needed R to derive P→R in the next outer subproof, which we do using conditional introduction.

We needed that to obtain the consequent of the goal proposition.

And again using conditional introduction, we can produce the whole goal proposition.

(Agler 221)

 

Agler notes another effective way to complete the proof. Let us go back to step 3.

[Recall this strategic assumption rule: “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.’”] Instead of using SA#2(→) like above, we can notice that the goal proposition is R, and thus is atomic. That means we can also use SA#1(P,¬Q), where we assume the negation of R and derive a contradiction. So let us do that.

Now how will we derive a contradiction? [One way might be to use IMP on line 1 to get Q implies R. Then using Modus Tolens on that and line 4 we get negated Q. Then with conditional elimination on line 2 we get negated P, which contradicts the assumption in line 3.] We might see one possibility already, since we have P in line 3 and negated P as the consequent in line 2. If we can just find negated Q, then we can obtain that contradiction of P and negated P. We will do this by working through the conditional in line 1. So we use conditional elimination on line 1 to get Q implies R.

Then using Modus Tolens we can obtain negated Q.

Then with conditional elimination on 2 we can derive negated P.

This contradicts P in line 3, so let us reiterate it to expose that contradiction in the lowest subproof.

That contradiction allows us to derive the non-negated form of our assumption, so we obtain R in the next outer subproof.

From this point on we follow the same procedure as before.

(Agler 222)

 

 

 

 

 

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