In the first-order language of classical and intuitionistic logic, a type of formula meeting the criterion that all disjunctive or existentially quantified subformulae appearing within the scope of a conditional appear in the antecedent position. The class $\mathscr{H}$ of Harrop formulae may be recursively defined by the clauses:

• • If $p$ is prime (i.e., atomic or a propositional constant), then $p\in \mathscr{H}$

• • If $\psi \in \mathscr{H}$, then $\phi \to \psi \in \mathscr{H}$

• • If $\phi \in \mathscr{H}$, then $\forall x\phi \in \mathscr{H}$

• • If $\phi \in \mathscr{H}$ and $\psi \in \mathscr{H}$, then $\phi \wedge \psi \in \mathscr{H}$

That $\neg \phi$ is a Harrop formula for arbitrary $\phi$ follows from the definition of $\neg \phi$ as $\phi \to \perp$. Naturally, a Harrop theory is any theory axiomatized by a set of Harrop formulae. Named for mathematician Ronald Harrop (1926– ), who proved that any Harrop theory in intuitionistic logic enjoys the disjunction property and the existence property.