Skip to content
docs
Arxo ↗

nb-19 — Unknown, presumed and deemed: negation, closure, presumptions, fictions, constraints

For LLMs10 sections
← Course mapChapter 19 / 25 · Advanced II

Northbridge course, Stage 4 areas B+C (needs beginner only: nb-01: First permit: facts, a rule and a question → nb-02: Why a missing fact is not a refusal). Northbridge is synthetic; every applicant, file, notice and fee below is fictional and unofficial. No real municipal deployment or legal-validity claims. Tool law 0.1.0, language version 0.2, semantics law.core/0.2, std 0.2.0 (from law --version, quoted below).

Mira, the Northbridge permits clerk, faces four files on one morning. Ann’s file is empty: no residence record, no denial either. Bob’s file holds two residence records that contradict each other. Carl is listed in the residents’ file index but has no residency record. Dana is not in the index at all. On top of that, the office applies three “as-if” tools: every applicant is treated as being in good standing until an unpaid fine shows up; a posted notice counts as received; and a permit may be issued only after the fee is paid — while a separate rule adds a late fee when it was not. The auditor’s question: which of these unknowns, presumptions and deemed facts does the machine actually establish — and which tool did the work in each case?

Mira needs sharp lines between these tools. Unknown means absence of support: neither a fact nor its denial is established (NEITHER). An explicit denial — written with assert not or derived by a rule head then not … — is support against a statement, and can yield FALSE_ONLY. And not_known(p(x)) is a condition that holds when nothing establishes p(x); it lets a rule react to silence.

A closure declares one file complete for one predicate, so inside that file absence becomes denial. A presumption concludes something by default until rebutting evidence arrives. A fiction deems a fact from its trigger with no rebuttal path.

A constraint is different in kind: it reports a violation as a finding and never concludes anything itself. The late fee in Mira’s files comes from a separate rule standing next to the constraint.

nb-01: First permit: facts, a rule and a question: facts, strict rules, the four truth statuses (TRUE_ONLY, FALSE_ONLY, NEITHER, BOTH), and law test as the way to check a claim. nb-02: Why a missing fact is not a refusal: a missing fact is unknown, not a refusal — silence yields NEITHER. nb-06: When the register may stay silent: register silence and the file index as a completeness domain.

New here: not in heads, conditions and assertions; not_known in conditions; closure … derive_explicit_negative; presumption … presume … unless; fiction … deem; and constraint … require … severity error, standing next to a rule that carries the separate legal consequence.

Excerpts 1–7 are from packs/examples/language-demo/unknown/package.law (identifiers as written; the other area’s block cut in each case).

Excerpt 1 — explicit denial in a rule head (lines 25–29). The area-C block and the remaining area-B rules are cut.

Arxo Law
rule DenyListed strict {
for a: Applicant;
when blacklisted(a);
then not permit_ok(a);
}

One idea: a denial is derived support against the conclusion, not the absence of support for it.

Look at the head: then not permit_ok(a) concludes the denial of eligibility from a blacklist record. Nothing is missing here — the rule produces positive evidence against the permit.

Excerpt 2 — not_known beside explicit not (lines 33–43). Heads, closure and area C are cut.

Arxo Law
rule NeedsReview strict {
for a: Applicant;
when applied(a) and not_known(resident(a));
then needs_review(a);
}
rule ClearWhenDenied strict {
for a: Applicant;
when applied(a) and not resident(a);
then cleared(a);
}

One idea: the two rules differ by one token. NeedsReview fires on silence; ClearWhenDenied needs a denial.

Compare the two when lines token by token: applied(a) and not_known(resident(a)) against applied(a) and not resident(a). Everything else is identical, so the suite pair in section 4 tells exactly these two conditions apart. Both rules need the positive binder applied(a): a bare not_known(resident(a)) or not resident(a) binds no variable, and the engine refuses the rule (LDC-E4101, observed while writing this article).

Excerpt 3 — the closure (lines 45–51). Rules and area C are cut.

Arxo Law
closure FileComplete {
predicate resident;
domain on_file;
snapshot "urn:snapshot:demo-northbridge-unknown:2026";
complete_as_of @2026-01-01T00:00:00Z;
derive_explicit_negative true;
}

One idea: completeness is declared per predicate (resident) over one domain (on_file) at one moment — never “the file is complete”.

Read the three bound lines together: predicate says which statement the file speaks about, domain says whose records count, and the snapshot plus timestamp say as of when. The last line, derive_explicit_negative true, is what turns absence into denial inside those bounds.

Excerpt 4 — the presumption (lines 63–67). Fiction, constraint and area B are cut.

Arxo Law
presumption Standing(a: Applicant) {
when applied(a);
presume standing(a);
unless unpaid(a);
}

One idea: a default with a named exit — unless withdraws the conclusion instead of denying it.

Follow the three lines in order: when applied(a) opens the default for every applicant, presume standing(a) states what holds by default, and unless unpaid(a) names the one exit. The rebuttal does not conclude not standing(a) — it takes the conclusion away.

Excerpt 5 — the fiction (lines 69–73). Everything else is cut.

Arxo Law
fiction DeemedReceipt strict {
for a: Applicant;
when posted(a);
deem received(a);
}

One idea: no unless, no default — the trigger establishes the deemed fact unconditionally.

Notice what is missing beside deem received(a): there is no unless line and no rebuttal path. Posting the notice is enough — but without a posting, the fiction gives nothing, as the second fiction test shows.

Excerpt 6 — the constraint (lines 75–80). The rule below is cut.

Arxo Law
constraint IssueNeedsFee(a: Applicant) {
when issued(a);
require fee_ok(a);
severity error;
message "a permit is issued only after the fee is paid";
}

One idea: a finding, not a conclusion — a violation is reported as issue(CONSTRAINT_VIOLATED) while the triggering fact stays true.

Read when issued(a) as the trigger and require fee_ok(a) as the demand: an issued permit must come with a paid fee. The severity and message lines shape the finding. Nothing here concludes a new fact — the price of the breach lives in the next block.

Excerpt 7 — the separate consequence (lines 82–86). Everything above is cut.

Arxo Law
rule LateFee strict {
for a: Applicant;
when issued(a) and not fee_ok(a);
then late_fee(a);
}

One idea: the legal consequence lives in an ordinary rule next to the constraint — two mechanisms, one shared trigger.

This is a plain strict rule: issued plus explicitly unpaid fee yields a late fee. Note the not fee_ok(a) condition — mere silence about the fee does not trigger it, as exercise question 4 explores.

Record the build first:

Terminal
law --version

Observed:

Output
law 0.1.0
семантика: law.core/0.2
std для языка 0.2: 0.2.0

The Russian lines name the semantics (law.core/0.2) and the standard library for language 0.2 (0.2.0). Every status below holds for exactly this build.

Run the suite:

Terminal
law test packs/examples/language-demo/unknown

Observed (engine law 0.1.0):

Output
ok [demo.northbridge.unknown] tests/unknown.lawtest / silence is neither, support absent
ok [demo.northbridge.unknown] tests/unknown.lawtest / explicit denial is false
ok [demo.northbridge.unknown] tests/unknown.lawtest / contradiction is both
ok [demo.northbridge.unknown] tests/unknown.lawtest / unknown triggers review
ok [demo.northbridge.unknown] tests/unknown.lawtest / proof stops review
ok [demo.northbridge.unknown] tests/unknown.lawtest / denial clears
ok [demo.northbridge.unknown] tests/unknown.lawtest / silence does not clear
ok [demo.northbridge.unknown] tests/unknown.lawtest / closure: on file without a record is denied
ok [demo.northbridge.unknown] tests/unknown.lawtest / closure: outside the file silence stays
ok [demo.northbridge.unknown] tests/unknown.lawtest / closure does not leak to other predicates
ok [demo.northbridge.unknown] tests/unknown.lawtest / presumption holds by default
ok [demo.northbridge.unknown] tests/unknown.lawtest / rebuttal withdraws the presumption
ok [demo.northbridge.unknown] tests/unknown.lawtest / fiction deems receipt
ok [demo.northbridge.unknown] tests/unknown.lawtest / fiction needs its trigger
ok [demo.northbridge.unknown] tests/unknown.lawtest / constraint reports the violation
ok [demo.northbridge.unknown] tests/unknown.lawtest / unpaid issue carries a separate consequence
ok [demo.northbridge.unknown] tests/unknown.lawtest / fee paid: no consequence
итого: 17 проверено, 17 прошли, 0 не прошли, 0 не исполнены; код 0

All 17 tests pass. The summary is in Russian: 17 checked, 17 passed, 0 failed, 0 skipped, exit code 0. Read the test names as a map of the article: silence, denial and contradiction come first; then the two comparable pairs (review on silence versus proof, clearing on denial versus silence); then the three closure edges; then the presumption, fiction and constraint pairs. A passing test means the answer matched its expectation — it does not mean any applicant was cleared or charged.

Terminal
law engine check packs/examples/language-demo/unknown

Observed: check OK: packs/examples/language-demo/unknown.

Terminal
law fix imports packs/examples/language-demo/unknown

Observed: the package line plus блоки 'use self' канонические — nothing to rewrite (exit 0).

The static check passes, and the second verdict — in Russian, “use self blocks are canonical” — confirms the borrow lists need no rewriting.

Explicit not. Mira’s blacklist file needs support against a conclusion. DenyListed turns a blacklist record into truth(permit_ok) == FALSE_ONLY: the test explicit denial is false expects FALSE_ONLY plus applied(DenyListed). Dropping the rule would not do — silence gives NEITHER, and the first test shows not applied(Grant) with not applied(DenyListed).

Why not a defeater for the blacklist?

A defeater removes support without denying, so the answer would stay NEITHER instead of becoming FALSE_ONLY. Defeaters and priorities belong to nb-03: Exceptions and conflicting rules; this package needs a denial, not a defeat.

not_known. The review rule reacts to silence inside a rule. NeedsReview fires exactly when nothing establishes residence; adding the residence record flips the same question to NEITHER (unknown triggers review versus proof stops review — only the studied record changes). What this does NOT prove: that the fact is false. The review fires because the office does not know, not because it denied.

Explicit-not condition. Clearing requires a denial, not mere silence. ClearWhenDenied fires on assert not resident and stays silent on an empty file (denial clears versus silence does not clear — only the denial changes). The pair with the previous paragraph is the point: on the same empty file, needs_review is true while cleared stays unknown.

BOTH. Contradictions stay visible instead of resolving silently. Two records disagreeing about residence give BOTH for resident, and Grant still does not fire on a disputed premise. Not proven: any priority between the records — there is none in this package.

Closure. A complete file speaks denial inside its bounds. Carl, on file with no record, is FALSE_ONLY for resident; Dana, not on file, stays NEITHER; and Carl stays NEITHER for permit_ok — the closure covers resident only and never leaks to other predicates. Three tests, one mechanism, three edges.

Presumption. Good standing holds by default until evidence withdraws it. Applied with no fine record, standing is TRUE_ONLY; adding the fine record withdraws it to NEITHER — not to denial (only the rebutting record changes). This exercises matrix row DEMO-NB-P2-02 (default) and DEMO-NB-P2-03 (rebuttal), previously mentioned-only.

Fiction. A posted notice makes receipt TRUE_ONLY with no empirical receipt premise; an application alone leaves receipt NEITHER — fiction is not a default, it needs its trigger. Nothing rebuts it: no unless exists. This exercises DEMO-NB-P2-04.

Constraint plus consequence. The breach is reported and priced, separately. An issued permit with assert not fee_ok keeps issued true, raises issue(CONSTRAINT_VIOLATED), and derives late_fee through the adjacent rule; with the fee paid there is no consequence. Finding and consequence share a trigger and nothing else. This exercises DEMO-NB-P2-05.

Take unknown triggers review: Ann applied, nothing is known about her residence, and needs_review is TRUE_ONLY. Change exactly one condition — assert the residence record (proof stops review) — and the same question becomes NEITHER: not_known(resident(ann)) no longer holds, so the rule does not fire.

Now replay the same change against the neighbouring rule. In silence does not clear, asserting the residence record also leaves cleared at NEITHER — but asserting the denial (denial clears) flips it to TRUE_ONLY. One added record flips the not_known rule off; only an added denial flips the not rule on. Silence, proof and denial are three different inputs, and the suite tells them apart.

The mistake is treating the constraint as the consequence: deleting LateFee and expecting late_fee to follow from IssueNeedsFee. The observed consequence is that the unpaid issue carries a separate consequence test fails — nothing derives late_fee, because a constraint never concludes anything; it only reports issue(CONSTRAINT_VIOLATED).

The mirror mistake is treating the rule as the check: deleting the constraint keeps late_fee derivable, but the violation finding disappears. The fix in both directions is to keep the two mechanisms side by side. Rule of thumb: the constraint watches and reports; the rule prices and concludes. If either is missing, exactly one of the two observable effects goes missing with it.

Verified profile only. Every status above holds for tool law 0.1.0, language 0.2, semantics law.core/0.2, std 0.2.0. Other builds have their own support lists; re-run, do not assume.

Range restriction is a language fact. A condition made only of not … or not_known(…) binds no variable (§190): the rule is refused with LDC-E4101 until a positive conjunct (applied(a)) binds it. This refusal is observed, not hypothetical — the first draft of this package hit it.

Closures are bounded. FileComplete speaks only about resident, only for on_file members, only as of its snapshot. Outside all three bounds, silence stays silence — the suite pins all three edges.

Presumption withdrawal is not denial. Rebuttal yields NEITHER, never FALSE_ONLY. Fiction has no withdrawal at all. A constraint finding is not support for or against any fact.

Refusals are profile facts. LDC-E4101/LDC-E0201 (seen during authoring: unbound heads, double assertion ids) describe this build’s static checks, never a language-wide inability.

Predict each answer without running the engine, then check with law test packs/examples/language-demo/unknown:

  1. Carl is on file with no residence record. truth(resident(carl)) versus truth(permit_ok(carl)): which status each, and which declaration explains the difference?
  2. Ann applied and her residence is unknown: truth(needs_review(ann)) versus truth(cleared(ann)). Then assert not resident(ann): which of the two flips, and to what?
  3. Ann applied and posted nothing, but has an unpaid fine on record: truth(standing(ann)) versus truth(received(ann)) — which mechanism answers each, and why does the fine touch only one?
  4. Ann’s permit is issued and the fee record is absent entirely (neither fee_ok nor its denial asserted): does the constraint report a violation, and is late_fee derived? What differs from the assert not fee_ok case in the suite?
  5. Assert both resident(ann) and not resident(ann): what is truth(resident(ann)), and does Grant fire for her?

Write down each prediction first; run the suite; explain any miss in one sentence. Check your work against the full solution.

  • Source: packs/examples/language-demo/unknown/package.law (area-B rules Grant, DenyListed, NeedsReview, ClearWhenDenied, closure FileComplete; area-C presumption Standing, fiction DeemedReceipt, constraint IssueNeedsFee, rule LateFee)
  • Tests: packs/examples/language-demo/unknown/tests/unknown.lawtest (17 tests: silence, denial, contradiction, two comparable pairs, three closure edges, presumption pair, fiction pair, constraint plus consequence pair)
  • Suite tour: packs/examples/language-demo/unknown/README.md
  • Prerequisites: nb-01: First permit: facts, a rule and a question, nb-02: Why a missing fact is not a refusal, nb-06: When the register may stay silent; next: Stage 4 area D

Three levels:

  1. Northbridge use (this article): the clerk reads silence as NEITHER, denial as FALSE_ONLY, contradiction as BOTH; lets the complete file deny residence inside its bounds only; holds good standing by default, deems posted notices received, and prices unpaid issues through a rule next to the constraint — verified by the 17/17 suite and the quoted check OK above.
  2. Domain template: whenever a regime mixes unknowns with as-if tools, keep one mechanism per question — not_known reacts to silence, not requires denial, closures bound denial by predicate, domain and moment, presumptions name their exit, fictions have none, constraints report while rules conclude — and pin each with a comparable pair where only the studied record changes.
  3. Confirmed example elsewhere: the same four statuses, the same presumption shape (GoodStanding/unless), fiction (DeemedReceipt) and constraint (IssuedNeedsFee) run in packs/examples/language-demo/permits/ (28/28, see nb-05: Who counts as a suitable applicant); closures run in packs/examples/language-demo/register/; the condition table (not / not_known) is docs/language/08-cheat-sheet.law.md.
  4. Confirmed external formalization (corpus): state-task observance (Constitution of Türkiye, art. 65) — package tr.constitution, corpus/laws/tr/constitution/02-rights-general.law:123-131. A defeasible rule body holds when not_known(state_task_failure(polity, task)): the canonical case for not_known, where a state whose non-performance is not established counts as performing, with the carve-out carried by a negative producer (companion StateTaskBreached rule). Evidence: docs/research/constructs/07-negation-and-status/corpus-forms.en.md §1 (rated exemplary). Limit of verification: presence of the named construct at the cited lines only, confirmed by direct file read; no claim about deployment, runtime behaviour, or legal correctness.

Documentation for Arxo. Writings — blog.arxo.io.

Anonymous visit counts on stats.arxo.io, no cookies.