8.5. Proofs by choice and proofs of existence

8.5.0. Overview

Although formal proofs for disjunction involve some new ideas, these are mainly recombinations of ideas used for disjunction and universals.

8.5.1. Proof by choice
A conclusion can be derived from an existential by choosing a new name for the example whose existence it claims.

8.5.2. Constructive and non-constructive proof
A claim of exemplification can be established either by constructing an example or by reducing to absurdity the assumption that there is no such example.

8.5.3. Derivations for existentials
Our selection of derivation rules for existentials is analogous to that for disjunction, with two basic rules supplemented by an often useful attachment rule.

8.5.4. First-order logic
This completes our account of entailment for first-order logic, which has come to replace the theory of syllogisms as the generally accepted core of deductive logic.