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