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 :
- Valid sequents of SL
- Sequents not in SL, but are truth-functionally valid
- All other valid sequents
§1. Valid sequents of SL are still valid in MPL
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 :
- P ⊧ P
- (P&Q) ⊧ P
- P, (P→Q) ⊧ Q
- P, (~P∨Q) ⊧ Q
§2. Truth-functional validity in MPL
How about these sequents which can only be found in MPL?
- ∃zFz ⊧ ∃zFz
- (~Ca&Gb) ⊧ ~Ca
- Ka, (Ka→∀yDy) ⊧ ∀yDy
- ∃xWx, (~∃xWx∨Fc) ⊧ Fc
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 :
Definition of truth-functional validity in MPL
Suppose we have a valid sequent φ in SL.
- Take any number N of distinct sentence letters α1, α2, ...αN that appear in φ.
- Take N WFFs of MPL β1, β2, ...βN, none of which contain sentence letters that appear in φ.
- Now replace all occurrences of α1 by β1, and replace all occurrences of α2 by β2, ... , and replace all occurrences of αN by βN.
- If the original sequent φ is a valid sequent in SL, then the resulting new sequent after replacement is also a truth-functionally valid sequent in MPL.
So let us apply this rule once to see how it works. Consider this valid sequent φ in SL : (P→Q), (Q→R) ⊧ (P→R)
- Take 2 distinct sentence letters "P" and "R" that appear in the sequent.
- Take 2 WFFs of MPL : "∀x(Fx&Gx)", "~S", none of which contain sentence letters that appear in φ (i.e. no "P" or "R").
- Replace all occurrences of "P" in φ by "∀x(Fx&Gx)". Replace all occurrences of "R" by "~S".
- We end up with a new valid sequent : (∀x(Fx&Gx)→Q), (Q→~S) ⊧ (∀x(Fx&Gx)→~S)
Here are two more examples of truth-functionally valid sequents in MPL :
- Start with this valid sequent in SL : (P∨Q), ~Q ⊧ P
- Replacement scheme : P ⇒ ∃xFx, Q ⇒ He
- Result: (∃xFx∨He), ~He ⊧ ∃xFx
- Start with this valid sequent in SL : (P&~Q) ⊧ ~(P↔Q)
- Replacement scheme : P ⇒ ∀x(Gx&Fx)
- Result: (∀x(Gx&Fx)&~Q) ⊧ ~(∀x(Gx&Fx)↔Q)
Show that these sequents are truth-functionally valid by identifying the replacement schemes and the SL-valid sequents from which they can be derived :
- (P↔∃xGx), ~~~∃xGx ⊧ ~P
- (∀xFx→S), (P→Gb) ⊧ (~(∀xFx&P)∨(S&Gb))