Harrop formulae are "well-behaved" also in a constructive context. For example, in
Heyting arithmetic, Harrop formulae satisfy a classical equivalence not generally satisfied in constructive logic:[1]
There are however -statements that are -independent, meaning these are simple statements for which excluded middle is not -provable. Indeed, while intuitionistic logic proves for any , the disjunction wont be Harrop.
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:[4]
Rigid atomic formulae, i.e. constants or formulae , are hereditary Harrop;
is hereditary Harrop provided and are;
is hereditary Harrop provided is;
is hereditary Harrop provided is rigidly atomic, and is a G-formula.