Module: Predicate logic
Quote of the page
All life is problem solving.
- Karl Popper
In SL, we can use truth-tables to check the validity of sequents, but this method is not applicable to many of the sentences in MPL, such as the quantified wffs. It is indeed possible to use other methods to prove the validity of a sequent in MPL, or PL, but we shall not discuss them in this introductory course. If you are interested you can look up the more advanced textbooks in the section on further readings.
Basically, we can divide all the valid sequents in MPL into three kinds :
Let us look at the first kind of valid sequents. Since SL is part of MPL, all the valid sequents of SL are also sequents in MPL. Of course these sequents remain valid in MPL. They include :
How about these sequents which can only be found in MPL?
These sequents are actually all valid. Even though they are not sequents of SL, we can see that they are of the same form as the four valid sequents of SL above them. The third sequent, for example, is simply an application of modus ponens.
In other words, if any sequent of MPL has the same form as a valid sequent in SL, then it is also valid in MPL. What we need to do now is to give a more precise definition of this rule :
Suppose we have a valid sequent φ in SL.
So let us apply this rule once to see how it works. Consider this valid sequent φ in SL : (P→Q), (Q→R) ⊧ (P→R)
Here are two more examples of truth-functionally valid sequents in MPL :
Show that these sequents are truth-functionally valid by identifying the replacement schemes and the SL-valid sequents from which they can be derived :