Existentials bear the kind of analogy to disjunctions that universals bear to conjunctions, and their role in entailment reflects this. Our principle for the unrestricted existential as premise says that the existential will support a proof by choice. This is a sort of proof by cases in which cases for each instance of the existential are handled not one by one but by using a parameter to consider a single instance that sets the pattern for all the rest. The pattern-setting instance can thus be thought of as an example, chosen in ignorance of its specific identity, of the sort that the existential claims to exist. There are two approaches to establishing an existential conclusion. Our general principle for the unrestricted existential as a conclusion uses the idea of non-constructive proof, in which a claim of exemplification is based on the reduction to absurdity of a corresponding negative universal. In a constructive proof, an existential conclusion is based on the proof of an instance, which thus constructs
an example of the sort the existential claims to exist. Constructive proofs are supported by the attachment principle of existential generalization. There are analogous principles for the restricted existential as a premise and as a conclusion and of restricted existential generalization.
The laws for existential premises and conclusions are implemented in exploitation and planning rules using some ideas from the rules for universals. The principles for unrestricted existentials are implemented in the rules Proof by Choice (PCh), Non-constructive Proof (NcP), and Existential Generalization (EG); and, for the restricted existential, we have analogous rules of Proof by Restricted Choice (PRCh), Restricted Non-constructive Proof (RNcP), and Restricted Existential Generalization (REG). An alternative approach to the deductive properties of restricted existentials uses rules Restricted Existential Premise (REP) and Restricted Existential Conclusion (REC) to restate them using unrestricted quantifiers or conclude them from such restatements. Also as was the case with the universal quantifier, to uncover counterexamples to invalid arguments using finite ranges (when such counterexamples exist), we need supplemented forms of proof by choice and restricted choice, PCh+ and PRCh+.
The arguments for soundness and completeness also contain no new twists. The system we have now completed accounts for the entailments of what is known as first-order logic. That is, we consider quantification only over individuals and not over properties, properties of those properties, or any other second-order or higher-order entities. Although higher-order logic, or type theory, has attracted interest since Frege, it cannot be given a complete system of derivations.