Shantila's Inside Logic #11

Logical Truths

So far we have proved sequents that have at least one premise. The very first valid sequent we proved, for example, had two premises.

1 P>Q, P } Q

and recall that we proved it easily, using MP, as follows:

1 P>Q, P } Q

On the other hand, the valid sequent

9 ~~Q } Q

has only one premise. Recall its simple one-step proof, using DN:

9 ~~Q } Q

So now this leads to a question. Do sequents always have to have at least one premise?

The answer, perhaps surprisingly, is NO! Notice that because we have the Rule CP, we are completely entitled to write another line to the preceding proof of sequent 9, as follows:

Since in using CP we eliminate one assumption, the move from line 2 to 3 means that line 3 has no assumptions at all! We will say that if a sentence can be proved from no assumptions, that statement is a logical truth (or theorem).

We indicate that a sequent represents a logical truth by writing the } sign with no sentences at all to its left.

48 } ~~Q>Q

This is the proof of the the logical truth ~~Q>Q. The blank space on the left on line 3 indicates that we have been able to derive ~~Q>Q from no assumptions!

Logical truths are statements that are true simply because of the meanings of the core ideas of logic that we have been examining. For example, consider the statement"if it is not true that it is not cold today, then it is cold today." This can be represented as ~~C>C. The English statement is an instance of the logical truth 48 that we just proved. This means that the English statement can be known to be true without knowing anything about the weather outside! Of course the information in the sentence is rather trivial (it doesn't really tell us anything specific about the actual weather today). Nonetheless, it is a true statement, and we can know it is true simply because of the meanings of the core ideas "not" and "if".

Recall that the three core ideas we have explored so far are these:

We now have a rich enough special symbolic language and proof system so that we can prove logical truths that are not trivial and that express interesting connections between these core concepts. For example, the following sequent 49 is a logical truth that expresses the idea that we use in our rule MP. To prove 49 we once again use CP. (Notice how this logical truth corresponds to the valid sequent 1 mentioned at the beginning of this chapter.)

49 } (P&(P>Q))>Q

Using CP, we can see that any of the valid sequents we have proved can be turned into a logical truth, in just the same way that sequent 1 is turned into the logical truth proved using CP in sequent 49.