 PFL can also equivalently be formulated in a natural deduction system. The introduction and elimination rules for the operators of propositional logic and identity are as usual. The quantifier introduction and elimination rules are restricted by use of the predicate ‘\(\rE!\)’, as follows: