8.5.3. Derivations for existentials
To implement the laws we have just been considering, we will again use ideas introduced in connection with universals. In particular, a proof by choice will be marked by a veil of ignorance flagged by an independent term, and it will have a supposition that sets out the example chosen. However, the complications that appeared with the rules for exploiting universals may be left with those rules, since we manage planning for an existential conclusion simply by passing the buck on to universals.
The two basic rules for the unrestricted existential are Proof by Choice (PCh) and Non-constructive Proof (NcP):
|
→ |
|
Fig. 8.5.3-1. Developing a derivation at stage n by exploiting an unrestricted existential; the independent term a is new to the derivation.
|
→ |
|
Fig. 8.5.3-2. Developing a derivation at stage n by planning for an unrestricted existential.
Notice that the existential is rendered inactive in the first rule. Also remember that the independent term that is used in this rule should be new to the derivation; that will insure that the supposition that is introduced represents the only information about this independent term that may be used in closing the gap.
The second rule will often be a very indirect way of reaching an existential goal, and the attachment rule, Existential Generalization (EG), which implements the idea of constructive proof, can simplify derivations considerably:
|
Fig. 8.5.3-3. Developing a derivation at stage n by adding an unrestricted existential that has an instance among the active resources.
Although this is an attachment rule and therefore not part of the basic system, you should be as ready to use it as the two above.
Here are two derivations that illustrate these rules. Each shows that a claim of uniformly general exemplification implies the corresponding claim of general exemplification without a claim of uniformity.
The derivation on the left uses a non-constructive proof of the existential that is set as the goal in stage 2 while the one on the right uses EG to give a constructive proof of this existential. Both derivations begin by exploiting the existential premise, but derivations for the same entailment could have been developed by planning for the initial conclusion first; and, when NcP is used, it would be possible to postpone the exploitation of the initial premise until after NcP is applied. (It would be a good exercise at this point to write down these other derivations for this argument.) The savings in length and complexity that were achieved by using EG in this case are typical.
Since EG can be used only when the resources entail an existential, it often cannot be used in derivations that fail, and NcP is required even in some derivations for valid existential conclusions. A derivation showing the obversion principle ¬ ∀x Fx ⊨ ∃x ¬ Fx is simple example of this.
| │¬ ∀x Fx | (2) | |
| ├─ | ||
| ││∀x Fx | (2) | |
| ││● | ||
| │├─ | ||
| 2 Nc | ││⊥ | 1 |
| ├─ | ||
| 1 NcP | │∃x ¬ Fx |
EG could not have been applied here because the premise does not entail any sentence ¬ Fτ from which we could generalize.
|
→ |
|
Fig. 8.5.3-4. Developing a derivation at stage n by exploiting an unrestricted or a restricted existential; the independent term a is new to the derivation and the terms σ, …, τ include at least one from each current alias set for the gap
Arguments for the soundness and completeness of this system carry over from 7.7 without any new wrinkles. We solved all the key problems there, and a number are not even repeated here. However, we cannot avoid the consequences of the failure of decisiveness. If we wish to find finite counterexamples whenever they exist, we need to use a modified rule for exploiting existential resources in the way the rule for planning for a universal goal was modified in 7.8.1. Without such a rule, we will not reach dead-end open gap in any derivation whose resources contain a weak, though unrestricted, claim of general exemplification (e.g., a sentence of the form ∀x ∃y Rxy). The modified rule needed to search for finite counterexamples is Supplemented Proof by Choice (PCh+).
The following derivation illustrates this rule. It shows that a claim of general exemplification need not imply uniformity. That is, it finds a counterexample to the entailment ∀x ∃y Rxy ⊨ ∃y ∀x Rxy.
|
Although this is long and cumbersome, the development of the dead-end gap goes through the kinds steps you would need to go through in your own thinking to arrive the same counterexample (the bracketed numbers link steps in this thinking with the stages of the derivation):
The premise says that everything stands in relation R to something or other. And, to make the conclusion false, we need to know that there is nothing that has everything standing in the relation R to it [1]. So we must have an object a such that a stands in R to something but not everything stands in R to a [2-4]. Now we can’t be sure that a is related to itself; but we can still consider this possibility as one way of making it true that a is related to something by R, so let’s suppose that Raa [5]. But we also need to make it false that everything stands in R to a, so let’s suppose we have an object c that doesn’t stand in R to a [6-8]. Now c must stand in R to something and it can’t have everything standing in R to it [9-11, cf. 2-4]. Let’s try supposing it stands in R to itself (though it might be something else that it is related to) [12]. Now, we must also be sure that not everything stands in R to c, but nothing keeps us from supposing that a does not [13-14]. Summing up, we’ve described a possible world containing objects a and c where Raa, ¬ Rca, Rcc, ¬ Rac; and that’s enough to make the premise true and the conclusion false.
Developing the unfinished gaps would lead to other counterexamples. For example, the last open gap in this derivation explores the possibility of making the premise true by having a stand in R to another object b and it would, among other things, lead us to a counterexample in which each of a and b is stands in R to the other but neither stands in R to itself.