| theorem |
Definition. A THEOREM is a sentence that
can be proved from the empty set of premises.
|
|
|
Comment. We can assert that a given sentence is a theorem by
presenting it as the conclusion of a sequent with nothing to the left of
the turnstile.
|
|
|
|
| Example. |
| Prove |- P & Q->Q & P. |
| 1 (1) P & Q A |
| 1 (2) Q 1 &E |
| 1 (3) P 1 &E |
| 1 (4) Q & P 2,3 &I |
| (5) P & Q->Q & P 4 ->I (1) |
|
| Comment. Note that in step 5 we discharge assumption 1. Hence,
the final conclusion rests on no assumptions. |
|
|
| Exercise 1.7 | Prove the following theorems, (i) using primitive
rules only and (ii) using primitive rules together with derived rules
established in a previous exercise. |
|
|
| T1* | |- P->P Identity |
| T2* | |- P v ~P Excluded Middle |
| T3 | |- ~(P & ~P) Non-Contradiction |
| T4 | |- P->(Q->P) Weakening |
| T5* | |- (P->Q) v (Q->P) Paradox of Material Implication |
| T6* | |- P <-> ~~P Double Negation |
| T7 | |- (P <-> Q) <-> (Q <-> P) |
| T8* | |- ~(P <-> Q) <-> (~P <-> Q) |
| T9* | |- ((P->Q)->P)->P Peirce's Law |
| T10* | |- (P->Q) v (Q->R) |
| T11* | |- (P <-> Q) <-> (~ P <-> ~Q) |
| T12* | |- (~P->Q) & (R->Q) <-> (P->R)->Q |
| T13* | |- P <-> P & P & Idempotence |
| T14* | |- P <-> P v P v Idempotence |
| T15 | |- (P <-> Q) & (R <-> S)->((P->R) <-> (Q->S)) |
| T16 | |- (P <-> Q) & (R <-> S)->(P & R <-> Q & S) |
| T17* | |- (P <-> Q) & (R <-> S)->(P v R <-> Q v S) |
| T18 | |- (P <-> Q) & (R <-> S)->((P <-> R) <-> (Q <-> S)) |
| T19* | |- (P <-> Q)-> ((R->P) <-> (R->Q)) & ((P->R) <-> (Q->R)) |
| T20 | |- (P <-> Q)->(R & P <-> R & Q) |
| T21* | |- (P <-> Q)->(R v P <-> R v Q) |
| T22 | |- (P <-> Q)->((R <-> P) <-> (R <-> Q)) |
| T23 | |- P & (Q <-> R)->(P & Q <-> R) |
| T24 | |- P->(Q->R) <-> ((P->Q)->(P->R)) |
| T25 | |- P->(Q->R) <-> Q->(P->R) |
| T26 | |- P->(P->Q) <-> P->Q |
| T27* | |- (P->Q)->Q <-> (Q->P)->P |
| T28 | |- P->~Q <-> Q->~P |
| T29 | |- ~P->P <-> P |
| T30* | |- (P & Q) v (R & S) <-> ((P v R) & (P v S)) & ((Q v R) & (Q v S)) |
| T31* | |- (P v Q) & (R v S) <-> ((P & R) v (P & S)) v ((Q & R) v (Q & S)) |
| T32* | |- (P->Q) & (R->S) <-> ((~P & ~R) v (~P & S)) v ((Q & ~R) v (Q & S)) |
| T33 | |- (P v ~P) & Q <-> Q |
| T34 | |- (P & ~P) v Q <-> Q |
| T35 | |- P v (~P & Q) <-> P v Q |
| T36 | |- P & (~P v Q) <-> P & Q |
| T37 | |- P <-> P v (P & Q) |
| T38 | |- P <-> P & (P v Q) |
| T39 | |- (P->Q & R)->(P & Q <-> P & R) |
|
|
| theorems as derived rules |
Comment.We now consider a special case
of the use of sequents as derived rules. Since it is the
conclusion of a sequent without premises, a theorem or a substitution
instance of a theorem can be written as a line of a proof with an empty
assumption set. For a theorem to be used this way, it must have been
proved already by means of primitive rules alone. The annotation should be
the name of the theorem or T# (the theorem's number). If a substitution
instance is introduced, the substitution pattern should also be included in
the annotation.
|
|
|
| Example. |
| Prove P->Q, ~P->Q |- Q. |
| 1 (1) P->Q A |
| 2 (2) ~P->Q A |
| (3) P v ~P T2 |
| 1,2 (4) Q 1,2,3 SimDil |
|
|
| Comment. In the preceding example, the annotation for line 3
gives the number of the theorem introduced. Since this theorem has a name,
the annotation `Excluded Middle' would also have been acceptable. |
| Comment. As with sequent introductions, requiring that theorems
first be proved using only primitive rules is unnecessarily
restrictive. |
|
|
|
| Exercise 1.8 |
Prove the following using either primitive or
derived rules from the previous exercises. If you like a challenge, prove
them again using primitive rules only.
|
|
|
| S54 | ~P->P -| |- P |
| S55 | P <-> Q -| |- ~((P->Q)->~(Q->P)) |
| S56* | P <-> Q -| |- P v Q->P & Q |
| S57* | P <-> Q -| |- ~(P v Q) v ~(~P v ~Q) |
| S58 | P <-> Q -| |- ~(P & Q)->~(P v Q) |
| S59 | P <-> Q -| |- ~(~(P & Q) & ~(~P & ~Q)) |
| S60 | P v Q->R & ~P , Q v R, ~R |- C |
| S61 | ~P <-> Q, P->R, ~R |- ~Q <-> R |
| S62 | ~((P <-> ~Q) <-> R), S->P & (Q & T), R v (P
& S) |- S & K->R & Q |
| S63* | (P & Q) v (R v S) |- ((P & Q) v R) v S |
| S64 | P & (~Q & ~R), P->(~S->T), ~S->(T <-> R v Q)
|- S |
| S65 | P & ~Q->~R, (~S->~P) <-> ~R |- R <-> Q & (P & ~S) |
| S66* | P v Q, (Q->R) & (~P v S), Q & R->T |- T v S |
| S67 | P->Q v R, (~Q & S) v (T->~P), ~(~R->~P) |- ~T & Q |
| S68* | P v Q, P->(R->~S), (~R <-> T)->~P |- S & T->Q |
| S69* | (P <-> ~Q)->~R, (~P & S) v (Q & T), S v T->R |- Q->P |
| S70* | ~S v (S & R), (S->R)->P |- P |
| S71* | P v (R v Q), (R->S) & (Q->T), S v T->P v Q, ~P |- Q |
| S72* | (P->Q)->R, S->(~Q->T) |- R v ~T->(S->R) |
| S73* | P & Q->R v S |- (P->R) v (Q->S) |
| S74* | (P->Q) & (R->P), (P v R) & ~(Q & R) |- (P & Q) & ~R |
| S75* | P & Q->(R v S) & ~(R & S), R & Q->S,
S->((R & Q) v (~R & ~Q)) v ~P |- P->~Q
|
| S76 | ~(P & ~Q) v ~(~R & ~S), ~S & ~Q, T->(~S->~R & P) |- ~T |
|
|
|