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 an independent term to make a general argument. This instance can be thought of as an example, chosen in ignorance of its 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 using existential generalization, an existential conclusion is based on the proof of an instance, which thus constructs an example of the sort the existential claims to exist.

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). Also as was the case with the universal quantifier, to uncover counterexamples to invalid arguments using finite ranges (when such counterexamples exist), we would need a supplemented form of proof, in this case PCh+.

The system we have now completed accounts for the entailments of what is known as first-order logic. It has come to been seen as the core of deductive logic. Until a century ago that status was given to the theory of syllogims, which can be regarded as a portion of first-order logic which does not make use of the possibility of analyzing the restricting and quantified predicates of generalizations or claims of exemplification.

The qualification first-order indicates that 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.