The Logic Book, M. Bergmann, J. Moor, J. Nelson, McGraw Hill, 4th edition, 2004, Ex. 10.5, 3(d)

The task is to show that the statement: (x)(Ax ⊃Bx) ∨(∃x)Ax, is a theorem of predicate logic. Before we show the workings, we can reason like this: let 'Ax' be 'x' is a tiger; 'Bx' - 'x' is a man-eater. Then, we have: Either all tigers are man-eaters or tigers exist. Since the statement is a disjunction, it is false if and only if both disjuncts are false. If there is a tiger that is not a man-eater, our left disjunct will be false, but that still makes the whole sentence true, because tigers do exist. If we let: 'Ax' be 'x' is a unicorn, and 'Bx' - 'x' is white, then the existential claim on the right is of course false, but the universal claim on the left is true. Precisely because no unicorns exist, the statement: All unicorns are white, is true. So again, we have failed to force both disjuncts to be false.

In proving this theorem we can go a number of ways. We can assume the negation of one of the disjuncts (doesn't matter which), then discharge the assumption and simplify, or we can negate the whole theorem and show a contradiction. Both methods follow.

Show: (x)(Ax ⊃Bx) ∨(∃x)Ax

1. * ¬ (∃x)Ax / ACP
2. * (x) ¬ Ax / 1CQ
3. * ¬ Ax / 2UI x/x
4. * ¬ Ax ∨Bx / 3Add.
5. * Ax ⊃Bx / 4MI
6. * (x)(Ax ⊃Bx) / 5UG
7. ¬ (∃x)A x ⊃ (x)(Ax ⊃Bx) / 1-6CP
8. (∃x)A x ∨ (x)(Ax ⊃Bx) / 7MI
9. (x)(Ax ⊃Bx) ∨(∃x)Ax / 8Comm.
   

Show: (x)(Ax ⊃Bx) ∨(∃x)Ax

1. * ¬ [(x)(Ax ⊃Bx) ∨(∃x)Ax] / AIP
2. * ¬ (x)(Ax ⊃Bx) • ¬ (∃x)Ax / 1DeM
3. * ¬ (x)(Ax ⊃Bx) / 2Simp.
4. * (∃x)(Ax • ¬ Bx) / 3CQ
5. * Am • ¬ Bm / 4EI x/m
6. * Am / 5Simp.
7. * ¬ (∃x)Ax / 2Simp.
8. * (x) ¬ Ax / 7CQ
9. * ¬ Am / 8UI x/m
10. * Am • ¬ Am / 6,9Conj.
11. ¬ ¬ [(x)(Ax ⊃Bx) ∨(∃x)Ax] / 1-10IP
12. (x)(Ax ⊃Bx) ∨(∃x)Ax / 11DN