| turnstile |
Definition. The TURNSTILE is the symbol |-.
|
|
|
|
| sequent |
Definition. A SEQUENT consists of a number
of sentences separated by commas (corresponding to the premises of an
argument), followed by a turnstile, followed by another sentence
(corresponding to the conclusion of the argument).
|
|
| Example. |
| (P & Q)->R, ~R & P |- ~Q |
|
| Comment. SequeNts are nothing more than a convenient way of
displaying arguments in the formal notation. The turnstile symbol may be
read as `therefore'. If there is just one sentence on each side of the
turnstile, the turnstile may be reversed ( -| ) to represent the argument
from the sentence on the right to the sentence on the left. |
|
|
|
| double turnstile |
Example.
|
| P -| |- Q |
|
|
Comment. This example corresponds to two sequents: P |- Q and Q
|- P. You may read the example as saying `P therefore Q, and Q
therefore P'. When proving PHI -| |- PSI, one must give two proofs:
one for PHI |- PSI and one for PSI |- PHI.
|
|
| Example. |
| Prove P -| |- P v P. |
|
| (a) Prove P |- P v P. |
| 1 (1) P A |
| 1 (2) P v P 1 vI |
|
|
| (b) Prove P v P |- P. |
| 1 (1) P v P A |
| 2 (2) ~P A |
| 1,2 (3) P 1,2 vE |
| 1 (4) P 2,3 RAA (2) |
|
|
Comment. A number of strategies aid in the discovery of proofs,
but there is no substitute for practice. We do not provide any
proof-discovery strategies in this book--that is the instructor's job. We
do provide plenty of exercises, so there should be no lack of opportunity
to practice.
|
|
|
|
Exercise 1.5 |
Give proofs for the following sequents, using the
primitive rules of proof. |
|
|
| S1* | P -| |- ~~P Double Negation |
| S2* | P->Q, ~Q |- ~P Modus Tollendo Tollens |
| S3 | P->~Q, Q |- ~P MTT |
| S4* | ~P->Q, ~Q |- P MTT |
| S5 | ~P->~Q, Q |- P MTT |
| S6* | P->Q, Q->R |- P->R Hypothetical Syllogism |
| S7* | P |- Q->P True Consequent |
| S8* | ~P |- P->Q False Antecedent |
| S9 | P |- ~P->Q FA |
| S10 | P->Q, P->~ Q |- ~P Impossible Antecedent |
| S12 | P v Q -| |- ~P->Q v-> |
| S13 | P v Q -| |- ~Q->P v-> |
| S14 | P v ~Q -| |- Q->P v-> |
| S15 | P v Q, P->R, Q->R |- R Simple Dilemma |
| S16* | P v Q, P->R, Q->S |- R v S Complex Dilemma |
| S17 | P->Q, ~P->Q |- Q Special Dilemma |
| S18* | ~(P v Q) -| |- ~P & ~QDeMorgan's Law |
| S19 | ~(P & Q) -| |- ~P v ~Q DM |
| S20 | P & Q -| |- ~(~P v ~Q) DM |
| S21 | P v Q -| |- ~(~P & ~Q) DM |
| S22* | ~(P->Q) -| |- P & ~Q Negated Arrow (Neg->) |
| S23 | ~(P->~Q) -| |- P & Q Neg-> |
| S24 | P->Q -| |- ~(P & ~Q) Neg-> |
| S25 | P->~Q -| |- ~(P & Q) Neg-> |
| S26 | P & Q -| |- Q & P & Commutativity |
| S27* | P v Q -| |- Q v P v Commutativity |
| S28* | P <-> Q -| |- Q <-> P <->Commutativity |
| S29 | P->Q -| |- ~Q->~P Transposition |
| S30 | P & (Q & R) -| |- (P & Q) & R & Associativity |
| S31* | P v (Q v R) -| |- (P v Q) v R v Associativity |
| S32* | P & (Q v R) -| |- (P & Q) v (P & R) &/v Distribution |
| S33 | iP v (Q & R) -| |- (P v Q) & (P v R) v/& Distribution |
| S34 | P->(Q->R) -| |- P & Q->R Imp/Exportation |
| S35 | P <-> Q, P |- Q Biconditional Ponens |
| S36 | P <-> Q, Q |- P BP |
| S37 | P <-> Q, ~P |- ~Q Biconditional Tollens |
| S38 | P <-> Q, ~Q |- ~P BT |
| S39 | P <-> Q -| |- ~Q <-> ~P BiTransposition |
| S40 | P <-> ~Q -| |- ~P <-> Q BiTrans |
| S41 | ~(P <-> Q) -| |- P <-> ~Q Negated <-> |
| S42 | ~(P <-> Q) -| |- ~P <-> Q Neg<-> |
| S43* | P <-> Q -| |- (P & Q) v (~P & ~Q) |
| S44 | P->Q & R, R v ~Q->S & T, T <-> U |- P->U |
| S45* | (~P v Q) & R, Q->S |- P->(R->S) |
| S46* | Q & R, Q->P v S, ~(S & R) |- P |
| S47 | P->R & Q, S->~R v ~Q |- S & P->T |
| S48 | R & P, R->(S v Q), ~(Q & P) |- S |
| S49 | P & Q, R & ~S, Q->(P->T), T->(R->S v W) |- W |
| S50 | R->~P, Q, Q->(P v ~S) |- S->~R |
| S51 | P->Q, P->R, P->S, T->(U->(~V->~S)), Q->T,
R->(W->U), V->~W, W |- ~P |
| S52 | P <-> ~Q & S, P & (~T->~S) |- ~Q & T |
| S53 | P v Q <-> P & Q |- P <-> Q |
|
|
|
| substitution |
Definition. A SUBSTITUTION
INSTANCE of a instance sequent is the result of uniformly replacing its
sentence letters with wffs.
|
|
|
Comment. This definition states that each occurrence of a given
sentence letter must be replaced with the same wff throughout the
sequent.
|
|
|
| Example. |
| The sequent |
| P v Q |- ~P->Q |
| has as a substitution instance the sequent |
| (R & S) v Q |- ~(R & S)->Q |
| according to the substitution pattern |
| P/(R & S); Q/Q. |
|
|
|
Comment. The given substitution pattern shows that the sentence
letter P was replaced throughout the original sequent by the wff (R &
S), and the sentence letter Q was replaced throughout by itself.
|
|
|
|
| Exercise 1.6 | Identify each of the following with a sequent in
exercise 1.5 and identify the substitution pattern. |
|
|
| i* | R->S -| |- ~S->~R |
| ii* | ~P->Q v R, Q v R->S |- ~P->S |
| iii* | (P & Q) v R -| |- R v (P & Q) |
| iv* | (P v Q) & (~R v ~S) -| |- ((P v Q) & ~R) v ((P v Q) & ~S) |
| v* | R v S -| |- ~~(R v S) |
| vi* | (P v R) & S -| |- ~(P v R->~S) |
| vii* | P v (Q v R) -| |- ~P->Q v R |
| viii* | ~(P & Q) |- R->~(P & Q) |
| ix* | ~((P & Q) v (R & S)) -| |- ~(P & Q) & ~(R & S) |
| x* | P v (R v S), P->Q & R, R v S->Q & R |- Q & R |
|
|
|
|
| derived rule |
Comment. Any sequent that one has proved
using only the primitive rules may subsequently be used as a DERIVED
RULE of proof if
|
|
|
| (i) |
some sentences appearing in the proof are the premises of the sequent, or
|
| (ii) |
some sentences appearing in the proof are the premises of a substitution instance of the sequent.
|
|
|
In case (i) the conclusion of the sequent may be asserted on the
current line; in case (ii) the conclusion of the substitution instance may
be asserted.
|
|
|
Annotation: the line numbers of the premises;S#, where S# is the
number from the book, or the name of the sequent (see comment below); and
the substitution pattern used, if applicable. (Substitutions of the
form f/f may be omitted.)
|
|
Assumption set: The union of the assumption sets of the premises.
|
|
Comment. Many of the sequents in exercise 1.5, particularly
S1-S34, are used so frequently as rules of proof that they have the names
we have indicated. (Indeed, in some systems of logic some of our derived
rules are given as primitive rules.)
|
|
|
| Examples. |
| (a) Prove R v S->T, ~T |- ~R. |
| 1 (1) R v S->T A |
| 2 (2) ~T A |
| 1,2 (3) ~(R v S) 1,2 MTT(P/R v S; Q/T) |
| 1,2 (4) ~R & ~S 3 DM (P/R; Q/S) |
| 1,2 (5) ~R 4 &E |
|
| (b) Prove P v R->S, T->~S |- T->~(P v R). |
| 1 (1) P v R->S A |
| 2 (2) T->~S A |
| 1 (3) ~S->~(P v R) 1 Trans (P/P v R; Q/S) |
| 1,2 (4) T->~(P v R) 2,3 HS (P/~S; Q/T; R/P v R) |
|
|
|
Comment. Requiring that the sequent has been proved using only
primitive rules is unnecessarily restrictive. If the sequents are proved in
a strict order and no later sequent in the series is used in the proof of
an earlier sequent, then no logical errors can result. We suggest the
stronger restriction only because it is good practice to construct proofs
using only the primitive rules.
|
|