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 (⊥);
- [math]\displaystyle{ A \wedge B }[/math] is Harrop provided [math]\displaystyle{ A }[/math] and [math]\displaystyle{ B }[/math] are;
- [math]\displaystyle{ \neg F }[/math] is Harrop for any well-formed formula [math]\displaystyle{ F }[/math];
- [math]\displaystyle{ F \rightarrow A }[/math] is Harrop provided [math]\displaystyle{ A }[/math] is, and [math]\displaystyle{ F }[/math] is any well-formed formula;
- [math]\displaystyle{ \forall x. A }[/math] is Harrop provided [math]\displaystyle{ 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. Harrop formulae are "well-behaved" also in a constructive context. For example, in Heyting arithmetic, Harrop formulae satisfy a classical equivalence not usually satisfied in constructive logic:[1]
- [math]\displaystyle{ A \leftrightarrow \neg \neg A. }[/math]
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
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 [math]\displaystyle{ r }[/math] or formulae [math]\displaystyle{ r(t_1,...,t_n) }[/math], are hereditary Harrop;
- [math]\displaystyle{ A \wedge B }[/math] is hereditary Harrop provided [math]\displaystyle{ A }[/math] and [math]\displaystyle{ B }[/math] are;
- [math]\displaystyle{ \forall x. A }[/math] is hereditary Harrop provided [math]\displaystyle{ A }[/math] is;
- [math]\displaystyle{ G \rightarrow A }[/math] is hereditary Harrop provided [math]\displaystyle{ A }[/math] is rigidly atomic, and [math]\displaystyle{ G }[/math] is a G-formula.
G-formulae are defined as follows:[4]
- Atomic formulae are G-formulae, including truth(⊤);
- [math]\displaystyle{ A \wedge B }[/math] is a G-formula provided [math]\displaystyle{ A }[/math] and [math]\displaystyle{ B }[/math] are;
- [math]\displaystyle{ A \vee B }[/math] is a G-formula provided [math]\displaystyle{ A }[/math] and [math]\displaystyle{ B }[/math] are;
- [math]\displaystyle{ \forall x. A }[/math] is a G-formula provided [math]\displaystyle{ A }[/math] is;
- [math]\displaystyle{ \exists x. A }[/math] is a G-formula provided [math]\displaystyle{ A }[/math] is;
- [math]\displaystyle{ H \rightarrow A }[/math] is a G-formula provided [math]\displaystyle{ A }[/math] is, and [math]\displaystyle{ H }[/math] is hereditary Harrop.
See also
References
- ↑ 1.0 1.1 Dummett, Michael (2000). Elements of Intuitionism (2nd ed.). Oxford University Press. p. 227. ISBN 0-19-850524-8.
- ↑ 2.0 2.1 A. S. Troelstra; H. Schwichtenberg (27 July 2000). Basic proof theory. Cambridge University Press. ISBN 0-521-77911-1.
- ↑ Ronald Harrop (1956). "On disjunctions and existential statements in intuitionistic systems of logic". Mathematische Annalen 132 (4): 347–361. doi:10.1007/BF01360048.
- ↑ 4.0 4.1 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
 |  |
