Agler (5.4) Symbolic Logic: Syntax, Semantics, and Proof, "Strategies for Proofs", 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.4 Strategies for Proofs

 

 

 

Brief summary:

Certain guidelines can enable us to figure out proofs more effectively. There are two rules that do not involve assumptions, called strategic proof rules (SP#). They are:

SP#1(E)

First, eliminate any conjunctions with ‘∧E,’ disjunctions with ‘∨E,’ conditionals with ‘→E,’ and biconditionals with ‘↔E.’ Then, if necessary, use any necessary 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).

(Agler 194)

And there are four rules that do involve assumptions:

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)

 

Summary

 

 

5.4 Strategies for Proofs

 

Agler will provide some strategies for making proofs more effectively. There are two kinds of strategies.

(1) strategies aimed at the direct manipulation of propositions in the proof, and

(2) strategies aimed at the deliberate and tactical use of assumptions.

(Agler 194)

 

 

5.4.1 Strategies Involving Premises

 

The first two strategies do not involve assumptions, and Agler calls them SP rules, for strategic proof.

SP#1(E)

First, eliminate any conjunctions with ‘∧E,’ disjunctions with ‘∨E,’ conditionals with ‘→E,’ and biconditionals with ‘↔E.’ Then, if necessary, use any necessary 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).

(Agler 194)

 

So we will begin with the first strategic rule. Agler explains that “the basic idea behind this strategic rule is to start a proof by simplifying or breaking down any available premises.” (195). He has us consider the following example.

P→(R∧M), (P∧S)∧Z ⊢ R

(Agler 195)

[So let us first set it up with the goal proposition noted.

As we can see there can be a series of eliminations that will lead us finally to R. So we begin with using conjunction elimination on line 2.

We are going to want just the P from line 3, but we will decompose the conjunction entirely with conjunction elimination.

Now that we have P, we can use conditional elimination on line 1.

And finally we can derive our goal proposition using conjunction elimination.]

 

Agler then has us consider a variation on the above example.

P→R, (P∧S)∧Z ⊢ R∧S

[Let us set it up.

And we use conjunction elimination to derive some more propositions.

And again, we will need the P.

Now with the P, we can derive R.

And we have all the basic parts we need to derive the goal proposition, but we will need to use an introduction rule.]

 

Now recall the second SP rule.

SP#2(B)

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

(Agler 194)

Agler says that “the basic idea behind this strategy is this: rather than moving forward (downward) in a proof from the premises or assumptions to a conclusion, work backward (upward) from the conclusion to the premises or assumptions” (196).

 

He has us consider the following argument:

P→R, Z→W, P ⊢ R∨W

(Agler 197)

[Note, in my version of the text, the argument is given as:

P→R, Z→W, P Z ⊢ R∨W

] [So let us set it up.

Now note that we could use an elimination rule on lines 1 and 3. However, Agler will have us jump to the conclusion, so that we can find the path to it.

We now work backward; we ask, by means of what derivation rule might we obtain R∨W? Since it is a disjunction, it could very well have been obtained from disjunction introduction.]

We will call propositions that are obtained as a result of the working-backward method intermediate conclusions. Thus, working backward we obtain the intermediate conclusions ‘R’ and ‘W’:

(Agler 198)

[What the ‘V’ spanning R and W means is that so long as we can derive either R or W, then we can derive R∨W using disjunction introduction. There seems to be no way to obtain W, but R we can derive using conditional elimination.]

In the above, we have created two paths. The first path links the premises to one of the intermediate conclusions. The second path links the intermediate conclusion to the conclusion of the proof. With both of these paths, we can finish the proof as follows:

Thus, the general idea behind SP#2(B) is to start with the conclusion and work backward, using any introduction rules that would yield an intermediate conclusion. Once you have worked backward to a sufficient degree, try to use any elimination rules that would lead you to an intermediate conclusion.

(Agler 198)

 

5.4.2 Strategies Involving Assumptions

 

Agler now will discuss strategic rules for proof solving for “proofs that either do not involve premises or that require the use of assumptions” (199).

 

Agler begins with rules involving assumptions. He says there are “roughly” four of them. Each is “classified by the main operator of the goal operation” (199). He continues:

That is, there is a strategic rule for atomic propositions and negated propositions (‘P,’ ‘¬Q’), one for conditionals (→), one for disjunctions (∨), and one for conjunctions (∧).

 

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)

 

Agler begins with this example:

P→Q, ¬Q ⊢ ¬P

(Agler 199)

So let us set it up.

[Recall SA#1: 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.’] Agler notes that since the goal proposition is a negated atomic proposition, ¬P, we should begin by assuming the non-negated form, P.

[I do not recall the use of “contra” in the justifications from before. I think when doing negation introduction or elimination, we would just put the other form of the proposition. From what follows I gather the reason for using “contra” is that we may not know at the beginning which contradiction we are trying to obtain. At any rate, we see that with P we can derive Q.

And we can reiterate ¬Q.

On the basis of this contradiction we can derive ¬P in the main proof.

 

 

Agler has us now consider this example:

P ⊢ ¬¬P

(Agler 200)

[As we can see, we have a negated form of an atomic formula. It should not matter that it is doubly negated. We will assume the form that is once less negated, ¬P.

That contradicts the premise P.

Thus by using negation introduction, we can derive ¬¬P.

Agler explains:

The goal proposition of this proof is a negated proposition. SA#1(P, ¬Q) says to start by assuming the opposite of our desired goal. In this case, ‘¬P’ is assumed. Next, SA#1(P,¬Q) says to derive a contradiction. This is done at lines 2 and 3. Finally, SA#1(P,¬Q) says to close the subproof with ‘¬I.’ This is done at line 4.

(Agler 201)

 

Next Agler has us consider this argument:

⊢ ¬(P∧¬P)
(Agler 201)

As we can see, there are no premises to it. As such, “it will require starting the proof by making an assumption” (201). [As there are no premises, our first line will be the assumption. We will assume the unnegated form of the goal proposition.

As we can see, we can draw out a contradiction from it.

Thus we can derive the goal proposition in the main proof.]

(Agler 201)

[This intuitively seems valid. We cannot have a proposition and its negation, because this is a contradiction. So given our rules of logic, we should be able to prove ¬(P∧¬P) without needing any more support, that is to say, we should be able to prove it merely with an assumption and with our rules of derivation alone.]

[Recall the second strategic assumption rule: SA#2(→): If the conclusion is a conditional, assume the antecedent, derive the consequent, and use ‘→I.’] Next we consider:

R ⊢ P→R

(Agler 201)

Let us set it up.

If we follow SA#2, then we begin by assuming the antecedent, P.

We then can derive R by reiterating it.

And finally by using conditional introduction, we can derive the goal proposition.

 

Agler next gives this example:

R ⊢ (P∨R)→R

(Agler 202)

So we first set it up.

SA#2 tells us to assume the antecedent of the goal proposition.

Now we need to derive the consequent. We see that it is the premise, so we reiterate it.

Then we can use conditional introduction to derive the goal proposition.

(Agler 202)

 

Agler then has us consider one last example for the second assumption rule:

⊢  P→(Q→P)

Since it has no premises, we must begin with an assumption. As we can see, it is a conditional, so we will assume the antecedent.

By itself this will not not allow us to accomplish anything else. We see that we will need P implies that Q implies P. We can obtain the Q implies P by first assuming Q in a sub-subproof.

We then reiterate P from the outer proof.

With this structure we can then derive Q→P in the outer subproof.

We now have all the contents we need to derive the goal proposition in the main proof.

(Agler 203)

 

We now recall the third assumptional strategy:

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.

(Agler 203)

 

To illustrate, he has us consider this example:

¬(P∨Q) ⊢ ¬P∧¬Q

[This one is perhaps less obvious how to solve. We need to recall disjunction introduction. We can disjoin any given proposition to any other. We also know from the rule that we will want to assume the non-negated forms, P and Q. When we have the assumption of either, we can then disjoin it to the other, which will contradict the premise. For each case, we will be able to derive the negated forms, and thus in the main proof we can derive ¬P∧¬Q. So let us set it up.

And we begin by assuming P.

We then use disjunction introduction to disjoin P to Q.

We notice the contradiction with the premise. So let us reiterate the premise to establish that contradiction.

This means we can use negation introduction to derive ¬P in the main proof.

Now let us assume Q, so that we can in the end derive the right-conjunct in the goal proposition.

We will follow the same procedure. We disjoin Q to P.

We reiterate the premise to establish the contradiction.

This allows us to derive ¬Q in the main proof.

And we can now derive the goal proposition using conjunction introduction.

(Agler 204)

 

Now we turn to the fourth strategic proof involving assumptions. Recall that it was:

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

 

To illustrate it, Agler offers this example:

¬(¬P∧¬Q) ⊢ P∨Q

(Agler 204)

[This example is very tricky. It is probably not immediately obvious how to solve it, even with the forth rule in mind. Let us first run quickly through some reasoning, then we will repeat it below with illustration. The rule says we should assume ¬(P∨Q). But then what? The rule says to find a contradiction next. We just need to find any contradiction whatsoever, and then we can derive the unnegated form of ¬(P∨Q) using negation elimination. Given the tools we have, our only options seem to be finding either (¬P∧¬Q) to contradict the premise, or P∨Q to contradict the assumption. In order to obtain P∨Q in the first layer of subproof, we will need to obtain either P or Q in the second layer of subproof. We could do that by assuming their negations. However, with our available tools, it is not obvious how we will find a contradiction based on that assumption. So let us instead see our prospects with deriving ¬P∧¬Q in the first level of subproof. To get this, we need by means of two independent sub-subproofs to derive ¬P and ¬Q. To do this, we might begin by assuming P in one case and Q in another, then finding a contradiction in each case. This can conceivably be done by using disjunction introduction to obtain P∨Q in the sub-subproof, which will contradict our first assumption, thereby allowing us for each case of a sub-subproof to derive ¬P and ¬Q in the outer subproof. With these propositions we can derive ¬P∧¬Q in the subproof, which contradicts the first premise. That means we can derive the negation of our first assumption, which is the goal proposition. So let us work through this complicated proof little by little, beginning by setting it up.

We will run through the above reasoning again step by step with depictions. So at this point, with our given derivation tools, no easy straightforward path to a solution is immediately obvious. So here we notice that the conclusion is a disjunction, hence we follow the fourth rule. It tells us to first assume the negation of the disjunction.

As we noted, our contradiction can be any contradiction whatsoever. But given our derivation rules, there is not much we can produce to which we might find a contradiction. We have a negated conjunction and a negated disjunction. Perhaps later with De Morgan’s Laws we can derive something useful from them. But for the time being, the best we can do at this point is find a contradiction with either ¬(¬P∧¬Q) (from line 1) or with ¬(P∨Q) (from line 2), in their entirety. So long as we can at least do that, then we have a contradiction with our main assumption, which will allow us to use negation elimination to derive the non-negated form of the first assumption and thereby obtain the conclusion. So that means we have two options, we can find either ¬P∧¬Q or P∨Q.

(Agler 205)

Agler will only show us the first option. Perhaps this is because the second option is too complicated or impossible. Suppose we try for the second option. How can we derive P∨Q? Nothing available allows us to do that. So we will need to make further assumptions. What assumptions can we make that will allow us to get P∨Q? All we need is either P or Q, and then we can add the other using disjunction introduction. Our only tool for obtaining either P or Q is to assume their negation and find a contradiction. Can we do that? I cannot think of a way. So recall our two options:

What about the first option? To derive that formula, we could build it up using conjunction introduction. To do that we need to make subproofs that assume P or Q, then find a contradiction, thereby allowing us to derive both ¬P and ¬Q in the first subproof. Let us begin with P and see how we might go from there.

With just P, I do not think we can derive something to contradict line 1. However, by using disjunction introduction, we could contradict the second line. So let us do that.

We reiterate line 2 to expose the contradiction within the sub-subproof.

This allows us to derive ¬P in the outer subproof.

Now we need to do the same to get ¬Q. So let us assume Q.

We again use disjunction introduction to find a contradiction with line 2.

We reiterate line 2 again to expose the contradiction now in this sub-subproof.

This allows us to derive ¬Q in the outer subproof.

We currently have within the outer subproof the contents we need to make a contradiction with line 1. So let us use conjunction introduction to get ¬P∧¬Q.

We will reiterate line 1 to expose the contradiction in the subproof.

On the basis of this contradiction, we can derive the unnegated form of the assumption using negation elimination.

(Agler 204-206)

 

Agler then comments on the strategic rules so far.

Let’s take stock. We are working with two different kinds of strategies for solving proofs. First, there are the strategic proof rules that involve manipulating propositions that are available in the proof by either breaking down complex propositions with elimination rules or working backward with introduction rules. Second, there are strategic rules involving assumptions. Whenever you need to make an assumption, the proposition you assume should be guided by the main operator in the proposition you are trying to derive; that is, if it is a conditional, use SA#2(→).

(Agler 206)

 

 

 

 

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