Harrop formula

Quality 0.50 · 3 views · Updated 2 months ago

title: "Harrop formula" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["constructivism-(philosophy-of-mathematics)", "intuitionism"] topic_path: "philosophy" source: "https://en.wikipedia.org/wiki/Harrop_formula" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0

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 and existential quantification (except in the antecedent of implication), non-constructive predicates are avoided, which has benefits for computer implementation.

Discussion

Harrop formulae are more "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: :\neg \neg A \leftrightarrow A. But there are still \Pi_1-statements that are {\mathsf{PA}}-independent, meaning these are Harrop formulae \forall x. A for which excluded middle is however not {\mathsf{HA}}-provable. The standard example is the arithmetized consistency of {\mathsf{PA}} (or {\mathsf{HA}}-equivalently that of {\mathsf{HA}}). So :{\mathsf{HA}}\vdash \neg\neg{\mathrm{Con}}({\mathsf{HA}})\leftrightarrow {\mathrm{Con}}({\mathsf{HA}}) but :{\mathsf{HA}}\nvdash {\mathrm{Con}}({\mathsf{HA}})\lor \neg{\mathrm{Con}}({\mathsf{HA}}). And a plain disjunction is never Harrop itself, in the syntactic sense. So the above is compatible with the fact that intuitionistic logic itself already proves \neg\neg(P\lor \neg P) indeed for any P.

Note that Harrop formulea in the syntactic sense are equivalent to non-Harrop formulas, for example through explosion as A\leftrightarrow (A\lor\bot).

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:

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

References

References

  1. Dummett, Michael. (2000). "Elements of Intuitionism". [[Oxford University Press]].
  2. A. S. Troelstra. (27 July 2000). "Basic proof theory". [[Cambridge University Press]].
  3. Ronald Harrop. (1956). "On disjunctions and existential statements in intuitionistic systems of logic". [[Mathematische Annalen]].
  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

::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::

constructivism-(philosophy-of-mathematics)intuitionism