[PL08] Validity

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 :

So let us apply this rule once to see how it works. Consider this valid sequent φ in SL : (P→Q), (Q→R) ⊧ (P→R)

1. Take 2 distinct sentence letters "P" and "R" that appear in the sequent.
2. Take 2 WFFs of MPL : "∀x(Fx&Gx)", "~S", none of which contain sentence letters that appear in φ (i.e. no "P" or "R").
3. Replace all occurrences of "P" in φ by "∀x(Fx&Gx)". Replace all occurrences of "R" by "~S".
4. 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 :

Example #1:

1. Start with this valid sequent in SL : (P∨Q), ~Q ⊧ P
2. Replacement scheme : P ⇒ ∃xFx, Q ⇒ He
3. Result: (∃xFx∨He), ~He ⊧ ∃xFx

Example #2:

1. Start with this valid sequent in SL : (P&~Q) ⊧ ~(P↔Q)
2. Replacement scheme : P ⇒ ∀x(Gx&Fx)
3. Result: (∀x(Gx&Fx)&~Q) ⊧ ~(∀x(Gx&Fx)↔Q)