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):

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:

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.

EG could not have been applied here because the premise does not entail any sentence ¬ Fτ from which we could generalize.

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.

│∀x ∃y Rxy a:2, c:9 ├─ ││∀y ¬ ∀x Rxy a:3, c:10 │├─ 2 UI ││∃y Ray 5 3 UI ││¬ ∀x Rxa 4 ││ ││││Raa (7) │││├─ │││││● ││││├─ 7 QED │││││Raa 6 ││││ ││││ⓒ ││││││¬ Rca (15) │││││├─ 9 UI ││││││∃y Rcy 12 10 UI ││││││¬ ∀x Rxc 11 ││││││ ││││││││Rca (15) │││││││├─ ││││││││ⓓ ││││││││││¬ Rdc │││││││││├─ ││││││││││● │││││││││├─ 15 Nc ││││││││││⊥ 14 ││││││││├─ 14 IP │││││││││Rdc 13 │││││││├─ 13 UG ││││││││∀x Rxc 12 │││││││ ││││││││Rcc (18) │││││││├─ ││││││││││¬ Rac │││││││││├─ ││││││││││○ Raa, ¬ Rca, Rcc, ¬ Rac ⊭ ⊥ │││││││││├─ ││││││││││⊥ 17 ││││││││├─ 17 IP │││││││││Rac 16 ││││││││ │││││││││● ││││││││├─ 18 QED │││││││││Rcc 16 ││││││││ ││││││││ⓕ │││││││││(unfinished) ││││││││├─ │││││││││Rec 16 │││││││├─ 16 UG+ ││││││││∀x Rxc 12 │││││││ │││││││ⓔ ││││││││Rcd │││││││├─ ││││││││(unfinished) │││││││├─ ││││││││∀x Rxc 12 ││││││├─ 12 PCh+ │││││││∀x Rxc 11 │││││├─ 11 CR ││││││⊥ 8 ││││├─ 8 IP │││││Rca 6 │││├─ 6 UG+ ││││∀x Rxa 5 │││ │││ⓑ ││││Rab │││├─ ││││(unfinished) │││├─ ││││∀x Rxa 5 ││├─ 5 PCh+ │││∀x Rxa 4 │├─ 4 CR ││⊥ 1 ├─ 1 NcP │∃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:

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.