10.5 Sidetrack: Derived Rules for the Existential Quantifier

As for the propositional case is it possible to design derived rules of the first order rules. You might often want to construct tableaux directly for formulae that contain existential quantifiers, without pre-processing them to contain negated universal quantifiers instead. You can use the derived rules given below for this purpose (see Section 7.2.8 on the concept of a derived rule).

In analogy to the -rules, we will call the -rule universal and the -rules existential . It's probably obvious why our defined rules do what they should do.