PHIL 250: Introduction to Symbolic Logic
tennant.9@osu.edu


Spring 1998



Notes on constructing proofs of conclusions from premisses.

Introduction Mode:

1. Look at the conclusion of the deductive problem posed.

2. Ask yourself what its dominant operator is.

3. Recall the introduction rule for that operator.

4. Break the problem into the sub-problem(s) called for by the form of that introduction rule.

[THIS IS WHY YOU HAVE TO KNOW THE RULES OF INFERENCE OFF BY HEART!]

Thus, if you have to prove (PQ), set about proving P and proving Q (from the available assumptions). If you have to prove ¬P, then assume P (for reductio ad absurdum) and try to prove absurdity (⊥) from P plus the other available assumptions. Once you have reached absurdity, you will be able to apply negation-introduction to obtain the conclusion ¬P, thereby discharging the assumption P. If you have to prove (PQ), then assume P for the sake of argument and try to prove Q from P plus the other available assumptions.

This strategy (of Introduction Mode) usually works when the dominant operator of the conclusion is negation, conjunction or implication. It might not work if the dominant operator of the conclusion is disjunction, and there are any disjunctions among the premisses (or disjunctive subformulae among the premisses, which, when unearthed, would become available as premisses). The obvious case of this would be the problem

	A∨B
	___

	B∨A
The lesson is that problems involving disjunction might be better approached by trying disjunction-elimination (so-called ``proof by cases") as the last step of the proof. In ``building the proof up from below" you will be provisionally intending to have a disjunction-elimination lower down in the proof than the disjunction-introductions that you would otherwise be tempted to try. [Following this advice, try proving the last problem before proceeding further. If you get stuck, find the solution here. ]

Repeat Introduction Mode until the conclusions of sub-problems are atomic. Then proceed to

Elimination Mode:

Look for a promising premiss in order to perform an elimination on its dominant operator.
[AGAIN, THIS IS WHY YOU MUST KNOW THE RULES OFF BY HEART!]

Conjunctive premisses PQ can automatically be decomposed by conjunction-elimination into their conjuncts P and Q. Disjunctive premisses PvQ automatically generate sub-problems in the form of ``case-proofs" for disjunction-elimination, using the disjuncts P and Q as case-assumptions (to be discharged later) along with whatever other assumptions are available at that point. A negated premiss like ¬P calls for you to supply a proof of the unnegated part P (so that you can then perform negation-elimination to obtain ⊥). Implications (PQ) call for a proof of the antecedent P, so that you can then infer the consequent Q by conditional-elimination (modus ponens). Repeat Elimination Mode as often as possible; but go back to Introduction Mode at any point where you have a newly generated complex conclusion in a sub-problem.

Note that in general you will toggle between Introduction Mode and Elimination Mode. For example, if in Elimination Mode you deal with a conditional premiss (P→Q) (as the major premiss of a conditional-elimination), you will generate the sub-problem of having to prove the antecedent P from the available assumptions. If P is complex, this will put you back into Introduction Mode, trying to get P as a conclusion by means of an application of the introduction rule for its dominant connective.

Eventually, after toggling sufficiently often between Introduction Mode and Elimination Mode, you reach a point where you have to ``glue the middle bits together", these middle bits usually being atomic (if the problem has been posed efficiently). You will have been ``building up" by means of introduction rules (Introduction Mode), and ``building down" by means of elimination rules (Elimination Mode). The bottom bits of the upper part and the top bits of the lower part have to be joined together at points where they have occurrences of the same formulae (usually atomic).

To see the preceding advice put into effect, try working through this simple example:


	A→B
	¬B
	___

	¬A

Now try following the strategic advice given above on some simple deductive problems, which have been selected so that the advice will work.