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.

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.

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.

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.

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.

Relationships to Other Abstractions

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

• Harrop Formula → Formal System → Formalization → Representation → Abstraction

Show alternative path (1)

Neighborhood in Abstraction Space

Harrop Formula sits in a sparse region of the domain-specific corpus (81^st 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

• Monoidal t-Norm Logic — 0.83
• Formal Theory — 0.83
• Negation as Failure — 0.81
• Heyting arithmetic — 0.81
• Second-order logic — 0.81

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