Predicate Invention

Before the law stands a doorkeeper. A man from the country comes to this doorkeeper and asks for admission to the law. But the doorkeeper says he cannot grant him admission now.

Predicate invention is treated here as governed signature extension. A17 requires local grounding, typed overlap agreement, and invariant preservation before a proposed symbol acquires wider standing.

The Failure Mode We Are Fixing

A user wants to search for "puffy dresses." The catalog has no agreed predicate for puffiness. A retrieval system can return candidates; a database can evaluate a supplied expression, expose a view or typed function, or store a registered predicate definition. None of those operations alone settles which meaning the user intends or how it should relate to another user's definition.

The missing information concerns admission: the candidate's interpretation, evaluation method, evidence, applicable scope, authority, and effects on existing commitments. Those obligations arise whether the candidate is supplied by a person, a learning system, or a program.

Part III supplied candidate mathematical machinery for expressing some of these obligations. Part IV proposes how to organize them into a lifecycle that existing database, graph, and verification components could implement. It does not report a general implemented solution to schema discovery or cross-context certification.

Admitting a New Predicate

Here predicate invention names governed signature extension. Candidate generation and admission are separate: A17 primarily specifies the conditions under which a proposed symbol may acquire standing.

The proposal requires local grounding, typed overlap agreement, and invariant preservation. A conforming implementation would retain the evidence for acceptance and explain an established failure. Where an obligation cannot be decided within the declared method or resource limit, it must report that limit rather than present the candidate as certified.

An uninterpreted or unevaluated symbol can still be a predicate symbol in logic. The narrower operational requirement here is that a predicate admitted for checked use comes with the evaluation and evidence contract required in its declared scope. This is a policy of the proposed architecture, not a definition of every legitimate predicate.

These obligations describe a proposed admission process. The examples below illustrate its intended records and outcomes; they are not execution logs or demonstrations of a complete implementation. Acceptance is justified only for the obligations actually discharged under the declared logic, scope, and evidence policy. An established failure must be distinguished from an inconclusive check, as the decidability qualification below requires.

Standing Is a Gradient

Standing can increase without requiring every local experiment to pass a global admission gate. The proposed lifecycle distinguishes candidate use from certified use:

These are standing labels, not interchangeable kinds of evidence. An observation log, an attestation, a sampled evaluation, and a formal proof establish different things. A receipt must preserve that distinction. A proposed search term may remain useful before certification, provided consumers do not treat its ranking as an authoritative assertion.

The design permits exploratory local use while requiring checks for uses that claim wider authority or certified scope. A scope extension must satisfy all applicable promotion gates, including authority approval; overlap agreement alone is insufficient. Local use also remains subject to the hard invariants and permissions that apply locally.

Checking on demand can avoid evaluating irrelevant overlaps. Its cost depends on the actual context graph, candidate language, and checking procedure; no universal complexity or solved-language-understanding requirement follows from this lifecycle alone.

Obligation 1: Local Grounding

A predicate is locally grounded under A17 when its signature, evaluation method, exemplars, provenance, and authority declaration meet the stated contract in a view. This supports inspection of a result; it does not imply that every admitted evaluation method is a total decision procedure or that its outputs are infallible.

The components are straightforward. First, a signature: what type of things does this predicate apply to, and what type of values does it return? For "puffy," the domain is Dress and the codomain is Score (a continuous value from 0 to 1). Not Bool. Making it Score forces us to think about what happens when two views have different scales.

Second, an evaluation method. How do you compute puffy(d) for a given dress d? Four options:

Measurement: a deterministic procedure. For puffy, the toy procedure uses volume_ratio(d) / max_volume_in_reference_set, assuming a positive denominator and a declared domain whose ratios do not exceed it. On that domain its outputs lie in [0,1]. The reference set is pinned at creation time and recorded in provenance; otherwise the measurement drifts as the catalog changes. The procedure is traceable: given the same inputs and the same reference set, it returns the same output.

Rule: a logical formula in terms of existing predicates. A separate Bool-valued proposal could use voluminous(d) ∧ ¬structured(d), if those predicates already exist. The formula is auditable: you can check whether the rule was applied correctly.

Oracle: human judgment. A stylist looks at a dress and assigns a puffiness score. The oracle must be declared, not hidden. The system records that this predicate's values come from human judgment, not computation.

Learned function: a classifier or regressor trained on exemplars. A model takes dress features and returns a score. The proposed contract requires model provenance and a stated evaluation regime. An error bound must identify its evidence, assumptions, and applicable population; recording a bound does not establish that it holds outside those conditions.

Third, a witness set. Not a test suite in the QA sense, but a set of exemplars that ground the predicate's meaning. For puffy: five dresses labeled as high-puffy (score > 0.7), five labeled as low-puffy (score < 0.3), each with provenance (who labeled it, when, in what context). The witness set also includes boundary cases: items where the label is disputed or uncertain.

Fourth, an authority level. The dossier declares who proposes to assert the predicate and the scope sought. Preventing an unauthorized promotion also requires an authenticated identity, a trusted authorization policy, and an enforced admission path. The declaration records the requested standing; a working authorization mechanism must decide whether to grant it.

The key constraint: predicates start non-global. You can ground a predicate locally without proving it works everywhere. Globality is a promotion outcome, earned through overlap agreement and authority approval, not assumed at creation time.

PredicateSpec(puffy, user_session_view) = {
  signature: {
    domain: Dress,
    codomain: Score,
    codomain_agreement: Calibration
  },
  evaluation: Measurement(volume_ratio / max_volume), // max_volume > 0; domain ratios ≤ max_volume
  witness_set: {
    positive: [(dress_A, 0.9, user_session), (dress_B, 0.85, user_session), ...],
    negative: [(dress_X, 0.1, user_session), (dress_Y, 0.2, user_session), ...],
    boundary: []
  },
  authority: { level: "user", declaring_agent: user_42 },
  scope: { defining_view: user_session_view, global: false }
}

Obligation 2: Overlap Agreement (Typed)

If two views both define q, their definitions must be reconcilable on the overlap.

Exact agreement under the sheaf hypotheses is one case of A13. The proposed operational contract also permits other declared comparisons. Those comparisons must not inherit the exact gluing guarantee without the additional construction and proof.

For Bool predicates, reconcilable means literal equality: if Merchant A says sustainable(dress_X) = true and Merchant B says sustainable(dress_X) = false, that is a disagreement. The system cannot glue.

For Score predicates, reconcilable means calibration: two views can have different scales as long as there exists a monotone transform that aligns them. If Merchant A's puffy scores range from 0 to 1 and Merchant B's range from 0 to 10, that is fine if multiplying A's scores by 10 produces agreement on shared items. The calibration witness records the transform and the evidence that it works.

For learned predicates, reconcilable means agreement on a certified test set within a declared error bound. Agreement on that evaluation set establishes the measured comparison there. It does not by itself establish either classifier’s validity on a wider population, nor unique gluing of their outputs.

AgreementType(codomain) = {
  comparator: (V₁, V₂) → Bool,           // how to compare values
  evidence: EvidenceType,                 // what witness is required
  acceptance_rule: EvidenceType → Bool    // when agreement holds
}

where EvidenceType =
  | Equality                              // for Bool: values match after A15 translation
  | CalibrationWitness {                  // for Score
      transform: V → V,                   // monotone function aligning scales
      tolerance: ε,                       // max allowed deviation
      test_items: [(x, v₁, v₂, aligned)]  // alignment evidence
    }
  | ErrorBoundWitness {                   // for Learned
      test_set: [(x, expected, actual)],
      error_bound: δ,
      coverage: CoverageMetric
    }
  | RefinementWitness {                   // for versions
      direction: v2 ⪯ v1,
      implication_proof: ∀x. q_v2(x) ⇒ q_v1(x)
    }

Overlap agreement is evaluated after A15 status translation. If View A uses classical logic with OWA and View B uses classical logic with CWA, their source statuses and absence policies must be retained for comparison. Opposed assertions are recorded as a conflict between reports, not a fourth status of the consistency-scoped A4 definition. If both concern the same proposition and scope, a positive assertion and an absence-derived negative are contrary assertions. Their different grounds matter: the comparison must inspect the closure rule and its support rather than treating either value as established by its label.

For nonexact comparisons, or comparisons on different domains, two accepted pairwise checks need not establish a third. A cover-level contract must state and check the necessary composition conditions. Exact equality on one common domain is transitive; this operational difficulty does not refute that law.

sustainable\_A(d) := material(d) ∈ (organic\_cotton, recycled\_polyester, linen)

sustainable_B(d) := certified(d, [GOTS, OEKO-TEX, B-Corp])

OverlapDisagreement {
  predicate: sustainable,
  codomain_type: Bool,
  views: [Merchant_A, Merchant_B],
  overlap: catalog_intersection,
  witness_items: [(item_X, true, false, equality_failed)],
  resolution_options: [
    "Fork: maintain sustainable_A and sustainable_B as distinct predicates",
    "Negotiate: define sustainable_global := sustainable_A ∧ sustainable_B",
    "Escalate: authority decides canonical definition"
  ]
}

The medical example in Interlude III-A distinguishes authorization in one market from authorization in another. US clearance and an explicitly unmarked EU status can be recorded together; they answer different market-indexed questions. They do not jointly establish authorization in both markets. A missing registry entry presents a further evidentiary question, whose answer depends on the register’s coverage at the relevant date. None of these distinctions is repaired merely by naming a comparison map.

Obligation 3: Invariant Preservation

The new predicate must not break what already works.

This sounds obvious, but "break" has two meanings that must be kept distinct.

Tier 3a: Hard Invariant Conservativity

The new predicate must not force violations of existing hard invariants. Hard invariants come in two flavors:

Logical invariants: type constraints (puffy : Dress → Score, not puffy : String → Float), integrity constraints (¬(puffy_score > 0.8 ∧ fitted) if that's declared), mutual exclusions (a dress cannot be both minimalist and maximalist).

Operational invariants: units (if price is in USD, affordable thresholds must be unit-compatible), cardinalities (if primary_category is single-valued, puffy cannot force multiple), authority bounds (user-generated predicates cannot claim system authority).

If adding puffy would require some dress to be both puffy and fitted when an invariant prohibits that combination, the candidate is rejected. Note: a predicate can exist locally even if it would violate invariants elsewhere. What is forbidden is asserting it as authoritative in a scope where it breaks hard invariants.

Tier 3b: Non-Interference (Practical Conservativity)

The operational contract identifies which old queries, meanings and evidence policies must remain stable. Performance or ranking is excluded only where the receiving contract actually excludes it. Logical conservativity—no new old-language theorems—is a separate condition, developed in Chapter 16.

The proposed operational non-interference check requires:

• Existing queries on Σ return the same answers after adding q
• If adding q would change existing truths (e.g., by triggering a derived invariant), the system must emit an explicit migration witness (A17b)

The proposal makes preservation the default obligation. Where a change breaks the receiving contract, a migration record must disclose it and the required approval must be obtained; emitting a record alone does not authorize the break.

InvariantViolation {
  predicate: puffy,
  tier: "3a_hard",
  violated_invariant: "¬(puffy_score > 0.8 ∧ silhouette = fitted)",
  invariant_type: "logical",
  witness: (dress_Y, puffy_score=0.95, silhouette=fitted, rule_violated),
  resolution_options: [
    "Retract predicate candidate",
    "Weaken invariant (requires authority approval)",
    "Scope restriction: exclude fitted dresses from puffy's domain"
  ]
}

The Predicate Dossier

Admission leaves something a later operation can examine. The successful dossier identifies the definition, its evaluation conditions, the checks completed and the scope earned. For the measurement of puffiness, this includes the pinned reference set: a later reader needs to know which maximum supplied the denominator. An authority declaration must remain connected to the approval actually obtained. Neither the current formula nor a standing label can recover those grounds after they have been discarded.

Chapter 22's A24 package organizes the definition, runtime, tests, invariants, provenance and scope. A16 supplies the property-specific transport certificates; A26 records version compatibility and correction. Those records let another operation find the work it can reuse and identify what its own purpose still requires. The detailed package belongs with that account of its subsequent use.

A completed admission check can produce a Predicate Dossier or evidence of an established violation. Missing grounds or unfinished checking instead produce Inconclusive, naming the required obligation and reason. The following artifact concerns the established-failure case:

ObstructionWitness {
  predicate_candidate: PredicateSpec,
  failed_obligation: "local_grounding" | "overlap_agreement" | "invariant_preservation",
  failure_details: GroundingFailure | OverlapDisagreement | InvariantViolation,
  resolution_options: [ResolutionOption, ...]
}

An exploratory proposal can remain available without pretending it passed those checks. When unfinished admission is used to keep a consequential matter pending, Appendix I, I.1.6 also requires an account of responsibility, review and the response if the question remains unsettled. Recording the candidate preserves the possibility of further work; it does not grant the standing that work was meant to establish.

The Promotion Protocol

Promotion claims a wider scope of use. It requires grounds covering that scope; exact gluing is one available construction under its own hypotheses, not the definition of every successful promotion.

A predicate starts local. To expand its scope, the predicate must pass additional gates.

Promotion rule: A predicate may be promoted from view U to cover $\{U_i\}$ iff:

1. Overlap agreement holds on all pairwise overlaps in the cover (or obstruction witnesses are explicitly accepted as forks)
2. Calibration witnesses exist where codomains differ (e.g., different scoring scales reconciled via monotone transform)
3. Authority witness approves the promotion scope under the applicable process
4. Receiving admission requirements hold, including hard invariants, grounding and the declared preservation obligations. A calibration or accepted fork cannot waive those requirements or turn approximate agreement into exact gluing

PromotionRequest {
  predicate: puffy,
  from_scope: user_session_view,
  to_scope: [org_catalog_view],
  overlap_agreements: [
    // For Bool: equality witness
    // For Score: calibration witness (a specialized overlap agreement)
    (user_session, merchant_A, AgreementWitness { type: calibration, transform: identity })
  ],
  authority_approval: org_admin_approval_ref
}

PromotionResult = 
  | Promoted { new_scope: [org_catalog_view], dossier_updated: puffy_v1.1 }
  | Rejected { 
      overlap_failures: [(user_session, merchant_B, obstruction)],
      authority_denied: null
    }
  | Inconclusive { unchecked_obligations: [...], reason: ... }

Under the proposed promotion rule, an implementation must evaluate every applicable gate and retain the evidence for its decision. A demonstrated failure warrants rejection with a structured explanation; an unresolved check warrants an explicit inconclusive outcome. A human resolution must carry the authority required for the requested scope.

Related Operations and Learning Methods

The proposed admission discipline can be combined with schema-on-read, feature engineering, ontology development, and embedding methods. Each can supply representations or candidate definitions. The comparison should therefore ask which checks a particular workflow performs, when they run, and what evidence survives downstream use.

Schema-on-read describes when interpretation is applied; it does not by itself specify overlap reconciliation. A feature or embedding cluster can become an input to the proposed process once its definition, evidence, and intended use are stated. An ontology workflow may already supply typed definitions and governance. A17 asks how those artifacts participate in the additional obligations of this architecture; it does not establish that their existing disciplines are absent or inadequate.

Relation to Inductive Logic Programming

Inductive Logic Programming includes methods for learning definitions and inventing predicates from examples and background knowledge. For example, Hocquette and Muggleton's 2020 predicate-invention method proves completeness within a specified fragment of dyadic Datalog and evaluates a concrete learner. That is evidence about a named algorithm and fragment, not a guarantee for every deployment of ILP.

A17 addresses a different stage of the lifecycle: the standing of a proposed definition across declared views, authorities, and transport conditions. An ILP learner could supply candidates to that process. Conversely, an ILP deployment could add scope, provenance, validation, and authorization. The comparison cannot infer that such additions are impossible merely because they are not part of a selected learning formulation.

The proposed contribution is the joint admission contract: local grounding, typed overlap obligations, preservation requirements, and records for later promotion and transport. Whether this packaging improves reliability or cost over existing combinations requires a specified implementation and comparison. The smaller formal core described below does not establish that result.

A17 gathers local grounding, overlap agreement, and invariant preservation into one proposed admission discipline. The predicate dossier retains the evidence needed for later transport, promotion, and versioning.

The companion Lean project for Predicate Invention Under Sheaf Constraints verifies a smaller formal core. It constructs finite Z/2 overlap examples, proves incompatibility for one concrete family of local predicates, and proves gluing for finite set-valued predicates under joint coverage and pairwise agreement. Those results show that local compatibility can be tested and that some finite disagreements obstruct a global predicate. They do not establish a general H^1 classification, an extension-torsor theorem, conservativity descent, Beth definability for sites, or schema discovery. A17 therefore remains a proposed governed construction whose general mathematical account is open.