Harrop formula

In intuitionistic logic, the Harrop formulae, named after Ronald Harrop, are the class of formulae inductively defined as follows:^[1]^[2]^[3]

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.

Discussion

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

\neg \neg A\leftrightarrow A.

There are however $\Pi _{1}$ -statements that are ${\mathsf {PA}}$ -independent, meaning these are simple $\forall x.A$ statements for which excluded middle is not ${\mathsf {HA}}$ -provable. Indeed, while intuitionistic logic proves $\neg \neg (P\lor \neg P)$ for any $P$ , the disjunction will not 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 $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:^[4]

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.

History

Harrop formulae were introduced around 1956 by Ronald Harrop and independently by Helena Rasiowa.^[2] Variations of the fundamental concept are used in different branches of constructive mathematics and logic programming.

References

^ ^a ^b Dummett, Michael (2000). Elements of Intuitionism (2nd ed.). Oxford University Press. p. 227. ISBN 0-19-850524-8.
^ ^a ^b A. S. Troelstra; H. Schwichtenberg (27 July 2000). Basic proof theory. Cambridge University Press. ISBN 0-521-77911-1.
^ Ronald Harrop (1956). "On disjunctions and existential statements in intuitionistic systems of logic". Mathematische Annalen. 132 (4): 347–361. doi:10.1007/BF01360048. S2CID 120620003.
^ ^a ^b Dov M. Gabbay, Christopher John Hogger, John Alan Robinson, Handbook of Logic in Artificial Intelligence and Logic Programming: Logic programming, Oxford University Press, 1998, p 575, ISBN 0-19-853792-1

[dummett-1] Dummett, Michael (2000). Elements of Intuitionism (2nd ed.). Oxford University Press. p. 227. ISBN 0-19-850524-8.

[basic_proof_theory-2] A. S. Troelstra; H. Schwichtenberg (27 July 2000). Basic proof theory. Cambridge University Press. ISBN 0-521-77911-1.

[3] Ronald Harrop (1956). "On disjunctions and existential statements in intuitionistic systems of logic". Mathematische Annalen. 132 (4): 347–361. doi:10.1007/BF01360048. S2CID 120620003.

[handbook-4] Dov M. Gabbay, Christopher John Hogger, John Alan Robinson, Handbook of Logic in Artificial Intelligence and Logic Programming: Logic programming, Oxford University Press, 1998, p 575, ISBN 0-19-853792-1

[1]

[2]

[3]

[4]

Discussion

Hereditary Harrop formulae and logic programming

History

See also

References