Harrop formula

In intuitionistic logic, the Harrop formulae, named after Ronald Harrop, are the class of formulae inductively defined as follows:

• Atomic formulae are Harrop, including falsity (⊥);
• ${\displaystyle A\wedge B}$ is Harrop provided ${\displaystyle A}$ and ${\displaystyle B}$ are;
• ${\displaystyle \neg F}$ is Harrop for any well-formed formula ${\displaystyle F}$;
• ${\displaystyle F\rightarrow A}$ is Harrop provided ${\displaystyle A}$ is, and ${\displaystyle F}$ is any well-formed formula;
• ${\displaystyle \forall x.A}$ is Harrop provided ${\displaystyle A}$ is.

By excluding disjunction and existential quantification (except in the antecedent of implication), non-constructive predicates are avoided, which has benefits for computer implementation.