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.

Harrop formulae are more "well-behaved" also in a constructive context. For example, in Heyting arithmetic ${\displaystyle {\mathsf {HA}}}$, Harrop formulae satisfy a classical equivalence not generally satisfied in constructive logic:¹

${\displaystyle \neg \neg A\leftrightarrow A.}$

But there are still ${\displaystyle \Pi _{1}}$-statements that are ${\displaystyle {\mathsf {PA}}}$-independent, meaning these are Harrop formulae ${\displaystyle \forall x.A}$ for which excluded middle is however not ${\displaystyle {\mathsf {HA}}}$-provable. The standard example is the arithmetized consistency of ${\displaystyle {\mathsf {PA}}}$ (or ${\displaystyle {\mathsf {HA}}}$-equivalently that of ${\displaystyle {\mathsf {HA}}}$). So

${\displaystyle {\mathsf {HA}}\vdash \neg \neg {\mathrm {Con} }({\mathsf {HA}})\leftrightarrow {\mathrm {Con} }({\mathsf {HA}})}$

but

${\displaystyle {\mathsf {HA}}\nvdash {\mathrm {Con} }({\mathsf {HA}})\lor \neg {\mathrm {Con} }({\mathsf {HA}}).}$

And a plain disjunction is never Harrop itself, in the syntactic sense. So the above is compatible with the fact that intuitionistic logic itself already proves ${\displaystyle \neg \neg (P\lor \neg P)}$ indeed for any ${\displaystyle P}$.

Note that Harrop formulea in the syntactic sense are equivalent to non-Harrop formulas, for example through explosion as ${\displaystyle A\leftrightarrow (A\lor \bot )}$.

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 ${\displaystyle r}$ or formulae ${\displaystyle r(t_{1},...,t_{n})}$, are hereditary Harrop;
• ${\displaystyle A\wedge B}$ is hereditary Harrop provided ${\displaystyle A}$ and ${\displaystyle B}$ are;
• ${\displaystyle \forall x.A}$ is hereditary Harrop provided ${\displaystyle A}$ is;
• ${\displaystyle G\rightarrow A}$ is hereditary Harrop provided ${\displaystyle A}$ is rigidly atomic, and ${\displaystyle G}$ is a G-formula.

G-formulae are defined as follows:⁴

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

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.