Skip to content

Harrop Formula

An intuitionistic formula built so disjunctions and existential quantifiers occur only in negative positions, yielding a stable, computationally disciplined fragment and inspiring hereditary-Harrop logic programming.

Version
v2 · 2026-09-06 · History
Domain-specific #
1982
Origin domain
mathematics
Subdomain
intuitionistic logic
Aliases
Harrop formulae, Harrop formulas, Harrop sentence

Core Idea

A Harrop formula is an intuitionistic formula with no positive occurrence of disjunction or existential quantification. One standard first-order grammar includes atomic formulas and falsity; closes under conjunction and universal quantification; and permits \(B\to H\) whenever the consequent \(H\) is Harrop while the antecedent \(B\) is arbitrary. Negation \(\neg B\) is included as \(B\to\bot\). Harrop introduced the fragment while studying disjunction and existence properties of intuitionistic systems.[1]

The polarity condition—not the mere absence of the symbols \(\lor\) and \(\exists\)—is decisive: those constructors may occur inside an implication antecedent, where polarity is reversed.

Structural Signature

  • A specified intuitionistic propositional or first-order language.
  • Atomic formulas and usually falsity as base cases.
  • Closure under conjunction.
  • Closure under universal quantification.
  • Closure under implication with a Harrop consequent.
  • Arbitrary well-formed antecedents.
  • Negation represented as implication to falsity.
  • No positive disjunction occurrence.
  • No positive existential-quantifier occurrence.
  • An inductive membership derivation over the syntax tree.
  • Proof-theoretic stability and extraction consequences under stated theories.
  • A boundary from the two-grammar hereditary Harrop fragment.

What It Is Not

It is not simply a formula written without \(\lor\) or \(\exists\): those may occur negatively. It is not a semantic equivalence class, because a Harrop formula can be intuitionistically equivalent to a syntactically non-Harrop formula. It is not every negative formula under every author's grammar. It is not identical to a Horn clause or hereditary Harrop formula, although the latter generalizes related polarity discipline for logic programming.

Scope of Application

Harrop formulas appear in constructive proof theory, conservation and disjunction/existence-property arguments, normalization, realizability, arithmetic, proof search, and program extraction. Related hereditary Harrop formulas extend Horn-clause programming with embedded implications, universal goals, and higher-order structure; they underlie languages such as \(\lambda\)Prolog.[2]

Clarity

State the base logic, grammar, treatment of truth and falsity, definition of negation, free-variable policy, and whether “Harrop” or “hereditary Harrop” is intended. Check syntactic polarity on the given parse tree rather than rewriting by semantic equivalence. Qualify stability results by the surrounding intuitionistic theory.

Manages Complexity

The restriction suppresses positive choices and positive witness production in assumptions or conclusions where they would obstruct deterministic proof behavior. Its recursive grammar yields a linear syntax-tree membership test and supports proof-search phases with fewer branching forms. The hereditary extension separates program clauses from goals so operational proof search remains aligned with intuitionistic provability.[3]

Abstract Reasoning

  1. Parse the formula under the declared grammar.
  2. Assign the root positive polarity.
  3. Preserve polarity through conjunction and quantifiers.
  4. Reverse polarity in an implication antecedent and preserve it in the consequent.
  5. Reject \(\lor\) or \(\exists\) at positive positions.
  6. Or derive membership directly from the inductive Harrop clauses.
  7. Distinguish syntactic membership from provable equivalence.
  8. Apply only the proof-theoretic consequences justified by the base theory.

Knowledge Transfer

The portable pattern is restrict choice-producing constructors by polarity so a logical fragment gains stronger operational and proof-theoretic behavior. It transfers to focused proof systems and executable specification languages. The proposed immediate parent is Formal System.

Examples

The formula \(P\land\forall x(Q(x)\to R(x))\) is Harrop when the atoms are. The formula \((\exists x\,P(x))\to Q\) is also Harrop because the existential lies in the antecedent. In contrast, \(P\lor Q\) and \(\exists x\,P(x)\) are not Harrop at the root. Constructive logic texts develop the fragment's connection with negative and stable formulas while keeping theory-specific boundaries explicit.[4]

Structural Tensions

  • Syntactic membership versus semantic equivalence.
  • Ordinary Harrop versus hereditary Harrop grammar.
  • Restricted positive choice versus expressive goals.
  • Stability results versus theory-dependent assumptions.
  • Deterministic proof behavior versus full intuitionistic expressiveness.
  • Historical variants versus one modern normalized presentation.

Structural–Framed Character

Inductive definition, polarity, closure, and constructor restriction are structural. Intuitionistic implication, disjunction, existential quantification, proof properties, and logic-programming use are constitutive. The identity is domain-specific.

Structural Core vs. Domain Accent

The portable core is classify syntax recursively -> exclude branching or witness constructors in positive positions -> gain disciplined reasoning. The domain accent is intuitionistic formulas and their proof theory.

Formal System is the proposed immediate parent. Classification, Constraint, Mathematical Induction, Deductive Reasoning, and Symbolic Representation are related. Sequent and Skolem Normal Form are neighboring logical objects, not coverage.

The prospective queue contains one strict edge to prime:formal_system. No live DAG mutation is authorized.

Relationships to Other Abstractions

Local relationship map for Harrop FormulaParents appear above the current abstraction, mutual partners to the right, and children below. Node labels state whether each abstraction is prime or domain-specific; colors identify relation types.Harrop FormulaDOMAINPrime abstraction: Formal System — is a kind ofFormal SystemPRIME

Current abstraction Harrop Formula Domain-specific

Parents (1) — more general patterns this builds on

  • Harrop Formula is a kind of Formal System Prime

    Formal System is the proposed immediate parent.

Hierarchy paths (2) — routes to 2 parentless roots

Neighborhood in Abstraction Space

Harrop Formula sits in a sparse region of the domain-specific corpus (81st percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Fuzzy, Monoidal & Higher-Order Logic (5 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With

  • Formula with no printed disjunction or existential symbol.
  • Hereditary Harrop formula without qualification.
  • Horn clause.
  • Negative normal form.
  • Skolem normal form.
  • A formula semantically equivalent to a Harrop formula.

References

[1] Ronald Harrop, “On Disjunctions and Existential Statements in Intuitionistic Systems of Logic,” Mathematische Annalen 132 (1956–1957): 347–361, https://eudml.org/doc/160525. registry ↩

[2] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov, “Hereditary Harrop Formulas and Uniform Proof Systems,” in Proceedings of the Second Annual Symposium on Logic in Computer Science (IEEE, 1987): 98–105, https://www.lix.polytechnique.fr/~dale/papers/clmps1987.pdf. registry ↩

[3] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov, “Uniform Proofs as a Foundation for Logic Programming,” Annals of Pure and Applied Logic 51 (1991): 125–157, doi:10.1016/0168-0072(91)90068-W. registry ↩

[4] A. S. Troelstra and D. van Dalen, Constructivism in Mathematics, vol. 1 (North-Holland, 1988), ISBN 9780444702661. registry ↩