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 (ā„);
*
is Harrop provided
and
are;
*
is Harrop for any well-formed formula
;
*
is Harrop provided
is, and
is any well-formed formula;
*
is Harrop provided
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:
:
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 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
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.
''G''-formulae are defined as follows:
* Atomic formulae are ''G''-formulae, including truth(ā¤);
*
is a ''G''-formula provided
and
are;
*
is a ''G''-formula provided
and
are;
*
is a ''G''-formula provided
is;
*
is a ''G''-formula provided
is;
*
is a ''G''-formula provided
is, and
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