Markdown for LLMs

Use a disputed fact deliberately

The source Markdown for this article. Copy it into your assistant or download it as a text file.

# Use a disputed fact deliberately

## Intention

I want to order a review when there is positive support, even if the fact is contested.

## Incorrect form and why it stays silent

A bare atom requires TRUE_ONLY and stays silent on BOTH:

```text title="Incorrect form"
when registered(p) and (eligible(p));
```

## Correct form

```law
language "law.core" version "0.2";
package recipes.v.r06 version "0.1.0";
namespace "urn:recipe:v-negation:06";

entity Person;
relation registered(p: Person);
relation eligible(p: Person);
relation review(p: Person);
// rationale: наличие положительного основания достаточно для проверки;
// спор об eligible при этом сохраняется и не считается разрешённым.
rule Review strict {
    for p: Person;
    when registered(p) and supported(eligible(p));
    then review(p);
}
```

## Frozen execution scene

| Facts | Question | Answer |
|---|---|---|
| registered, eligible | review(a) | TRUE_ONLY |
| registered, eligible, not eligible | eligible(a) | BOTH |
| same both supports | review(a) | TRUE_ONLY |
| same both supports, supported removed | review(a) | NEITHER |
| registered, only not eligible | review(a) | NEITHER |

## Counterfactual

evaluates.without removes the word supported: a lawful formula `(eligible(p))` remains, and the conflict no longer activates Review. That is a change of reading, not deletion of the negative fact.

## Boundary

Positive support does not resolve the dispute. The reason for the deliberate reading is written in the rationale comment. Recursion without that intention uses [Walk a chain with strict recursion](/recipes/v-negation/recursive-chain/).

## Pitfall

Using supported for ordinary recursion needlessly lifts the whole package to a higher stratum; monotone keeps it low. Here the higher stratum is chosen on purpose: we care about the positive side of a disputed fact. Both supports yield BOTH, an ordinary reader stays silent, and supported derives review. Replacing the test does not resolve the contradiction itself.