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 (⊥); A ∧ B {\displaystyle A\wedge B} is Harrop provided A {\displaystyle A} and B {\displaystyle B} are; ¬ F {\displaystyle \neg F} is Harrop for any well-formed formula F {\displaystyle F} ; F → A {\displaystyle F\rightarrow A} is Harrop provided A {\displaystyle A} is, and F {\displaystyle F} is any well-formed formula; ∀ x . A {\displaystyle \forall x.A} is Harrop provided A {\displaystyle A} is.