In intuitionistic logic, the Harrop formulae, named after , are the class of formulae inductively defined as follows:
* 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. 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.
Attributes | Values |
---|
rdfs:label
| |
rdfs:comment
| - In intuitionistic logic, the Harrop formulae, named after , are the class of formulae inductively defined as follows:
* 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. 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. (en)
|
dcterms:subject
| |
Wikipage page ID
| |
Wikipage revision ID
| |
Link from a Wikipage to another Wikipage
| |
sameAs
| |
dbp:wikiPageUsesTemplate
| |
has abstract
| - In intuitionistic logic, the Harrop formulae, named after , are the class of formulae inductively defined as follows:
* 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. 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: 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. (en)
|
prov:wasDerivedFrom
| |
page length (characters) of wiki page
| |
foaf:isPrimaryTopicOf
| |
is Link from a Wikipage to another Wikipage
of | |
is Wikipage redirect
of | |
is Wikipage disambiguates
of | |
is foaf:primaryTopic
of | |