Appendix B Alternative proof systems

In formulating our natural deduction system, we treated certain rules of natural deduction as basic, and others as derived. However, we could equally well have taken various different rules as basic or derived. We will illustrate this point by considering some alternative treatments of disjunction, negation, and the quantifiers. We will also explain why we have made the choices that we have.

B.1 Alternative disjunction elimination

Some systems take DS as their basic rule for disjunction elimination. Such systems can then treat the $\vee$ E rule as a derived rule. For they might offer the following proof scheme:

Line number	Subproof level	Formula	Justification
$m$	0	$\mathscr{A}\vee\mathscr{B}$
$i$	open subproof, 1	$\mathscr{A}$	AS
$j$	1	$\mathscr{C}$
$k$	close subproof, open subproof, 1	$\mathscr{B}$	AS
$l$	1	$\mathscr{C}$
$n$	close subproof, 0	$\mathscr{A}\rightarrow\mathscr{C}$	$\rightarrow$ I $i$ – $j$
$n+1$	0	$\mathscr{B}\rightarrow\mathscr{C}$	$\rightarrow$ I $k$ – $l$
$n+2$	open subproof, 1	$\neg\mathscr{C}$	AS
$n+3$	open subproof, 2	$\mathscr{A}$	AS
$n+4$	2	$\mathscr{C}$	$\rightarrow$ E $n+3$ , $n$
$n+5$	2	$\bot$	$\neg$ E $n+2$ , $n+4$
$n+6$	close subproof, 1	$\neg\mathscr{A}$	$\neg$ I $n+3$ – $n+5$
$n+7$	1	$\mathscr{B}$	DS $m$ , $n+6$
$n+8$	1	$\mathscr{C}$	$\rightarrow$ E $n+7$ , $n+1$
$n+9$	1	$\bot$	$\neg$ E $n+2$ , $n+8$
$n+10$	close subproof, 0	$\mathscr{C}$	IP $n+2$ – $n+9$

So why did we choose to take $\vee$ E as basic, rather than DS?¹¹ 1 P. D. Magnus’s original version of this book went the other way. Our reasoning is that DS involves the use of ‘ $\neg$ ’ in the statement of the rule. It is in some sense ‘cleaner’ for our disjunction elimination rule to avoid mentioning other connectives.

B.2 Alternative negation rules

Some systems take the following rule as their basic negation introduction rule:

Line number	Subproof level	Formula	Justification
$m$	open subproof, 1	$\mathscr{A}$	AS
$n-1$	1	$\mathscr{B}$
$n$	1	$\neg\mathscr{B}$
	close subproof, 0	$\neg\mathscr{A}$	$\neg$ I* $m$ – $n$

and a corresponding version of the rule we called IP as their basic negation elimination rule:

Line number	Subproof level	Formula	Justification
$m$	open subproof, 1	$\neg\mathscr{A}$	AS
$n-1$	1	$\mathscr{B}$
$n$	1	$\neg\mathscr{B}$
	close subproof, 0	$\mathscr{A}$	$\neg$ E* $m$ – $n$

Using these two rules, we could we could have avoided all use of the symbol ‘ $\bot$ ’ altogether.²² 2 Again, P. D. Magnus’s original version of this book went the other way. The resulting system would have had fewer rules than ours.

Another way to deal with negation is to use either LEM or DNE as a basic rule and introduce IP as a derived rule. Typically, in such a system the rules are given different names, too. E.g., sometimes what we call $\neg$ E is called $\bot$ I, and what we call X is called $\bot$ E.³³ 3 The version of this book due to Tim Button goes this route and replaces IP with LEM, which he calls TND, for “tertium non datur.”

So why did we chose our rules for negation and contradiction?

Our first reason is that adding the symbol ‘ $\bot$ ’ to our natural deduction system makes proofs considerably easier to work with. For instance, in our system it’s always clear what the conclusion of a subproof is: the sentence on the last line, e.g., $\bot$ in IP or $\neg$ I. In $\neg$ I* and $\neg$ E*, subproofs have two conclusions, so you can’t check at one glance if an application of them is correct.

Our second reason is that a lot of fascinating philosophical discussion has focussed on the acceptability or otherwise of indirect proof IP (equivalently, excluded middle, i.e., LEM, or double negation elimination DNE) and explosion (i.e., X). By treating these as separate rules in the proof system, you will be in a better position to engage with that philosophical discussion. In particular: having invoked these rules explicitly, it would be much easier for us to know what a system which lacked these rules would look like.

This discussion, and in fact the vast majority of mathematical study on applications of natural deduction proofs beyond introductory courses, makes reference to a different version of natural deduction. This version was invented by Gerhard Gentzen in 1935 as refined by Dag Prawitz in 1965. Our set of basic rules coincides with theirs. In other words, the rules we use are those that are standard in philosophical and mathematical discussion of natural deduction proofs outside of introductory courses.

B.3 Alternative quantification rules

An alternative approach to the quantifiers is to take as basic the rules for $\forall$ I and $\forall$ E from chapter 36, and also two CQ rules which allow us to move from $\forall\mathscr{x}\,\neg\mathscr{A}$ to $\neg\exists\mathscr{x}\,\mathscr{A}$ and vice versa.⁴⁴ 4 Warren Goldfarb follows this line in Deductive Logic, 2003, Hackett Publishing Co.

Taking only these rules as basic, we could have derived the $\exists$ I and $\exists$ E rules provided in chapter 36. To derive the $\exists$ I rule is fairly simple. Suppose $\mathscr{A}$ contains the name $\mathscr{c}$ , and contains no instances of the variable $\mathscr{x}$ , and that we want to do the following:

Line number	Subproof level	Formula	Justification
$m$	0	$\mathscr{A}(\ldots\mathscr{c}\ldots\mathscr{c}\ldots)$
$k$	0	$\exists\mathscr{x}\,\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{c}\ldots)$

This is not yet permitted, since in this new system, we do not have the $\exists$ I rule. We can, however, offer the following:

Line number	Subproof level	Formula	Justification
$m$	0	$\mathscr{A}(\ldots\mathscr{c}\ldots\mathscr{c}\ldots)$
$m+1$	open subproof, 1	$\neg\exists\mathscr{x}\,\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{c}\ldots)$	AS
$m+2$	1	$\forall\mathscr{x}\,\neg\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{c}\ldots)$	CQ $m+1$
$m+3$	1	$\neg\mathscr{A}(\ldots\mathscr{c}\ldots\mathscr{c}\ldots)$	$\forall$ E $m+2$
$m+4$	1	$\bot$	$\neg$ E $m+3$ , $m$
$m+5$	close subproof, 0	$\exists\mathscr{x}\,\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{c}\ldots)$	IP $m+1$ – $m+4$

To derive the $\exists$ E rule is rather more subtle. This is because the $\exists$ E rule has an important constraint (as, indeed, does the $\forall$ I rule), and we need to make sure that we are respecting it. So, suppose we are in a situation where we want to do the following:

Line number	Subproof level	Formula	Justification
$m$	0	$\exists\mathscr{x}\,\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{x}\ldots)$
$i$	open subproof, 1	$\mathscr{A}(\ldots\mathscr{c}\ldots\mathscr{c}\ldots)$	AS
$j$	1	$\mathscr{B}$
$k$	close subproof, 0	$\mathscr{B}$

where $\mathscr{c}$ does not occur in any undischarged assumptions, or in $\mathscr{B}$ , or in $\exists\mathscr{x}\,\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{x}\ldots)$ . Ordinarily, we would be allowed to use the $\exists$ E rule; but we are not here assuming that we have access to this rule as a basic rule. Nevertheless, we could offer the following, more complicated derivation:

Line number	Subproof level	Formula	Justification
$m$	0	$\exists\mathscr{x}\,\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{x}\ldots)$
$i$	open subproof, 1	$\mathscr{A}(\ldots\mathscr{c}\ldots\mathscr{c}\ldots)$	AS
$j$	1	$\mathscr{B}$
$k$	close subproof, 0	$\mathscr{A}(\ldots\mathscr{c}\ldots\mathscr{c}\ldots)\rightarrow\mathscr{B}$	$\rightarrow$ I $i$ – $j$
$k+1$	open subproof, 1	$\neg\mathscr{B}$	AS
$k+2$	1	$\neg\mathscr{A}(\ldots\mathscr{c}\ldots\mathscr{c}\ldots)$	MT $k$ , $k+1$
$k+3$	1	$\forall\mathscr{x}\neg\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{x}\ldots)$	$\forall$ I $k+2$
$k+4$	1	$\neg\exists\mathscr{x}\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{x}\ldots)$	CQ $k+3$
$k+5$	1	$\bot$	$\neg$ E $k+4$ , $m$
$k+6$	close subproof, 0	$\mathscr{B}$	IP $k+1$ – $k+5$

We are permitted to use $\forall$ I on line $k+3$ because $\mathscr{c}$ does not occur in any undischarged assumptions or in $\mathscr{B}$ . The entries on lines $k+4$ and $k+1$ contradict each other, because $\mathscr{c}$ does not occur in $\exists\mathscr{x}\,\mathscr{A}(\ldots\mathscr{x}\ldots\mathscr{x}\ldots)$ .

Armed with these derived rules, we could now go on to derive the two remaining CQ rules, exactly as in chapter 40.

So, why did we start with all of the quantifier rules as basic, and then derive the CQ rules?

Our first reason is that it seems more intuitive to treat the quantifiers as on a par with one another, giving them their own basic rules for introduction and elimination.

Our second reason relates to the discussion of alternative negation rules. In the derivations of the rules of $\exists$ I and $\exists$ E that we have offered in this section, we invoked IP. But, as we mentioned earlier, IP is a contentious rule. So, if we want to move to a system which abandons IP, but which still allows us to use existential quantifiers, we will want to take the introduction and elimination rules for the quantifiers as basic, and take the CQ rules as derived. (Indeed, in a system without IP, LEM, and DNE, we will be unable to derive the CQ rule which moves from $\neg\forall\mathscr{x}\,\mathscr{A}$ to $\exists\mathscr{x}\,\neg\mathscr{A}$ .)