The Refusal Obligation: The prime that cannot exist

Any consistent formal system within which a certain amount of elementary arithmetic can be carried out is incomplete; there are statements of the language which can neither be proved nor disproved.

This chapter formalizes the obligation to refuse logically impossible queries, defining Anchor A27 (Refusal Obligation). The central construction is the RefusalArtifact: a structured response comprising an unsat core, a derivation chain, and a refusal witness that certifies the soundness of the refusal. A27 integrates the consistency requirement of A1 (Commitment Sets), the hard invariants of A18 (Invariant Set), and the query-as-contract semantics of A25 to distinguish logical contradictions from semantic conflicts. The corresponding narrative motivation appears in Volume I, Chapters 6 and 8, where the absence of constraint-aware refusal is diagnosed as a pathology of both the string and schema paradigms.

The Numbers That Look Plausible

Ask a system whose job is to be helpful: "List all integers between 1 and 100 that are both prime and divisible by 4."

The system gives you five numbers: 2, 4, 12, 20, 28. It looks like an earnest attempt to reconcile evenness, divisibility, and primality. Confident delivery. No hesitation. All wrong.

Not wrong because the assistant made a calculation error. Wrong because no such numbers exist. A prime greater than 2 cannot be divisible by 4. The query is logically impossible. The assistant should have refused. Instead, it hallucinated candidates for an empty set.

This is T1, the first touchstone. We introduced it in Chapter 1 as a pathology of the string empire: plausibility engines generate candidates for contradictory queries because they lack constraint representation. The embedding space does not encode mutual exclusion. "Prime" and "divisible by 4" have distributional proximity (both number-theoretic terms) but logical incompatibility (cannot coexist for n > 2).

The schema empire handles this differently but not better. Run the equivalent SQL:

SELECT n FROM integers 
WHERE n BETWEEN 1 AND 100 
  AND is_prime(n) 
  AND n % 4 = 0

Result: empty set. No explanation. No indication that the query was logically empty versus contingently empty. The database checked the data, found no matches, and returned silence. A user seeing this might add more rows, thinking the data is incomplete. The data is fine. The query is impossible.

A coherent system must do neither. It must refuse gracefully and explain why.

Contingent Versus Logical Emptiness

The distinction is fundamental.

Contingent emptiness is a fact about the data. "Blue dresses under $50" returns empty because the catalog happens to contain no blue dresses under $50. Add inventory, and the query might succeed. The world could satisfy the constraints; it just does not right now.

Logical emptiness is a fact about the query. "Minimalist maximalist dresses" returns empty because no possible catalog could satisfy the constraints. Minimalist and maximalist are mutually exclusive by definition. The query contradicts itself. No amount of inventory will help.

The difference matters operationally. Contingent emptiness warrants "no items match your criteria." Logical emptiness warrants "your criteria cannot be satisfied, and here is why." The first is informative. The second is diagnostic.

A system that conflates them wastes user effort. A system that distinguishes them earns trust.

Anchor A27: Refusal Obligation

RefusalArtifact = {
  result: ∅,
  reason: "unsatisfiable_constraints",
  unsat_core: UnsatCore,
  derivation: DerivationChain,
  witness: RefusalWitness,
  rewrite_hints?: [...]       // optional, non-normative
}

UnsatCore = {
  constraints: [c₁, ..., cₖ],
  minimality: "subset-minimal"  // removing any one makes it satisfiable
}

DerivationChain = {
  steps: [(premise, rule, conclusion), ...],
  final_step: ⊥,
  derivation_ref?: "full_trace_id"  // if >10 steps, summarize + reference
}

RefusalWitness = {
  class: decidable,
  method: constraint_propagation | SMT | resolution | tableau,
  sound: true,      // no false refutations (relative to L_U and I_hard)
  checkable: true   // verifier can confirm
}

An unsat core is a subset-minimal set of commitments that cannot all be true together: remove any one, and consistency returns. The derivation chain shows how they conflict. The witness certifies that the refusal is sound: the system is not falsely claiming impossibility.

This integrates with the machinery from Parts II–V:

The system is not failing when it refuses. It is succeeding at a different task: detecting that no answer exists and explaining why.

Logical Versus Semantic Contradiction

A27 triggers on unsatisfiable constraints. But unsatisfiability has two sources, and the distinction matters for user response.

Logical contradiction is impossibility in any world. "Prime and divisible by 4" fails because no integer satisfies both properties. The failure is mathematical. No revision of the taxonomy, no expansion of the catalog, no retraining of the model will produce a satisfying assignment. The query is ill-posed.

Semantic conflict is impossibility in this vocabulary. "Minimalist and maximalist" fails because the style taxonomy defines them as mutually exclusive (constraint C-47). But the exclusion is a modeling choice, not a mathematical necessity. A garment with a minimalist silhouette and maximalist embellishment might exist; the taxonomy simply does not admit it. A user with sufficient authority could override the constraint or propose a vocabulary extension.

The RefusalArtifact should distinguish these:

RefusalReason = 
  | LOGICAL_CONTRADICTION   // no model satisfies; math forbids
  | SEMANTIC_CONFLICT       // no model in this vocabulary satisfies; 
                            // taxonomy forbids, override possible

For logical contradictions, the derivation chain terminates in a mathematical impossibility. No vocabulary extension or constraint override will help. The user must reformulate the query.

For semantic conflicts, the derivation chain terminates in a vocabulary constraint. The rewrite hints can include: "Override constraint C-47 with authority X" or "Propose vocabulary extension that admits both properties." The system is not claiming the combination is impossible in all worlds—only that the current vocabulary does not support it.

This distinction respects the difference between what mathematics forbids and what institutions forbid. Both are real constraints. Only one is negotiable.

Temporal conflicts are a third category. Stale snapshots and version mismatches typically surface as obstruction witnesses under A23/A25 rather than refusals. If "as of timestamp T" is encoded as a hard constraint, then temporal conflicts become A27 triggers. Otherwise they are coherence failures, not refusals.

The Minimalist Maximalist Dress

Consider a query to a fashion catalog: "Show me minimalist maximalist dresses under $300."

Context U has:

• Signature Σ with predicates: minimalist/1, maximalist/1, dress/1, price/2
• Hard invariant C-47: $\forall x.\, \neg(\text{minimalist}(x) \land \text{maximalist}(x))$
• Logic $L_U$: classical with closed-world assumption on style taxonomy

Step 1: Parse query into constraints.

C_query_hard(Q) = {
  dress(x),
  minimalist(x),
  maximalist(x),
  price(x) < 300
}

Step 2: Combine with context invariants.

Step 3: Check satisfiability via constraint propagation.

From $C_{\text{hard}}$: minimalist(x) $\land$ maximalist(x).
From C-47: $\neg(\text{minimalist}(x) \land \text{maximalist}(x))$.
Contradiction: $\bot$.

Step 4: Extract unsat core.

UnsatCore = {
  constraints: ["minimalist(x)", "maximalist(x)", "C-47"],
  minimality: "subset-minimal"
}

Note: dress(x) and price(x) < 300 are not in the core. They do not contribute to the contradiction.

Step 5: Generate derivation chain.

DerivationChain = {
  steps: [
    ("minimalist(x) ∧ maximalist(x)", "conjunction of query terms", "query_constraint"),
    ("¬(minimalist(x) ∧ maximalist(x))", "C-47 from I_hard", "taxonomy_invariant"),
    ("⊥", "contradiction (P ∧ ¬P)", "refutation")
  ],
  final_step: "⊥"
}

Step 6: Produce RefusalArtifact.

RefusalArtifact = {
  result: ∅,
  reason: "unsatisfiable_constraints",
  
  unsat_core: {
    constraints: ["minimalist(x)", "maximalist(x)", "C-47: style exclusion"],
    minimality: "subset-minimal"
  },
  
  derivation: {
    steps: [...],
    final_step: "⊥"
  },
  
  witness: {
    class: "decidable",
    method: "constraint_propagation",
    sound: true,
    checkable: true
  },
  
  rewrite_hints: [
    "Try 'minimalist dresses' or 'maximalist dresses' separately",
    "Consider 'modern minimal' for restrained elegance"
  ]
}

Human-readable output:

Your query asks for dresses that are both minimalist and maximalist. These style categories are mutually exclusive (constraint C-47 in the style taxonomy). No dress can satisfy both criteria simultaneously.

Conflicting constraints:

• "minimalist" (from your query)
• "maximalist" (from your query)
• Style taxonomy rule C-47: a garment cannot be both minimalist and maximalist

Suggestions: Try searching for one style or the other.

The system refused gracefully, explained the conflict, and offered alternatives. The user learns something about the domain. The interaction succeeds even though the query does not.

Implementation Notes

Detection relies on standard tools: constraint propagation for small sets, SAT/SMT solvers (Z3(Bjørner 2008)Leonardo Mendonça de Moura and Nikolaj S. Bjørner, "Z3: An Efficient SMT Solver," in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008) (Springer, 2008), 337–340.View in bibliography, CVC5) for larger ones. Subset-minimal cores are polynomial to extract. The key design choice: A27 fires before query execution, not after. Constraint satisfiability is checked when the query contract (A25) is submitted. If unsatisfiable, the system returns a RefusalArtifact without touching the data layer. For most queries, this check is linear in constraint count.

Consequence

T1 is resolved. The system refuses gracefully when queries are logically impossible. The refusal is not a failure mode; it is a capability. The machinery from Parts II–V makes this possible:

• A1 defines consistency as the requirement that $C \not\vdash \bot$
• A18 provides the hard invariants that feed into $C_{\text{hard}}$
• A25 treats RefusalArtifact as a valid query outcome

The first fugue is complete. A coherent system does not hallucinate candidates for impossible queries. It explains why the query cannot be satisfied, what constraints conflict, and how the user might reformulate.

Chapter 26 takes up T2: pomegranates, properly. When the same word means different things in different contexts, how does the system disambiguate without losing either meaning?