# Negation and truth statuses

**In one sentence:** “no” (`not p` — established absence with its own
source) and “unknown” (Not established, not refuted — support silence, `not_known` — a
check-stage test) are different answers at different prices; the author takes
explicit negation when the absence has a holder (a refusal-norm, a negative
fact, closure), and `not_known` when the rule must fire exactly
while nothing is known yet.

The language specification treats established absence and unknown as
different answers: “no” needs its own source — a refusal-norm, a negative
fact, or a closure — while `not_known` fires exactly while nothing is known
yet and proves nothing about the atom itself.

## 1. When to use and when not to

| Instead | Selection rule |
|---|---|
| `not p(x)` in a body vs `not_known(p(x))` | `not p` requires Refuted — established negative support. If there is no completeness holder but the meaning is “not otherwise established”, `not_known` is needed, not `not`: bare `not` without a source gives Not established, not refuted forever (trap 1, `LDC-E4113`) |
| `not_known(P)` vs `closure` | `not_known` does not refute `P` and gives no certificate: the answer on `P` stays Not established, not refuted. Where the registry is complete and the completeness has a holder — `closure` with `derive_explicit_negative true`, and only there |
| `refuted(p(x))` vs `not p(x)` in a body | Equivalent in reading (`not p` is Refuted), but a status test does not bind variables: a positive conjunct is needed nearby, otherwise `LDC-E4101` |
| `established(p(x))` vs bare `p(x)` in a body | A bare literal already reads as established (Established); the explicit test is written for readability, not for new meaning |

## 2. Minimal example

Package `research.negation.explicit_negation`: a refusal-norm (licence revocation
extinguishes it) and a consequence rule (an unlicensed registry carrier is
suspended).

```law
rule RevocationNegatesLicence strict {
    for c: Carrier;
    when licence_revoked(c);
    then not licensed(c);
}

rule SuspendUnlicensed strict {
    for c: Carrier;
    when in_registry(c) and not licensed(c);
    then must_suspend(c);
}
```

Case 01 facts: `in_registry(alpha)` + `licence_revoked(alpha)`. Query:
`evaluate truth(must_suspend(alpha))`.

Actual engine answer:

```text
law test research.negation.explicit_negation: мир research.negation.explicit_negation
  ok   [research.negation.explicit_negation#authored] tests/01-suspension-follows.lawtest / urn:query:research-negation-01
  ok   [research.negation.explicit_negation#authored] tests/02-no-source-no-suspension.lawtest / urn:query:research-negation-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0
```

`law engine check` — `check OK`, no warnings: the negativity producer
(`RevocationNegatesLicence`) is in the package, `LDC-E4113` is silent.

Sensitivity: removing the `licence_revoked` fact changes the expectation
from Established to Not established, not refuted (the no-source test)
— the `not licensed` lost its only negative support, the second rule’s body does
not hold, the example is not vacuous. The reverse mistake would be
expecting the absence of positive support to give `not licensed` on its
own: it does not.

Second package `research.negation.not_known_step` — a check stage: while nothing is
known about the tax certificate, the carrier is sent for inspection; the
arrival of the `tax_clearance` fact extinguishes `not_known` and the answer
changes from Established to Not established, not refuted. Runs — 2/2, `check OK`.

## 3. Example by domain

- **Law:** package `tr.constitution` (Constitution of Türkiye) —
  “a state whose non-performance is not established counts as performing the
  task”: `when not_known(state_task_failure(polity, task))`. Exemplary “counts as, until established”.
- **Customary law:** package `ie.clonmel.code_duello` (Code Duello, Irish duelling code) —
  `when quarrel_recorded(q) and not_known(ground_taken(q))`:
  the duel code reads the record’s silence as grounds for apology.
- **Regulation (teaching case):** package `research.negation.explicit_negation` — a carrier
  licence registry: revocation as a refusal-norm, suspension as a
  consequence of established absence.
- **Religion, science, sport:** in the checked fragments, negation in this
  pair of forms did not occur; the selection rule does not depend on domain
  — it depends on whether the absence has a holder. No fictitious
  “debatable” case is given here.

## 4. How the engine answers

Table — actual runs of this section’s teaching packages:

| Facts | Question | Answer | Why |
|---|---|---|---|
| `in_registry`, `licence_revoked` | `must_suspend` | Established | the `then not licensed` head gave negative support, the `not licensed` body read Refuted |
| `in_registry` | `must_suspend` | Not established, not refuted | `licensed` has no support at all; absence of data is not negation |
| `in_registry` | `clearance_check_required` | Established | nothing known about the certificate — `not_known` is true |
| `in_registry`, `tax_clearance` | `clearance_check_required` | Not established, not refuted | positive support exists — `not_known` is false, and it did not infer `not tax_clearance` |

Additionally, further checked behaviours of the earlier edition (these teaching packages
hold no closures — the behaviour is stated from the language description, not from runs):

| Facts | Question | Answer | Why |
|---|---|---|---|
| `in_registry`, `licensed` | alpha’s `licensed` | Established | the record exists; the closure stays silent |
| `in_registry` | alpha’s `licensed` | Refuted | in-domain, no record — the closure’s negative |
| nothing | beta’s `licensed` | Not established, not refuted | outside the domain the closure says nothing |
| same, closure cut; `in_registry` | alpha’s `must_suspend` | Not established, not refuted | without a negativity source the body never holds (counterfactual) |
| `in_registry` | alpha’s `barred_from_tender` | Established | `refuted(licensed)` — the same negative via status test |
| beta’s `licence_revoked` | beta’s `licensed` | Refuted | a negative head works outside the domain too |
| `in_registry`, `licensed`, `licence_revoked` | alpha’s `licensed` | Contradiction | the fact gives positive, the strict refusal-norm gives negative support; neither extinguishes the other |
| same | alpha’s `must_suspend` | Not established, not refuted | `not licensed` requires Refuted, not Contradiction |
| `in_registry` | alpha’s `uninsured_notice` | Not established, not refuted | `insured` has no negativity source at all |
| `in_registry`, `not insured` | alpha’s `uninsured_notice` | Established | a negative case fact is a source |
| `not insured` | alpha’s `insured` | Refuted | a `not p(x)` fact is stored as its own support |
| `in_registry` | alpha’s `audited` | Not established, not refuted | `derive_explicit_negative false`: no negative |

- Positive and negative support are independent: Established is positive only,
  Refuted is negative only, Contradiction is both, Not established, not refuted is neither.
  The Contradiction row (a `licensed` fact + revocation) is not covered by a run
  in these teaching packages: both readers `p(x)` and
  `not p(x)` stay silent on Contradiction.
- In `why_not`, absent support gives Not established, not refuted without naming a culprit:
  the engine does not distinguish “the fact has not arrived yet” from “the
  fact will never come”.
- A closure with `derive_explicit_negative true` carries a closure
  certificate in the proof graph; these teaching packages
  hold no closures — the behaviour is stated from the language description,
  not from runs.
- A support conflict (Contradiction) is read by neither side: an atom in Contradiction
  activates neither `p(x)` nor `not p(x)`. One side of the
  conflict is taken only through `supported(P)` — that reading
  was not run in the teaching packages and is marked here as stated from the
  language description, not as a run fact.
- The second package’s sensitivity mirrors the first: in
  the check-while-unknown test the Established answer rests on the
  absence of `tax_clearance` support; adding exactly one `tax_clearance`
  fact (the known-clears-check test) gives Not established, not refuted. The rule did
  not “change its mind” and did not infer `not tax_clearance` — it simply
  stopped firing (`not_known` refutes nothing).

## Status tests: what is executable in 0.2

Six readings are executable: `established`, `supported`, `refuted`,
`unknown`, `monotone`, and `not_known`. Reserved past 0.2 —
`opposed`, `conflicted`, `no_evidence`: the lexer rejects them as terms,
`LDC-E0201`. The Refuted branch covers `refuted(P)`; the
Contradiction branch is not read by a separate test in 0.2 — a conflict is taken
through `supported(P)`.

Stratification: `default` (`not_known`) and `status` (`established`,
`refuted`, `unknown`, bare atom) edges cannot enter a cycle — `LDC-E4102`.
All producers of both polarities of `P` complete before the
first status reader (completion barrier); a strict `not_known(P)`
reader over a defeasible producer is `LDC-E4103`.

## 5. Common mistakes

1. `when not p(x)` without a negativity source — Not established, not refuted forever,
   warning `LDC-E4113` (pitfalls, item 1).
2. `not_known` instead of a closure: no refutation and no certificate
   (pitfalls, item 2).
3. A closure without a mandatory field (`predicate`/`domain`/`snapshot`/
   `complete_as_of`) — `LDC-E1307` (pitfalls, item 3).
4. `derive_explicit_negative false` — the closure exists, no negatives
   (pitfalls, item 4).
5. `not (A and B)` — `LDC-E1305`, negation only over an atom
   (pitfalls, item 5).
6. A status test as the only conjunct — `LDC-E4101`, the test does not bind
   variables (pitfalls, item 6).

## 6. References

- Syntax — section 7 below (grammar excerpts); the carrier licence
  registry — section 2 above; the corpus counts — the
  [corpus forms](/constructs/negation-and-status/corpus-forms/).
- The [closed-world](/tutorials/closed-world/) and [defeaters](/tutorials/defeaters/)
  tutorials live in the tutorials catalogue.
- Neighbour pages: [strict rules](/constructs/rule-strict/),
  [facts and evidence](/constructs/facts-and-evidence/),
  [priority](/constructs/priority/).
- The pitfalls page lists the diagnostics (`LDC-E4113`, `LDC-E1307`,
  `LDC-E1305`, `LDC-E4101`, `LDC-E4102`, `LDC-E4103`, `LDC-E0201`) with wrong
  forms and fixes.

## 7. Grammar excerpts

A literal, a call, and arguments; status tests (the `proposition`,
`predicate_call`, `argument`, `argument_list`, `named_argument`,
`status_test`, `status_function` productions; the `_` position and named
arguments are checked by lowering, not by the grammar):

```ebnf
proposition             = [ "not" ], predicate_call ;
predicate_call          = qualified_name, "(", argument_list, ")" ;
(* Errata E-0165 (§98): подчёркивание аргументом литерала тела правила —
   экзистенциальный аргумент «есть какое-либо значение». Законная позиция
   одна — положительный литерал тела; в голове, под `not`, в статус-тесте,
   внутри терма, в утверждении дела и в вопросе `_` по-прежнему не терм
   (E-0041, LDC-E0207) — позицию проверяет lowering, а не грамматика. *)
argument                = expression | "_" ;
(* Errata E-0195 (§59, DECISION-0342): третья альтернатива — полная форма
   агрегата `sum(xs, empty: 0 KZT)`: коллекция позиционно, политика пустоты
   и округление именами. Позиционный аргумент после именованного не
   разбирается ни в одной из трёх форм. Какие вызовы вправе её писать —
   вопрос статической семантики §189, а не грамматики: у relation смешение
   по-прежнему LDC-E0201, у функции и конструктора имена по-прежнему
   LDC-E2140. Та же граница, что у `_` выше: форму даёт грамматика, позицию
   проверяет lowering. *)
argument_list           = [ argument, { ",", argument }, [ "," ] ]
                        | named_argument, { ",", named_argument }, [ "," ]
                        | argument, { ",", named_argument }, [ "," ] ;
named_argument          = identifier, ":", argument ;

(* RESERVED 0.2: `opposed`, `conflicted` и `no_evidence` не реализованы ни
   одной реализацией (лексер их отвергает как терм) и ждут семантики BOTH-
   ветви §62 и EvidencePolicy §61; шесть остальных статусов исполнимы
   (DECISION-0072). *)
status_test             = status_function, "(", proposition, ")"
                        | "no_evidence", "(", proposition,
                          [ ",", "policy", "=", reference ], ")" ;
status_function         = "established" | "supported" | "refuted"
                        | "monotone"
                        | "opposed" | "conflicted" | "unknown"
                        | "not_known" ;
```

A closure (the `closure_decl`, `closure_item` productions;
`predicate`, `domain`, `snapshot`, `complete_as_of` are mandatory):

```ebnf
closure_decl            = "closure", identifier, "{",
                            { closure_item },
                          "}" ;
closure_item            = "predicate", reference, ";"
                        | "domain", expression, ";"
                        | "snapshot", reference, ";"
                        | "complete_as_of", temporal_literal, ";"
                        | "derive_explicit_negative", boolean_literal, ";"
                        | effective_clause
                        | label_item
                        | metadata_item ;
```