The Refusal Obligation

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."

Suppose 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.

The proposed numbers fail the conditions, and there is a stronger reason no corrected list of examples can succeed: no such numbers exist. A prime greater than 2 cannot be divisible by 4. The query is logically impossible. The assistant should have explained why the requested set is empty. Instead, it hallucinated candidates for an empty set.

T1 asks what the recipient gains from more than failed candidates. The short derivation excludes every number under the stated arithmetic interpretation. A generator can produce that derivation too; what matters is whether the receiving procedure checks and preserves its grounds, rather than accepting another plausible list.

An ordinary database query can correctly return the empty relation: 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.

Returning that empty relation meets an ordinary retrieval contract. A27 proposes a further explanatory obligation where the service undertakes to diagnose unsatisfiable constraints. The failed generation and the correct empty query are not equivalent errors.

Contingent Versus Logical Emptiness

An empty table and an inconsistent request invite different next steps.

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 catalog satisfying the stipulated exclusion could contain such an item. The exclusion is this taxonomy’s modeling choice. 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_1, ..., c_k],
  minimality: "subset-minimal" | "not-established"
}

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
}

The core identifies commitments that cannot all be true together; the derivation chain shows how they conflict. A subset-minimal core also establishes that removing any one of its commitments restores consistency. The witness supports the refusal under the declared interpretation and hard constraints, whether or not that additional minimality check has been completed.

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.

Mathematical incompatibility follows under the stated arithmetic interpretation. "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.

Taxonomy conflict follows from an additional declared classification rule. "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. Differently dated snapshots are not inherently contradictory. An obstruction requires incompatible assertions under the same temporal interpretation; a stale record used as current may instead violate a freshness contract. 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 and dress/1, and a price function on items
• 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"
}

Dress(x) and price(x) < 300 are not needed for this contradiction. The displayed core is subset-minimal under the toy interpretation: dropping either positive predicate lets it be false while the other is true; dropping C-47 allows both to be true. These assignments establish the three required deletion checks.

Step 5: Generate derivation chain.

DerivationChain = {
  steps: [
    (["minimalist(x)", "maximalist(x)"], "conjunction", "minimalist(x) ∧ maximalist(x)"),
    (["C-47"], "universal instantiation", "¬(minimalist(x) ∧ maximalist(x))"),
    (["minimalist(x) ∧ maximalist(x)", "¬(minimalist(x) ∧ maximalist(x))"],
     "contradiction", "⊥")
  ],
  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¹, CVC5) for larger ones. A deletion procedure can use linearly many satisfiability-oracle calls; that is not a polynomial runtime bound for arbitrary constraints. The key design choice: For these examples, the contradiction can be established from the declared constraints before searching the catalog. The query service can return that refusal when the contract is submitted. A different check may need data, external evidence or computation before its result is established. The cost depends on the logic and representation. A resource-bounded checker must distinguish a proved contradiction from an inconclusive search; A27 does not make general satisfiability decidable.

Consequence

For the stipulated prime query and fashion taxonomy, the derivation establishes why adding more candidates cannot help. That answer lets the user reconsider a constraint instead of repeatedly enlarging a search. It differs from both a correct empty retrieval and a check that ran out of resources.

A27 asks the implementation to preserve the distinction. When unsatisfiability has been established, its grounds belong in the result. When the required examination is unfinished, the system has no such explanation to give. It must retain the missing obligation rather than manufacture either a candidate or a proof of impossibility.

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?