Harrop formula

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search

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 (⊥);
  • 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 and existential quantification (except in the antecedent of implication), non-constructive predicates are avoided, which has benefits for computer implementation. From a constructivist point of view, Harrop formulae are "well-behaved." For example, in Heyting arithmetic, Harrop formulae satisfy a classical equivalence not usually satisfied in constructive logic:[1]

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.

Hereditary Harrop formulae and logic programming[edit]

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.

G-formulae are defined as follows:[4]

  • 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.

See also[edit]


  1. ^ a b Dummett, Michael (2000). Elements of Intuitionism (2nd ed.). Oxford University Press. p. 227. ISBN 0-19-850524-8.
  2. ^ a b A. S. Troelstra, H. Schwichtenberg. Basic proof theory. Cambridge University Press. ISBN 0-521-77911-1.CS1 maint: uses authors parameter (link)
  3. ^ Ronald Harrop (1956). "On disjunctions and existential statements in intuitionistic systems of logic". Mathematische Annalen. 132 (4): 347. doi:10.1007/BF01360048.
  4. ^ 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