A more complex example of a formal proof is as follows:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
You might notice, right off the bat, that there are no simple components to work with here. Therefore, we can't work top-down, so to speak. If, for example, we had as a premise, J, then we could derive (S & G) from premise 2. Since we have no simple components to start out with, we have to approach this proof with what's called the bottom-up method. In other words, we have to assume something.
You can make two kinds of assumptions in propositional logic: conditional proof and indirect proof. A conditional proof is where you assume the antecedent to a conditional and try and derive its consequent. An indirect proof is when you assume the opposite of what you're trying to prove to be true. The theological problem of evil argument utilizes indirect proof, also known as Reductio Ad Absurdum. Anselm's ontological argument for the existence of God does, as well. With an indirect proof, we are looking to derive a contradiction of any kind. If, for instance, we assume B and, from this, are able to derive F & ~F, then we are allowed to leave the subproof by writing the negation of that which we assumed. In this case, we'd write ~B. Once a subproof is closed, we are not allowed to use any of those lines in our proof.
So which type of assumption should we use? I'd say our best bet is to use conditional proof. Although we can likely use indirect proof to derive some simple statement with which to begin breaking things apart, since the conclusion is a conditional itself, it is usually best to begin by assuming the antecedent of the conclusion, J, as a conditional proof:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
Whenever we make an assumption, we indent. Due to formatting issues on this forum, I'm filling in the gap with periods. Also, over on the right side we write "assume" and then, in parentheses, an abbreviation/acronym of the type of assumption we're making. In this case, CP for conditional proof. By asuming J as a conditional proof, we're attempting to derive ~R --> Q. Once we have this, we can leave this subproof. Moreover, once we have this, we have the conclusion and are finished with our proof.
As previously stated, since we're in a subproof, we must remain in it until we derive the consequent of the conditional statement we're trying to prove. In other words, line 5 will also remain indented. Also, whenever we're in a subproof, we are only allowed to utilize lines that are directly above or to the left of the subproof. And although we must continue to write our lines indented, we can utilize all lines (e.g. 1, 2 and 3). Since we now have J to work with, we see that on line 2, we have a conditional statement where the antecedent is J. So, the next move is simple:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
5. .........S & G....................................................2, 4 MP
We derive line 5 from lines 2 and 4 by the rule of modus ponens (MP).
At this point, we have to see how we might be able to use the simple components S and G. We notice that in premise 3 there is an S. However, it is currently stuck in a conjunction, and since we need both parts of the conjunction in order to play with that conditional, we are unable to do anything with premise 3. Once again, we have no top-down moves to make. We must make another assumption; a subproof within the subproof. We might notice that the conclusion we're trying to prove is a conditional statement within a larger conditional statement. We've already assumed the antecedent of the overall conditional on line 4. So the best next step would be to assume the antecedent of the conditional statement that appears in the conclusion after the J, namely, ~R. In other words, the conclusion is J --> (~R --> Q), we've assumed J and gone as far as we can, and so now we can assume ~R as another conditional proof in order to derive Q:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
5. .........S & G....................................................2, 4 MP
6. ...................~R.............................................Assume (CP)
The same rules apply as before: we can utilize all lines of the proof (since they are all directly up or to the left of the subproof) but we can't leave this new subproof until we've derived the conclusion we're looking for, namely, Q.
Once again, we look to see what ~R can do for us, top-down. Premise 1 is the only premise that houses an R. Lucky for us, there is a rule for conditionals known as modus tollens. Whereas modus ponens is used to derive the consequent by use of the antecedent, modus tollens is used to derive the negation of the antecedent by use of the negation of the consequent. An example in English might be as follows:
1. If Jason lives in Los Angeles, then he lives in California.
2. Jason does not live in California.
Therefore: Jason does not live in Los Angeles.
Beware of the fallacies known as asserting the consequent and denying the antecedent. Asserting the consequent looks as follows:
1. If Jason lives in Los Angeles, then he lives in California.
2. Jason lives in California.
Therefore: Jason lives in Los Angeles.
Obviously this does not follow and can be understood via the English since we know that other cities exist within California. Jason might, for instance, live in San Francisco.
The fallacy of denying the antecedent goes:
1. If Jason lives in Los Angeles, then he lives in California.
2. Jason does not live in Los Angeles.
Therefore: Jason does not live in California.
This does not follow for pretty much the same reason as above. Jason's not living in Los Angeles, CA does not, therefore, bar him from living in any other city within the state of California.
Back to our formal proof:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
5. .........S & G....................................................2, 4 MP
6. ...................~R.............................................Assume (CP)
7. ...................~H.............................................1, 6 MT
Again, line 7 comes from lines 1 and 6 by the rule of modus tollens. Now we look to see where we can utilize ~H. Premise 3 has it within the conjunction as the antecedent of a conditional statement. We realize that in order to use modus ponens on premise 3, we need both ~H and S. And, in fact, we already have both. The next step is to extract the S from line 5 by the rule of simplification so that we may utilize it on its own:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
5. .........S & G....................................................2, 4 MP
6. ...................~R.............................................Assume (CP)
7. ...................~H.............................................1, 6 MT
8. ...................S...............................................5 Simp
Line 8 comes from line 5 by the rule of simplification (Simp). So now we have the ~H and the S by themselves. We want them together as a conjunction in order to play with the conditional in line 3. This move is also very simple. Just as we can take off parts of a conjunction at will, we can put statements together as conjunctions at will. Of course, we could write it as S & ~H, but we want the conjunction to look as it does in premise 3. So the next step looks as follows:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
5. .........S & G....................................................2, 4 MP
6. ...................~R.............................................Assume (CP)
7. ...................~H.............................................1, 6 MT
8. ...................S...............................................5 Simp
9. ...................~H & S.......................................7, 8 Conj
Line 9 comes from lines 7 and 8 by the rule of conjunction (Conj). The next step we've already discussed:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
5. .........S & G....................................................2, 4 MP
6. ...................~R.............................................Assume (CP)
7. ...................~H.............................................1, 6 MT
8. ...................S...............................................5 Simp
9. ...................~H & S.......................................7, 8 Conj
10. .................Q...............................................3, 9 MP
Line 10 comes from lines 3 and 9 by the rule of modus ponens. If you'll remember, the current subproof assumed the antecedent ~R in order to try and derive the consequent Q. We have now accomplished that task. Therefore, we are now allowed to exit this subproof. However, we are still within the first subproof. When we leave the subproof of a conditional proof, the very next line must be the conditional we were trying to prove. In this case, ~R --> Q:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
5. .........S & G....................................................2, 4 MP
6. ...................~R.............................................Assume (CP)
7. ...................~H.............................................1, 6 MT
8. ...................S...............................................5 Simp
9. ...................~H & S.......................................7, 8 Conj
10. .................Q...............................................3, 9 MP
11. .......~R --> Q...............................................6, 10 CP
Line 11 comes from lines 6 and 10 by conditional proof. Since we have left the subproof that began on line 6 and ended on line 10, we are no longer able to utilize lines 6 through 10. They are now off limits. In other words, in no future lines can we refer back to 6, 7, 8, 9 or 10. That subproof is closed.
However, we are still within the subproof started on line 4. Looking back at line 4, we realize that we were assuming J as the antecedent of a conditional proof where the consequent being pursued was ~R --> Q. Well, we have that now on line 11. So, just as fast as we left our right-most subproof, we can leave this one:
1. H --> R
2. J --> (S & G)
3. (~H & S) --> Q................................................Therefore: J --> (~R --> Q)
4. .........J..........................................................Assume (CP)
5. .........S & G....................................................2, 4 MP
6. ...................~R.............................................Assume (CP)
7. ...................~H.............................................1, 6 MT
8. ...................S...............................................5 Simp
9. ...................~H & S.......................................7, 8 Conj
10. .................Q...............................................3, 9 MP
11. .......~R --> Q...............................................6, 10 CP
12. J --> (~R --> Q)............................................4, 11 CP
Line 12 comes from lines 4 and 11 by conditional proof. And we're finished. We've proven that, given the premises, we can derive the conclusion. In other words, we've proven validity.