Although formal proofs for disjunction involve some new ideas, these are mainly recombinations of ideas used for disjunction and universals.
8.5.1. The role of existentials in entailment
The role of existentials in entailment is analogous to the role of disjunctions in much the way the role of universals is analogous to that of conjunctions.
8.5.2. Derivations for existentials
Derivation rules for existentials then also exhibit an analogy with those for disjunction, with two basic rules supplemented by an often useful attachment rule.
8.5.3. First-order logic
This completes our account of entailment for first-order logic; higher-order logics concern quantifiers the generalize from predicates rather than individual terms but no complete system of derivations can be given for them.