Harrop formula

From Wikipedia, the free encyclopedia
Jump to: navigation, 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 (⊥);
  • 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. 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]

A \leftrightarrow \neg \neg A.

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

References[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. 
  3. ^ Ronald Harrop (1956). "On disjunctions and existential statements in intuitionistic systems of logic". Mathematische Annalen. 132, Number 4. 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