Harrop Formula
   HOME

TheInfoList



OR:

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 In logic, disjunction (also known as logical disjunction, logical or, logical addition, or inclusive disjunction) is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is ...
and
existential quantification Existentialism is a family of philosophy, philosophical views and inquiry that explore the human individual's struggle to lead an Authenticity (philosophy), authentic life despite the apparent Absurdity#The Absurd, absurdity or incomprehensibili ...
(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 , Harrop formulae satisfy a classical equivalence not generally satisfied in constructive logic: :\neg \neg A \leftrightarrow A. There are however \Pi_1-statements that are -independent, meaning these are simple \forall x. A statements for which excluded middle is not -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: Dov M. Gabbay, Christopher John Hogger, John Alan Robinson, ''Handbook of Logic in Artificial Intelligence and Logic Programming: Logic programming'',
Oxford University Press Oxford University Press (OUP) is the publishing house of the University of Oxford. It is the largest university press in the world. Its first book was printed in Oxford in 1478, with the Press officially granted the legal right to print books ...
, 1998, p 575,
* 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.


History

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.


See also

* Realizability


References

{{reflist Constructivism (mathematics) Intuitionism