CS 245 — Lecture 8

Derived rules

As mentioned before, we can consider some helpful rules that are not technically part of the core natural deduction ruleset, but are consequences of the proof system. These rules tend to map onto proof techniques that we use when proving things. Such rules are called derived rules. In theory, we could generate as many derived rules as we have proofs. Obviously, we will stick to a few useful ones.

Example 8.1. We will show that $\{p\} \vdash (\neg (\neg p))$. Recall that this is the "rule" we introduced as $\neg\neg i$.

Example 8.2. We will derive the rule $$\frac{(\alpha \rightarrow \beta) \quad (\neg \beta)}{(\neg \alpha)} \mathrm{MT}$$

This rule is called modus tollens, which is Latin for "mode that denies". We can think of an argument of this form as a form of the contrapositive. We will show $\{(p \rightarrow q), (\neg q)\} \vdash (\neg p)$.

Example 8.3. Another proof technique you should be familiar with is proof by contradiction, which goes by the Latin name reductio ad absurdum. With some work, we can also construct a derived rule from this. $$\frac{\boxed{\begin{matrix} (\neg \alpha) \\ \vdots \\ \bot \end{matrix}}}{\alpha} \textrm{PBC} $$

The idea is very similar to an idea we've encountered before with negation introduction. The derived rule here basically says we can make an assumption $\beta$ stated negatively as $(\neg \alpha) = \beta$, then arrive at a contradiction. Ordinarily, we would then apply $\neg i$ to get $(\neg (\neg \alpha))$, but then obviously, we can apply $\neg\neg e$ right after to get $\alpha$. This rule condenses this process slightly.

Example 8.4. We will show $\emptyset \vdash (((p \rightarrow q) \rightarrow p) \rightarrow p)$.

Observe that, since these are derived rules, we don't really need them and we can come up with alternate proofs that only use our basic rules of natural deduction.

Example 8.5. The final derived rule we'll be looking at is the law of excluded middle which also has a fancy Latin name, tertium non datur. As an inference rule, it looks like this. $$\frac{}{(\alpha \vee (\neg \alpha))} \textrm{LEM}$$

The idea behind this rule is that either we have $\alpha$ or we have $(\neg \alpha)$. There is no third (or "middle") possibility.

We will show that $\emptyset \vdash (p \vee (\neg p))$.

Example 8.6. Let's see how LEM might be helpful. We will show the other direction of the implication identity, $\{(p \rightarrow q)\} \vdash ((\neg p) \vee q)$. First, we will show that we can do this without LEM.

And the following is a proof with LEM.

Loose ends and other remarks

You may have noticed that we were able to derive a proof of the form $\emptyset \vdash \varphi$ for some formula $\varphi$. In particular, the law of excluded middle looks very familiar when rendered as $\emptyset \vdash (\alpha \vee (\neg \alpha))$. This, of course, should be an immediate callback to our trip through semantic entailment and the notion that $\emptyset \models (\alpha \vee (\neg \alpha))$ means that $(\alpha \vee (\neg \alpha))$ is a tautology. We already have the similar notion of contradiction in our proof system, so what does it mean for a formula to be provable without any premises?

Formulas $\varphi$ such that $\emptyset \vdash \varphi$ are called theorems. To see why this might be the case, we can think of the following proof for $\{p\} \vdash (q \rightarrow p)$.

This proof may look familiar to you if you remember back to when we first started talking about rules for implication. But first, let's think about what the statement $\{p\} \vdash (q \rightarrow p)$ means. We can think of this as saying given $p$, we can prove $(q \rightarrow p)$. That, of course, sounds a lot like the statement if $p$, then $(q \rightarrow p)$. And in fact, this formulation of the statement would look like $\emptyset \vdash (p \rightarrow (q \rightarrow p))$, which we proved as Example 7.1.

In other words, we can take any proof sequent, and start pushing the premises over to the right hand side and turn the formula into an implication. All we would need to do to change the proof would be to package up the proof into boxes appropriately. In fact, we can repeat this process for any number of premises we wish and in any order we wish. If we had $\{\varphi_1, \varphi_2, \dots, \varphi_k\} \vdash \psi$, we can start pushing each $\varphi_i$ over to the right hand side to get a statement $\emptyset \vdash (\varphi_1 \rightarrow (\varphi_2 \rightarrow \dots (\varphi_k \rightarrow \psi) \dots ))$.

Again, this notion matches our intution for how we go about proving a "real" theorem and how we might structure such a proof. We begin with some assumptions, work through some facts, and reach a conclusion. And we can frame such a theorem in either way, whether it's given $p_1, p_2, \dots, p_k$ or it's if $p_1, p_2, \dots, p_k$.

So it is fairly obvious that "proofs" have a connection with proofs and theorems, but what else is there? Where this discussion becomes more relevant is if we make the connection between proofs and programs. I mentioned before that historically, the development of these proof systems was meant to separate what we might consider the human aspect of proving mathematics and being able to automate or mechanicalize the entire thing. Of course, in the early 20th century, such machines were conceptual and no one really imagined building a machine that could do this sort of stuff except maybe in the old-timey steampunk kind of way. However, the Curry-Howard isomorphism makes this connection between proof systems and models of computation explicit. What you will find is that several proof systems are essentially the same as a particular model of computation in the sense that the inference rules that define either system can be translated from one to the other.