| dbpprop:abstract
|
- 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 (⊥); <math>A \wedge B</math> is Harrop provided <math>A</math> and <math>B</math> are; <math>\neg A</math> is Harrop provided <math>A</math> is; <math>F \rightarrow A</math> is Harrop provided <math>A</math> is, and <math>F</math> is any well-formed formula; <math>\forall x. A</math> is Harrop provided <math>A</math> 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: <math>A \leftrightarrow \neg \neg A</math> 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.
|
![[RDF Data]](/statics/sw-cube.png)
