Natural Deduction Proofs in QL

Trees employ a kind of 'brute force' strategy for proving entailment claims. When the logical structure of the relevant sentences are rather simple, as they are in SL and in some QL cases, it can be an effective strategy, but in some cases they can become very tedious and complex. It is useful to have a proof system that allows one to reason in a more targeted way --- especially if you already have an intuitive understanding of why a given argument should be expected to turn out valid. As we did in Chapter 7 for SL, in this chapter we will consider a natural deduction system for quantified logic. As in the case of trees, our QL natural deduction system is an extension of the one we learned previously for SL.

Like our SL natural deduction system, our system can only be used to demonstrate that an argument is valid. We do not have a formal method, as part of our natural deduction system, for demonstrating an argument invalid. In this respect natural deduction differs from trees. We won't go through the proof in this book, but the natural deduction is both sound and complete. That means that there are natural deductions proofs corresponding to all and only the valid arguments in QL.

13.1 Natural Deduction: the basics

In a natural deduction system, one begins by writing down the assumptions one begins with --- these correspond to the premises of an argument --- then adds a series of additional sentences, justified via a series of particular rules by the sentences above. Additional assumptions may be made and discharged along the way. If one succeeds in writing down the conclusion of the argument on a new line, with no additional undischarged assumptions, consistent with the natural deduction rules, one has proven that the conclusion follows from those premises. If you need a refresher on how that works, review Chapter 7.

Our QL system will use all the same sentential rules that our SL system did. All the introduction and elimination rules for the sentential connectives, as well as the derived and replacement rules, will be part of this system too. (These are summarized, along with our new rules, in the Quick Reference guide at the end of this book.) We'll add introduction and elimination rules for the existential and universal quantifiers, and some other derived rules as well.

13.2 Basic quantifier rules

Recall the relationship between quantified sentences and their instances. The sentence Pa is a particular instance of the general claim ∀xPx. For any wff Φ, constant c, and variable 𝓍, we define Φ[𝓍⇒c] to mean the wff that we get by replacing every occurrence of 𝓍 in Φ with c. Φ[𝓍⇒c] is called a substitution instance of ∀xΦ and ∃xΦ, and is called the instantiating constant. This should be familiar from our discussion of our tree rules for quantifiers in Chapter 10. We will also use this notation to describe our quantifier rules.

13.2.1 Universal elimination

If you have ∀xAx, it is legitimate to infer, of anything, that it is A. You can infer Aa, or Ab, or Az, or Ad₃, etc.. This is, you can infer any substitution instance -- in short, you can infer Ac for any constant c. This is the general form of the universal elimination rule (∀E):

Remember that the box mark for a substitution instance is not a symbol of QL, so you cannot write it directly in a proof. Instead, you write the substituted sentence with the constant c replacing all occurrences of the variable 𝓍 in Φ, as in this example:

This rule is very similar to the tree rule for universals, which, in our tree system, allowed one to develop a branch containing a universal with any instance of it one likes. Here you are permitted to write down any instance you like on a new line.

13.2.2 Existential introduction

When is it legitimate to infer ∃xAx? If you know that something is an A --- for instance, if you have Aa available in the proof.

This is the existential introduction rule (∃I):

It is important to notice that Φ[[𝓍⇒c]] is not necessarily a substitution instance. We write it with double boxes (or double "[[" and "]]", to make it a bit easier) to show that the variable does not need to replace all occurrences of the constant c. You can decide which occurrences to replace and which to leave in place. For example, each of lines 2--6 can be justified by ∃I:

13.2.3 Universal introduction

A universal claim like ∀xPx would be proven if every substitution instance of it had been proven, if every sentence Pa, Pb, … were available in a proof. Alas, there is no hope of proving every substitution instance. That would require proving Pa, Pb, …, Pj₂, …, Ps₇, …, and so on to infinity. There are infinitely many constants in QL, and so this process would never come to an end.

Consider a simple argument: ∀xMx,  ∴ ∀yMy

It makes no difference to the meaning of the sentence whether we use the variable x or the variable y, so this argument is obviously valid. Suppose we begin in this way:

We have derived Ma. Nothing stops us from using the same justification to derive Mb, …, Mj₂, …, Ms₇, …, and so on until we run out of space or patience. We have effectively shown the way to prove Mc for any constant c. From this, ∀yMy follows.

It is important here that a was just some arbitrary constant. We had not made any special assumptions about it. If a had already been mentioned, say as a premise in the argument, then this would not show anything about all y. For example:

This is the schematic form of the universal introduction rule (∀I):

^* The constant must not occur in any undischarged assumption.

Note that we can do this for any constant that does not occur in an undischarged assumption and for any variable.

Note also that the constant may not occur in any undischarged assumption, but it may occur as the assumption of a subproof that we have already closed. For example, here is a valid proof of ∀z(Dz⊃Dz) that does not use any premises.

13.2.4 Existential elimination

A sentence with an existential quantifier tells us that there is some member of the UD that satisfies a formula. For example, ∃xSx tells us (roughly) that there is at least one S. It does not tell us which member of the UD satisfies S, however. We cannot immediately conclude Sa, Sf₂₃, or any other substitution instance of the sentence. What can we do?

Suppose that we knew both ∃xSx and ∀x(Sx⊃Tx). We could reason in this way:

Since ∃xSx, there is something that is an S. We do not know which constants refer to this thing, if any do, so call this thing 'Ishmael'. From ∀x(Sx⊃Tx), it follows that if Ishmael is an S, then it is a T. Therefore, Ishmael is a T. Because Ishmael is a T, we know that ∃xTx.

In this paragraph, we introduced a name for the thing that is an S. We gave it an arbitrary name ('Ishmael') so that we could reason about it and derive some consequences from there being an S. Since 'Ishmael' is just a bogus name introduced for the purpose of the proof and not a genuine constant, we could not mention it in the conclusion. Yet we could derive a sentence that does not mention Ishmael; namely, ∃xTx. This sentence does follow from the two premises.

We want the existential elimination rule to work in a similar way. Yet since English language worlds like 'Ishmael' are not symbols of QL, we cannot use them in formal proofs. Instead, just as we did in the analogous rule within our tree system, we will use names that are new --- names which do not appear anywhere else in the proof. (This includes the conclusion you are aiming for.)

A constant that is used to stand in for whatever it is that satisfies an existential claim is called a proxy. Reasoning with the proxy must all occur inside a subproof, and the proxy cannot be a constant that is doing work elsewhere in the proof.

This is the schematic form of the existential elimination rule (∃E):

^* The constant must not appear outside the subproof.

Remember that the proxy constant cannot appear in Ψ, the sentence you prove using ∃E. (It would actually be enough just to require that the proxy constant not appear in ∃𝓍Φ, in Ψ, or in any undischarged assumption. In recognition of the fact that it is just a place holder that we use inside the subproof, though, we require an entirely new constant which does not appear anywhere else in the proof.)

The existential elimination rule, like the rules for conditional introduction and negation introduction and elimination, is a rule that involves discharging an assumption. Assume a proxy instance, and see what would follow from that instance; if you have the existential, then, you can stop making the assumption about the proxy, and help yourself to what would have followed from it. As with those other assumption-involving rules, instead of a justification, one includes a note --- in this case, 'for ∃E' --- about the role of the assumption in the proof. Remember that assumptions must be discharged before your proof is complete, so you should only make an assumption that goes beyond your premises when you have a plan for discharging it.

With this rule, we can give a formal proof that ∃xSx and ∀x(Sx⊃Tx) together entail ∃xTx.

13.2.4 Quantifier negation

¬∃𝓍¬Φ is logically equivalent to ∀𝓍Φ. The first says that nothing falsifies Φ; the second says everything satisfies Φ. In QL, they are provably equivalent. Here is a proof schema for half of that equivalence via a natural deduction reductio. For any wff Φ, variable 𝓍, and new name a:

^* Where name a does not appear outside the subproof.

This is a proof schema --- it is not itself a proof in QL, as its lines are not QL sentences. But it describes how a proof of this form can be given. For example, here is one instance of the above schema:

(Note that this proof encodes the same form of reasoning one would employ to demonstrate via a tree that ∀yAy ⊨ ¬∃y¬Ay. As an exercise: draw out the tree to compare it.)

In order to fully demonstrate that ¬∃𝓍¬Φ is logically equivalent to ∀𝓍Φ, we would also need a second proof that assumes ¬∃𝓍¬Φ and derives ∀𝓍Φ. We leave that proof as an exercise for the reader.

It will often be useful to translate between quantifiers by adding or subtracting negations in this way, so we add two derived rules for this purpose. These rules are called quantifier negation (QN):

QN is a replacement rule. Like our SL replacement rules (DeMorgan, Double Negation, etc.), it can be used on whole sentences or on subformulae.

13.3 Identity Introduction

The introduction rule for identity is very simple. Everything is identical to itself; so, for any name , one may write --- regardless of what one has on the previous lines of the proof --- that a = a:

The =I rule is unlike our other rules in that it does not require referring to any prior lines of the proof. We need only cite the rule itself; it does not reference any previous line numbers.

13.4 Identity Elimination

If you have shown that a = b, then anything that is true of a must also be true of b. For any sentence with a in it, you can replace some or all of the occurrences of a with b and produce an equivalent sentence. For example, if you already know Raa, then you are justified in concluding Rab, Rba, Rbb. Recall that Φ[[a⇒b]] is the sentence produced by replacing a in with b. This is not the same as a substitution instance, because b may replace some or all occurrences of a. The identity elimination rule (=E) justifies replacing terms with other terms that are identical to it:

Here is a simple proof of an instance of the transitivity of identity. Let's prove that if a = b and b = c, then a = c:

At line 4, we took advantage of the identity claim b = c on line 3, and replaced the b in line 2 with a c. Then we used the familiar ⊃I rule to discharge the assumption of line 1, proving the conditional we were aiming for.

13.5 Translation and evaluation

Consider this argument: There is only one button in my pocket. There is a blue button in my pocket. So there is no non-blue button in my pocket.

We begin by defining a symbolization key:

UD: buttons in my pocket
Bx: x is blue

Because we have no need to discuss anything other than buttons in my pocket, we've restricted the UD accordingly. If we included other things (buttons elsewhere and/or things other than buttons), we'd need predicates corresponding to being a button and things' locations. The simple version here is adequate for our present needs. The argument is translated as:

1. ∀x∀y x = y
2. ∃xBx
3. ∴ ¬∃x¬Bx

So the set-up for a natural deduction proof will be:

There are various strategies one might employ. Here are two clues that point toward one promising strategy. Note again that we have an existential on line 2 --- this suggests existential elimination as a possible strategy. Note also that we are aiming for ¬∃x¬Bx, which equivalent to ¬¬∀xBx by QN. This in turn is equivalent, by DN, to ∀xBx, which suggests that universal introduction is going to be an important step. If we introduce an assumption with a proxy instance of ∃xBx, we'll be able to work toward a generic instance of Bx. In this example, we'll take e as our proxy, and show that Bf follows from ∃xBx:

By line 7, we have discharged the assumption about the proxy --- we won't use the name e any more --- we have established that Bf follows from the two premises. Since f is an arbitrary name --- one that does not appear in any undischarged assumption --- we can perform universal introduction on that instance. This in turn lets us complete the proof via the two substitution rules mentioned above:

13.6 Natural deduction strategy

All the strategy advice given in Section 7.12 is equally applicable to natural deduction proofs in QL. Review the suggestions there for general advice for natural deduction proofs. Applied to our new QL rules, if you have a universal, you can think about taking any instances that look useful. (Taking random instances is unlikely to be useful.) If you have an existential, consider using the existential elimination rule, which begins by assuming an instance with a proxy, then deriving a conclusion that does not contain that proxy name.

Showing ¬∃xΦ can also be hard, and it is often easier to show ∀x¬Φ and use the QN rule.

13.6 Soundness and completeness

The proofs for soundness and completeness of our natural deduction system are beyond the scope of this textbook. But if you are interested in thinking through how those proofs would go, here are a few hints to get you started. Soundness in a natural deduction system amounts to the claim that if any sentence Φ is derivable from a set of sentences 𝒳, then 𝒳 ⊨ Φ. To prove this, you would need to demonstrate that any possible natural deduction proof meets this constraint. This is trivial for 'proofs' that only contain premises; you'd next have to show, for every possible way of extending the proof (i.e., everything permitted by any one of our rules), that any newly added lines with no undischarged assumptions are entailed by the premises.

Undischarged assumptions would require special treatment. You can think of an assumption as being similar to a 'temporary premise' --- what you really want to prove is that, for every possible line in a proof, that line is entailed by the premises in addition to any undischarged assumptions.

The completeness proof is more complex. We need some way to guarantee that there is a proof corresponding to every QL entailment. The way to do this is to find an algorithmic procedure that is guaranteed to find a proof if one exists, and to prove that this is so. One good way to do this is to take advantage of the proven completeness of our tree system for QL, presented in Chapter 11, and find a way to demonstrate that any tree proof can be converted to a natural deduction proof. Here is a hint if you'd like to undertake that project: the tree method encodes the same kind of reasoning that reductio proofs do.

Practice Exercises

Here is a set of instructions about how to use the natural deduction proof construction/checking tool.

Also, if you click here, you can find a slightly more user-friendly version (including real-time rendering of your proofs) of the below exercises.

Part A Provide a justification (rule and line numbers) for each line of proof that requires one.

Part B Provide a natural deduction proof of each claim.

Part C Provide a proof of the argument about Billy from Chapter 8:

The hospital will only hire a skilled surgeon. All surgeons are greedy. Billy is a surgeon, but is not skilled. Therefore, Billy is greedy, but the hospital will not hire him.

Part D Look back at Part E from Chapter 8. Provide proofs to show that each of the argument forms is valid in QL.

Part E Provide a natural deduction proof of each claim.

Part F Show that each pair of sentences is provably equivalent.

1. ∀x(Ax⊃¬Bx), ¬∃x(Ax& Bx)

2. ∀x(¬Ax⊃Bd), ∀xAx ∨ Bd

3. ∃xPx ⊃ Qc, ∀x(Px⊃Qc)

Here is a blank proof box for you to check your work in:

Part G Show that each of the following is provably inconsistent.

1. {Sa ⊃ Tm, Tm ⊃ Sa, Tm& ¬Sa}

2. {¬∃xRxa, ∀x∀yRyx}

3. {¬∃x∃yLxy, Laa}

4. {∀x(Px⊃Qx), ∀z(Pz⊃Rz), ∀yPy, ¬Qa & ¬Rb}

Part H Write a symbolization key for the following argument, translate it, and prove it:

There is someone who likes everyone who likes everyone that first person likes. Therefore, there is someone who likes themself.

Part I Provide a proof of each claim.

1. {Pa ∨ Qb, Qb ⊃ b = c, ¬Pa} ⊢ Qc

2. {m = n ∨ n = o, An} ⊢ Am ∨ Ao

3. {∀x x = m, Rma} ⊢ ∃xRxx

4. ¬∃x x ≠ m ⊢ ∀x∀y(Px⊃Py)

5. ∀x∀y(Rxy⊃x=y) ⊢ Rab ⊃ Rba

6. {∃xJx, ∃x¬Jx} ⊢ ∃x∃y x ≠ y

7. {∀x(x=n⊃Mx), ∀x(Ox∨¬Mx)} ⊢ On

8. {∃xDx, ∀x(x=p⊃Dx)} ⊢ Dp

9. {∃x[Kx& ∀y(Ky⊃x=y)& Bx], Kd} ⊢ Bd

10.  ⊢ Pa ⊃ ∀x(Px∨x≠a)

Here is a proof box to work in:

Part J For each of the following pairs of sentences: If they are logically equivalent in QL, give proofs to show this. If they are not, construct a model to show this.

1. ∀xPx ⊃ Qc, ∀x(Px⊃Qc)

2. ∀xPx& Qc, ∀x(Px& Qc)

3. Qc ∨ ∃xQx, ∃x(Qc∨Qx)

4. ∀x∀y∀zBxyz, ∀xBxxx

5. ∀x∀yDxy, ∀y∀xDxy

6. ∃x∀yDxy, ∀y∃xDxy

Part K For each of the following arguments: If it is valid in QL, give a proof. If it is invalid, construct a model to show that it is invalid.

1. ∀x∃yRxy,  ∃y∀xRxy

2. ∃y∀xRxy,  ∀x∃yRxy

3. ∃x(Px& ¬Qx),  ∀x(Px⊃¬Qx)

4. ∀x(Sx⊃Ta), Sd,  Ta

5. ∀x(Ax⊃Bx), ∀x(Bx⊃Cx),  ∀x(Ax⊃Cx)

6. ∃x(Dx∨Ex), ∀x(Dx⊃Fx),  ∃x(Dx& Fx)

7. ∀x∀y(Rxy∨Ryx),  Rjj

8. ∃x∃y(Rxy∨Ryx),  Rjj

9. ∀xPx ⊃ ∀xQx, ∃x¬Px,  ∃x¬Qx

10. ∃xMx ⊃ ∃xNx, ¬∃xNx,  ∀x¬Mx

Part L Look at the arguments given in Chapter 10, Problem Part C. For those arguments whose QL translations are valid, prove their validity via natural deduction.

Part M Look at the entailment claims given in Chapter 12, Problem Part F. For those entailment claims that are true, prove them via natural deduction.

Part N Look at the arguments given in Chapter 12, Problem Part H. For those arguments whose QL translations are valid, prove their validity via natural deduction.