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.

OverviewBoundariesCorpus formsPitfalls

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

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

Output

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.
• The closed-world and defeaters tutorials live in the tutorials catalogue.
• Neighbour pages: strict rules, facts and evidence, 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

Show syntax reference

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

Grammar

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

Grammar

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 ;