# Negation: when "no" must be proven

In the last tutorial the negative support came from the case: the ethics
committee revoked the accreditation, and `accredited(Ivanova)` became
`FALSE_ONLY`. But the case is not the only source of "no", nor the main
one. More often "no" is spoken by the norm itself: "issue is not made",
"is not recognised", "is not entitled". In the corpus such a negative
head stands in two and a half thousand rules across 271 packages
(measured 05.09.2026).

This page is about three things formalisers confuse most often: where
negative support comes from, what `not p(x)` in a body actually reads,
and how "not established" differs from "refuted".

The same Archive of Veliky Ustin. Home issue of documents and overdue
returns join the registry and accreditation.

```law
language "law.core" version "0.2";
package tutorial.archive version "0.2.1";
namespace "urn:law:tutorial:archive";

entity Person;

relation in_researcher_registry(p: Person) kind institutional;
relation accredited(p: Person) kind institutional;
relation overdue_item(p: Person) kind empirical;
relation may_borrow(p: Person) kind institutional;
relation must_settle_before_visit(p: Person) kind institutional;
relation reference_check_required(p: Person) kind institutional;
```

## A norm that refuses

The issue rules say: a reader who has not returned a document on time is
not issued items for home use. This is not a missing permission but
a direct refusal, and it is written with a negative head.

```law
rule OverdueBlocksBorrowing strict {
    for p: Person;
    when overdue_item(p);
    then not may_borrow(p);
}
```

| Facts | `may_borrow` |
|---|---|
| overdue item | `FALSE_ONLY` |

Having fired, the rule places a negative support on `may_borrow(Ivanova)`,
the same kind the committee's revocation gave in the last tutorial. The
engine does not care where the support came from: a norm head, a case
fact, and a completeness closure (more on it two pages ahead) all write
into the same "against" column. The specification recognises exactly
three sources, no fourth, and that is the main thing to remember from
this page.

## What `not` reads in a body

A researcher refused issue must settle the debt before visiting. Here
the refusal is a premise, standing in the body with the same `not`.

```law
rule SettleBeforeVisit strict {
    for p: Person;
    when in_researcher_registry(p) and not may_borrow(p);
    then must_settle_before_visit(p);
}
```

| Facts | `must_settle_before_visit` |
|---|---|
| listed, overdue | `TRUE_ONLY` |
| listed, no overdue | `NEITHER` |
| listed, refusal recorded in the case | `TRUE_ONLY` |
| listed, overdue plus a "issue allowed" record | `NEITHER` |

A bare literal in a body reads as `established`; we saw that across the
four states. `not p(x)` reads symmetrically, as `refuted(p(x))`: the body
needs an established negative support, `FALSE_ONLY`, and nothing else.

**The second row is the most important on the page.** For
`may_borrow(Ivanova)` there is neither an overdue item nor a record. The
rule does not "fire with a no answer"; it stays silent. There is no
negation by failure in the core: what nobody permitted is not yet
forbidden, and the silence of rules remains silence.

The third row is a refusal written into the case by hand, like the
committee's revocation in the last tutorial: `assert not may_borrow(…)`.
For the body it is the same "against" support as a norm's conclusion.

The fourth is `BOTH`. The librarian recorded "issue allowed" while the
norm refused; `may_borrow` now holds both supports. `not may_borrow(p)`
requires `FALSE_ONLY`, not "any support against at all", and on
a contradictory input the rule draws no conclusion, just as it drew none
on `BOTH` in a positive premise.

## A rule that will never fire

Remove the refusing norm and keep everything else. The compiler is
content, the layer is as before, but `SettleBeforeVisit` is dead: with
an overdue item, with anything, the answer is `NEITHER`. Only a refusal
written into the case by hand can revive it.

| What is in the package | `must_settle_before_visit` when overdue |
|---|---|
| with `OverdueBlocksBorrowing` | `TRUE_ONLY` |
| without it | `NEITHER` |

This is the formaliser's most frequent mistake, and it is caught by
a question worth asking of every `not p(x)` in a body: **who produces
`not p`?** A norm head, a case fact, or closure. If there is no answer,
yet you meant to write "unless otherwise established", then this is not
negation. It is ignorance, covered in the next section.

With the refusing norm cut out the answer is `NEITHER`: the lesson of
the dead rule holds just like the lesson of the live one.

## Ignorance is not negation

While nothing is established about a researcher's accreditation, the
archive requests a background check. That can be called neither a refusal
nor a ban: the norm acts on the gap case.

```law
rule ReferenceCheck strict {
    for p: Person;
    when in_researcher_registry(p) and not_known(accredited(p));
    then reference_check_required(p);
}
```

| Facts | `reference_check_required` | `accredited` |
|---|---|---|
| listed | `TRUE_ONLY` | `NEITHER` |
| listed, accredited | `NEITHER` | `TRUE_ONLY` |
| listed, accreditation revoked | `TRUE_ONLY` | `FALSE_ONLY` |

`not_known(P)` is true when `P` has no positive support after all its
producers have run. The question is different: not "is it refuted"
but "is it established". Hence two consequences, both visible in
the table.

`not_known` refutes nothing. The check is requested, while accreditation
in the first row stayed `NEITHER` and did not become `FALSE_ONLY`.
Writing `not_known` where a true refusal is needed yields a rule whose
head fires while the "no" never appears.

`not_known` does not mean "nothing is known". Third row: the committee
revoked the accreditation, there is no positive support, and the check is
requested, although plenty is known about the reader. If the norm says
"while there is no evidence at all", a status test `unknown(P)` is
needed: it is true only at `NEITHER`.

For "not established" the engine pays with ordering: to answer that
there is no positive support, it must wait for all producers of
`accredited`. That is why the layer view of this page shows
**L1**, not L0, with the note "default negation `not_known`".
A cycle through `not_known` of the form "A if B is not known; B if A is
not known" is rejected statically by the compiler: `LDC-E4102`.

## Three compiler refusals

`not` takes exactly one atom. The compiler does not apply de Morgan's
laws, and `not (A and B)` in a body is not a shorthand but an error:

```text
error LDC-E1305: not поверх не-атома в теле — вне L0-среза (§190)
```

The diagnostic reads: "`not` over a non-atom in a body — outside the L0 slice".

Write `not A or not B`, or introduce a predicate with a rule and negate
it.

Negation does not bind a variable. Leave in `SettleBeforeVisit`'s body
only `not may_borrow(p)` and `p` has no source of values:

```text
error LDC-E4101: SettleBeforeVisit: head использует несвязанные переменные [p]
— правило не range-restricted (§190: связывание только позитивным
established-конъюнктом конечного источника)
```

The diagnostic reads: "`SettleBeforeVisit`: head uses unbound variables [p] — the rule is not range-restricted: a variable must be bound by a positive established conjunct of a finite source".

Next to a negation there must stand a positive literal enumerating the
candidates; here it is the registry. Both refusals above belong to the
language itself: the compiler rejects such variants with exactly
these codes.

The third refusal is softer and hence more dangerous. `not_known` is
allowed only in a body; placed in a head, it yields warning `LDC-E1302`,
`check` stays green, and the whole rule drops out of the CLIR. The norm
looks written and does not exist. Read the `check` warnings: the broken
variant still compiles, and the `LDC-E1302` code must sound in them.

## Next

A negative head can refuse, but answers only for itself. Put next to it
a general norm that permits, and the answer will be `BOTH`, as in the
fourth row of the second table. For one norm to defeat another, defeat
and priority are needed: [the next tutorial](/tutorials/defeaters/).

The exercise for this page is [/tutorials/exercise-negation/](/tutorials/exercise-negation/).