PROOFS WITH EVEN FEWER TEARS

Being the Continuation of a Student's Handy Guide to Proving Sequents in the system of Allen/Hand, Logic Primer

Some more exercises from 1.5

The Notorious S29

S29. ~(P&Q) -||- ~Pv~Q

Left to right: No point repeating the argument to show that you can't get this one by vI, even though that is the first strategy to think of with disjunctions. (In this case, it just won't work). Instead, we have to resort to the indirect approach, which turns out not to be as bad as you might expect. Assume ~(~Pv~Q), then look for a contradictory pair. One nice contradictory pair to look for would be P&Q and ~(P&Q), since we already have ~(P&Q). In order to get P&Q, we need to get P and to get Q. The proof below does each of those indirectly: assume ~P (which at once gives you ~Pv~Q, the denial of (2)), then discharge with RAA; then do the analogous thing with ~Q. This gives P&Q, which is the denial of the premise, and so we can use RAA to discharge the assumption at (2).

Moral: it's often a good idea to try the indirect approach when proving disjunctions.

Right to left:

S27. P -> Q, ~P -> Q |- Q

Your text names this 'Special Dilemma', but another medieval name for it was 'Consequentia Mirabilis': 'the amazing consequence.'

This requires a little subtlety. To get Q out of (1), we'd need P, and there's no likely way to get it. So, best to try the indirect approach: we assume ~Q, then try to get a contradiction. Here is where it becomes subtle. There are two likely contradictory pairs we could aim for: Q and ~Q or P and ~P. Since we've assumed ~Q, it might be easiest to try to get Q. We could get Q if we had either P (from (1)) or ~P (from (2)). So, we could try to get one of those. I will choose ~P and try to get it with the indirect approach: assume P and look for a contradictory pair. In fact, we can get Q right away, giving us a contradictory pair with (3); ~P then gives us Q, so we have a contradictory pair after discharging the assumption of P, and we can then discharge the first assumption (~Q):

Notice that we can't stop at line (7), since its assumption set still includes the undischarged assumption (3). However, since we have contradictory lines (namely, it and that very assumption), we can discharge (3) with RAA.

S34. P -> Q -||- ~(P & ~Q)

Left to right: use the indirect approach. After you assume P&~Q, it's relatively quick to get both Q and ~Q, then use RAA. Right to left: what you want is a conditional, so use ->I (assume P and try to get Q). There's no rules for getting at the parts of negated conjunctions, so assume ~Q and look for a contradictory pair (the easiest one to get is ~(P&~Q) and P&~Q).

S36. P & Q -||- Q & P

This is easy, but it's important to realize that it does require proof. Here's the left-to-right part:

Right-to-left bears an extraordinary similarity to this.

S37. P v Q -||- Q v P

Compare this with the previous proof. It's not quite as easy. The only choice here is the indirect approach. After assuming ~(QvP), we need to get a contradictory pair. We can aim for the denial of that very assumption, that is, the thing we want to prove: QvP. To get that, we'd need either P or Q. However, we can get either one of those from (1) if we have the denial of the other. So, we assume one of them (in this case, I chose ~P):

There's a lot of other exercises in here you could do...

S54. P-> Q & R, R v ~Q -> S & T, T <-> U |- P -> U

Overall strategy: assume P, get U, use ->I. U occurs on the right side of a biconditional, so we can get it if we can get the other side (use <->E, then ->E), which is T. To get T, we need to get the right side of (2), for which we need its left side Rv~Q. Since that's a disjunction, we can get it if we can get either of its disjuncts R and ~Q. We can get R from the right side of (1) by &E; to get that, we'll need P. But we've already assumed P, so we've found the proof:

S55. (~P v Q) & R, Q -> S |- P -> (R -> S)

The conclusion is a conditional, so assume P and try to deduce R->S. Since that's also a conditional, assume R and try to get S. To get S we need Q, and we can get that from the left side of (1) and vE if we can get P; but we've already assumed P. So, we can discharge the two assumptions of R and P, in that order, to get the conclusion.

Notice that this is just a mite sneaky. We didn't actually use the assumption (4) to get anything at all: we got S without using it, then discharged it to get R->S. Sneaky, but legitimate.

S56. Q & R, Q -> P v S, ~(S & R) |- P

Use the indirect approach. Having assumed P, what shall we try to contradict? Since it's hard to think of anything else to do with ~(S&R), let's try for that. We can get its denial, S&R, if we can get both S and R. R is easy (line (1) by &E), so we're halfway there. We could get S if we could get the right side of (2) and use vE (we already have assumed ~P). But Q comes from (1) by &E, so we're home:

S57. P -> R & Q, S -> ~R v ~Q |- S & P -> T

S58. R & P, R -> (S v Q), ~(Q & P) |- S

S is a disjunct of the right side of (2), so if we can get that disjunct out (using ->E, requires R) we can get S with vE (this will require ~Q). R we can get from (1) with &E. ~Q is less obvious; we'll need to use the indirect approach. However, notice that if we assume Q and can get P, we can get Q&P, which is the denial of (3): so, there's our contradictory pair. Here's the proof:

S59. P & Q, R & ~S, Q -> (P -> T), T -> (R -> S v W) |- W

We could get W using vE, if we could get SvW out of line (4) and get ~S. ~S is available from (2) by &E. However, to get to SvW, we need T and R. R comes from line (2); T would come from the right side of (3), if we had P and Q. But we can get both those from (1), so we're set.

S60. R -> ~P, Q, Q -> (P v ~S) |- S -> ~R

Main strategy: Assume S and try to get ~R, then use ->E. To get ~R, assume R and aim for a contradictory pair, then use RAA. There's an S and a ~S in the premises, so the contradictory pair to try for is S and ~S. We already have S, so it's just a matter of getting ~S. To get that, we need first to get the right side of (3) , for which we need Q; but we already have Q. Then, we need ~P, for which we need R; but we've already assumed that. So, we can do the proof:

S61. P -> Q, P -> R, P -> S, T -> (U -> (~V -> ~S)), Q -> T, R -> (W -> U), V -> ~W, W |- ~P

This looks hideous, but we can approach it systematically. We want to assume P and aim or a contradictory pair, then use RAA. We have several possibilities hidden in the premises: w and ~W, S and ~S, V and ~V. Since W all by itself is a premise, let's try to get ~W. For that, we need V. We can get V (maybe) if we can get out the right side of the right side of (4), then use ->E twice (for which we will need T and U). We can get T from (5) if we can get Q, and we can get Q from (1) if we have P (but we've assumed it at (9). As for U, we can get that if we can get R and W; W we already have, and R we can get from (2) if we have P (and once again, we've assumed it at (9)). So, we can get ~V->~S. What we needed was V; so, we assume ~V and look for a contradictory pair, which is easy to find (get ~S from ~V->~S, S from (3) and (9)). Or, in its full glory:

S62. P <-> ~Q & S, P & (~T -> ~S) |- ~Q & T

We need to build a conjunction, so we need to get each of its conjuncts. ~Q is available by &E if we can get the right hand side of (1), so we'll want to use <->E and then look for P to use with the resulting conditional and ->E. To get T, we need first to get at the right hand side of P (use &E), then try assuming T for an RAA. The latter is relatively straightforward: we get ~S from ~T->~S, then get S from ~Q&S. Here (after a little tidying up) is the proof:

S63. P v Q <-> P & Q -||- P <-> Q

This is lengthy but relatively straightforward. Since each side is a biconditional, each of the two proofs will consist of two subproofs, each of which is the proof of a conditional. For left-to-right, we assume P and get Q, then assume Q and get P, then get the biconditional by <->I. In each case, we need only the left-right conditional from the premise.

Notice that the assumption set for line (15) is empty. That's not an error: line 15 is a theorem which can be proved from no assumptions at all.