# 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\wedge B$ is Harrop provided $A$ and $B$ are;
• $\neg F$ is Harrop for any well-formed formula $F$ ;
• $F\rightarrow A$ is Harrop provided $A$ is, and $F$ is any well-formed formula;
• $\forall x.A$ is Harrop provided $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. From a constructivist point of view, Harrop formulae are "well-behaved." For example, in Heyting arithmetic, Harrop formulae satisfy a classical equivalence not usually satisfied in constructive logic:

$A\leftrightarrow \neg \neg A.$ Harrop formulae were introduced around 1956 by Ronald Harrop and independently by Helena Rasiowa. Variations of the fundamental concept are used in different branches of constructive mathematics and logic programming.

## Hereditary Harrop formulae and logic programming

A more complex definition of hereditary Harrop formulae is used in logic programming as a generalisation of Horn clauses, and forms the basis for the language λProlog. Hereditary Harrop formulae are defined in terms of two (sometimes three) recursive sets of formulae. In one formulation:

• Rigid atomic formulae, i.e. constants $r$ or formulae $r(t_{1},...,t_{n})$ , are hereditary Harrop;
• $A\wedge B$ is hereditary Harrop provided $A$ and $B$ are;
• $\forall x.A$ is hereditary Harrop provided $A$ is;
• $G\rightarrow A$ is hereditary Harrop provided $A$ is rigidly atomic, and $G$ is a G-formula.

G-formulae are defined as follows:

• Atomic formulae are G-formulae, including truth(⊤);
• $A\wedge B$ is a G-formula provided $A$ and $B$ are;
• $A\vee B$ is a G-formula provided $A$ and $B$ are;
• $\forall x.A$ is a G-formula provided $A$ is;
• $\exists x.A$ is a G-formula provided $A$ is;
• $H\rightarrow A$ is a G-formula provided $A$ is, and $H$ is hereditary Harrop.