Harrop formula
id:
harrop-formula-171-11713115
title:
Harrop formula
text:
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 ∧ B is Harrop provided A and B are;
- ¬ F is Harrop for any well-formed formula F ;
- F → A is Harrop provided A is, and F is any well-formed formula;
- ∀ x. A is Harrop provided A is. By excluding disjunction and existential quantification, non-constructive predicates are avoided, which has benefits
brand slug:
wiki
category slug:
encyclopedia
description:
original url:
https://en.wikipedia.org/wiki/Harrop_formula
date created:
2009-05-02T06:26:30Z
date modified:
2024-09-01T11:02:45Z
main entity:
{"identifier":"Q5666472","url":"https://www.wikidata.org/entity/Q5666472"}
image:
fields total:
13
integrity:
14