Extended Rule of Implication

Theorem

Any sequent can be expressed as a theorem.

That is:

$p_1, p_2, p_3, \ldots, p_n \vdash q$

means the same thing as:

$\vdash p_1 \implies \left({p_2 \implies \left({p_3 \implies \left({\ldots \implies \left({p_n \implies q}\right) \ldots }\right)}\right)}\right)$

The latter expression is known as the corresponding conditional of the former.

Proof

From the Rule of Conjunction, we note the following.

Any sequent:

$p_1, p_2 \vdash q$

can be expressed as:

$p_1 \land p_2 \vdash q$

Also, from the Rule of Simplification, any sequent:

$p_1 \land p_2 \vdash q$

can be expressed as:

$p_1, p_2 \vdash q$

Let us take the expression:

$p_1, p_2, p_3, \ldots, p_{n-1}, p_n \vdash q$

By repeated application of the above, we can arrive at:

$p_1 \land \left({p_2 \land \left({p_3 \land \left({\ldots \land \left({p_{n-1} \land p_n}\right) \ldots }\right)}\right)}\right) \vdash q$

For convenience, we can use a substitution instance to substitute $r_1$ for:

$p_2 \land \left({p_3 \land \left({\ldots \land \left({p_{n-1} \land p_n}\right) \ldots}\right)}\right)$

to get:

$p_1 \land r_1 \vdash q$

From the Rule of Implication, we get:

$\vdash \left({p_1 \land r_1}\right) \implies q$

Using the Rule of Exportation, we then get:

$\vdash p_1 \implies \left({r_1 \implies q}\right)$

Then we can substitute back for $r_1$, to get:

$\vdash p_1 \implies \left({\left({p_2 \land \left({p_3 \land \left({\ldots \land \left({p_{n-1} \land p_n}\right) \ldots}\right)}\right)}\right) \implies q}\right)$

Now we make a substitution of convenience again. We substitute $r_2$ for:

$p_3 \land \left({\ldots \land \left({p_{n-1} \land p_n}\right) \ldots}\right)$

We can then take the expression:

$\left({p_2 \land r_2}\right) \implies q$

and express it as:

$p_2 \land r_2 \vdash q$

and use the Rule of Exportation to get:

$p_2 \implies \left({r_2 \implies q}\right)$

which, substituting back for $r_2$, gives us:

$p_2 \implies \left({\left({p_3 \land \left({\ldots \land \left({p_{n-1} \land p_n}\right) \ldots}\right)} \right) \implies q}\right)$

Similarly:

$\left({p_3 \land \left({\ldots \land \left({p_{n-1} \land p_n}\right) \ldots}\right)}\right) \implies q$

converts to:

$p_3 \implies \left({\left({\ldots \land \left({p_{n-1} \land p_n}\right) \ldots}\right) \implies q}\right)$

The pattern becomes apparent. Eventually we reach:

$\left({p_{n-1} \land p_n}\right) \implies q$

which converts to:

$p_{n-1} \implies \left({p_n \implies q}\right)$

We can substitute these back into our original expression and get:

$\vdash p_1 \implies \left({p_2 \implies \left({p_3 \implies \left({\ldots \implies \left({p_n \implies q}\right) \ldots }\right)}\right)}\right)$

$\blacksquare$

Comment

This shows us that every sequent containing the symbol $\vdash$ can, if so desired, be expressed in the form of a theorem which has $\implies$.

Some authors ignore the $\vdash$ concept, and construct their exposition of PropLog using $\implies$ instead. This is a completely valid approach, and appears to have been gaining favour in more recent years, particularly in the field of computability.

Sources

• Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems (2000): $\S 1.2.1$: Remark $1.12$