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.

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

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

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

Arxo 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:

Output

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:

Output

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.

The exercise for this page is /tutorials/exercise-negation/.