Skip to content
docs
Arxo ↗

Presumptions and rebuttal

For LLMs11 sections

On the last page the archive recognised a letter as received by fiction: the act said “counts” — and there was nothing to object with. More often a norm adds: “counts as received unless proven otherwise”. That is a presumption — a conclusion that stands by itself until someone establishes the named rebuttal. The corpus holds 236 presumptions in 47 packages (measured 05.09.2026); 197 of their provisos derive the opposite, 51 only remove the conclusion, and the difference between these two forms is the page’s main lesson.

Legally a presumption does not establish a fact but allocates the burden: nobody saw the receipt, yet it is clear who must prove what to change the conclusion. A rebuttal is an established fact, not silence. “The service did not confirm delivery” and “the service reported non-delivery” are different things, and only the second changes anything.

The archive sends a researcher a notice to return a document at the registry address. Next: what counts as received, who rebuts it with what, and what follows from a received notice.

Arxo Law
language "law.core" version "0.2";
package tutorial.archive version "0.10.0";
namespace "urn:law:tutorial:archive";
entity Person;
relation return_notice_sent_to_registered_address(p: Person) kind empirical;
relation delivery_failure_reported(p: Person) kind empirical;
relation non_residence_proven(p: Person) kind empirical;
relation address_change_unreported(p: Person) kind empirical;
relation return_notice_received(p: Person) kind institutional;
relation non_return_recorded(p: Person) kind empirical;
relation extension_granted(p: Person) kind institutional;
relation borrowing_suspended(p: Person) kind institutional;

A notice sent to the registry address counts as received. The reader may prove she did not reside at that address — then the notice was not received. But if she herself did not tell the archive about the address change, the risk of non-receipt lies with her, and the notice counts as received again. And a delivery-service report of non-delivery removes the presumption while asserting nothing in return.

Arxo Law
presumption ReturnNoticeReceipt {
for p: Person;
when return_notice_sent_to_registered_address(p);
presume return_notice_received(p);
unless non_residence_proven(p) then not return_notice_received(p);
unless return_notice_sent_to_registered_address(p) and address_change_unreported(p) then return_notice_received(p);
unless delivery_failure_reported(p);
}

presume is the presumed head, when the premise, unless the provisos in two forms: with then and without. There is no new mechanism behind the word presumption: it is sugar over rules and priorities, and the compiler shows the expansion via its expand command. Here it is compressed to names, strength, and head:

Output
$ lawc expand 12-presumptions.law.md --symbol ReturnNoticeReceipt
presumption ReturnNoticeReceipt (12-presumptions.law.md:7:24)
порождено узлов CLIR: 6
rule …#ReturnNoticeReceipt/R1 defeasible return_notice_received(p)
rule …#ReturnNoticeReceipt/R2 defeasible not return_notice_received(p)
rule …#ReturnNoticeReceipt/R3 defeasible return_notice_received(p)
priority_rule …#ReturnNoticeReceipt/R3/priority/0 R3 над R2
rule …#ReturnNoticeReceipt/R4 defeater return_notice_received(p)
priority_rule …#ReturnNoticeReceipt/priority R2 над R1

The command names the page file; on this page run it with the .en.law.md filename (the “CLIR nodes produced” line counts the generated nodes, “over” marks the priority direction).

The premise became the defeasible rule R1. The proviso with then not is the defeasible rule R2 with the opposite head and a direct priority over R1. The proviso with then but no not is rule R3 with priority over the previous link, R2. The bare proviso is the defeater R4, with priority over nothing: it removes support rather than arguing with it. All these are the tools of the defeat tutorial; a presumption merely assembles them into a form matching the act’s vocabulary.

Factsreturn_notice_received
notice sentTRUE_ONLY

The test from this page, byte for byte:

Arxo Law
test "уведомление направлено по адресу из реестра — считается полученным" {
given {
context {
decision_time @2026-04-01T09:00:00+05:00;
knowledge_time @2026-04-01T09:00:00+05:00;
legal_time @2026-04-01;
timezone "Asia/Almaty";
}
assert return_notice_sent_to_registered_address(entity_ref("urn:tutorial:ivanova")) {
id "assert-sent";
origin case_input;
}
}
evaluate truth(return_notice_received(entity_ref("urn:tutorial:ivanova")));
expect truth_status == TRUE_ONLY;
expect evaluation_status == COMPUTED;
}

The test name reads: “A notice sent to the registry address counts as received.”

TRUE_ONLY here is the support of a defeasible rule, not an established fact. The difference shows not in the answer but in what can be done with it: a strict support is defeated by nobody, while any of the three provisos removes the presumptive one. The compiler rejects a strict rule reading a presumed head (LDC-E4103): presumption consumers are written defeasible.

Two provisos, two different answers.

Factsreturn_notice_received
sent, service reported non-deliveryNEITHER
sent, non-residence at the address provenFALSE_ONLY

The non-delivery report is the bare proviso, the R4 defeater. It removes the support of R1 but does not prove non-receipt: the answer is NEITHER, and the archive must look into it, not count. Proven non-residence is the proviso with then not: rule R2 derives the opposite, the R2-over-R1 priority settles the dispute, the answer is FALSE_ONLY, and the archive must proceed on the notice not being received.

The choice of form is the act author’s legal decision, not a stylistic one. The question is the same as when choosing between a defeater and a priority: must the authority proceed from the opposite — or must it look into it? Writing then not where the act merely removes the presumption attributes to the act a conclusion it lacks; writing a bare proviso where the act rebuts leaves the case at NEITHER when the answer already exists.

Factsreturn_notice_received
sent, non-residence proven, address change unreportedTRUE_ONLY

The reader proved she did not reside at the address — but herself failed to tell the archive about the move. The third proviso returns the conclusion: R3 prevails over R2, and the notice counts as received. This is the proviso chain: each proviso with then takes priority over the previous link, not over the presumption at large. The record order is the chain order.

Hence the produced contrary rule is defeasible, not strict. Were R2 strict, no priority could beat it, and an exception to the exception would make no sense. An author needing a truly irrebuttable “not received” writes a separate strict rule with a not head — and then it is no longer a presumption proviso.

The second proviso repeats the presumption premise: return_notice_sent_to_registered_address(p) and address_change_unreported(p). The repetition is no accident. A produced rule’s body is the proviso’s own condition; the when premise is not carried into it. The natural reading of the norm says the opposite — “since this is an exception to the presumption, its conditions are already present” — which is exactly why the rule is written out explicitly in the specification.

Factsreturn_notice_received
nothing sent, address change unreportedNEITHER
nothing sent, non-residence provenFALSE_ONLY

Remove the premise repetition and the first row becomes TRUE_ONLY: a reader who did not report her address would “receive” a notice nobody sent. With the repetition cut out the answer becomes exactly this: the lesson of the spare conclusion holds just like the lesson of the needed one.

The second row shows the first proviso’s premise is deliberately not repeated: proven non-residence yields “not received” even without a notice, and that is correct — an unsent notice was not received. The rule is simple: look at each proviso as a separate norm with its own body, and ask what it will derive when the presumption premise is not established.

Factsreturn_notice_received
sent, non-delivery, non-residence provenFALSE_ONLY
sent, non-delivery, address change unreportedNEITHER

The R4 defeater removes support from any defeasible rule with the same head and no declared priority over it: from both R1 and R3. In the second row the exception to the exception fired — and was removed by the non-delivery report, because a bare proviso is no chain link and knows no priorities. In the first row the report did not touch R2: it has a different head.

Hence the record rule: a bare proviso goes last. Put it first and the next proviso with then not takes priority over the defeater rather than over the presumption; with proven non-residence the answer becomes BOTH. The compiler accepts such an order silently: the proviso chain is acyclic, and only the author knows it linked the wrong links. If blocking must yield to the exception to the exception, it is written as a separate defeater with a priority declared over it by an ordinary priority declaration.

A received notice is no end in itself: if the document was still not returned after it, home issue is suspended — except when the term was extended.

Arxo Law
rule SuspensionAfterNotice defeasible {
for p: Person;
when return_notice_received(p) and non_return_recorded(p);
then borrowing_suspended(p);
unless extension_granted(p);
}
Facts beyond the sent noticeborrowing_suspended
non-return recordedTRUE_ONLY
non-return recorded, service reported non-deliveryNEITHER
non-return recorded, non-residence provenNEITHER
non-return recorded, term extendedNEITHER

A bare premise reads as established: a removed presumption and a refuted one alike leave the norm without support. Non-return here is a control record, not silence about return, as in the duty tutorial. And unless on an ordinary rule is the same machine: SuspensionAfterNotice/unless/0 is a defeater against borrowing_suspended.

Article 912 of the Civil Code of Kazakhstan: one who announced a reward may withdraw the promise, except in three cases — the announcement provided withdrawal is barred, a term for action was given, someone already performed the action. In the corpus the three bars are three strict rules with one head withdrawal_barred, and the right to withdraw is a presumption with a then not proviso. Here one of the three rules and the presumption itself, as they stand in the public-reward package.

Arxo Law
entity Announcement;
relation public_reward_announced(announcement: Announcement, promisor: Person) kind institutional;
relation responder_already_performed_before_withdrawal(announcement: Announcement, person: Person) kind empirical;
relation withdrawal_barred(announcement: Announcement) kind institutional;
relation promisor_may_withdraw_the_promise(announcement: Announcement, person: Person) kind institutional;
rule PerformanceBeforeWithdrawalBarsIt strict {
for announcement: Announcement;
for responder: Person;
when responder_already_performed_before_withdrawal(announcement, responder);
then withdrawal_barred(announcement);
}
presumption PromisorMayWithdrawUnlessOneOfTheThreeBarsApplies {
for announcement: Announcement;
for promisor: Person;
when public_reward_announced(announcement, promisor);
presume promisor_may_withdraw_the_promise(announcement, promisor);
unless public_reward_announced(announcement, promisor)
and withdrawal_barred(announcement)
then not promisor_may_withdraw_the_promise(announcement, promisor);
}

The archive director publicly promised a reward for returning a lost file; Ivanova returned it.

Factspromisor_may_withdraw_the_promise
reward announcedTRUE_ONLY
announced, Ivanova performed the action before withdrawalFALSE_ONLY

The proviso repeats public_reward_announced(announcement, promisor) for the same reason: the R2 head names the promisor, while withdrawal_barred knows only the announcement. Remove the repetition and promisor in the head stays unbound.

A presumption has a second record form — the rebuttable_presumption definition from the expansion library (reasoning-scheme catalogue R01). An instance names cases by name and tells the two rebuttal contracts apart explicitly:

Output
expand rebuttable_presumption ReturnNoticeReceipt {
label ru-KZ unofficial "Уведомление, направленное по адресу из реестра, считается полученным";
bind subject = p: Person;
conditions = [return_notice_sent_to_registered_address];
presumed = return_notice_received;
case blocked DeliveryFailure {
label ru-KZ unofficial "Служба доставки сообщила о невручении";
premises = [delivery_failure_reported];
}
case contrary NonResidence {
label ru-KZ unofficial "Читатель доказал, что не проживал по адресу";
premises = [non_residence_proven];
}
}

The labels read: “A notice sent to the registry address counts as received”; “The delivery service reported non-delivery”; “The reader proved non-residence at the address”.

blocked is a defeater, contrary a contrary rule with priority over the presumption; the CLIR nodes are byte-equal to the hand record, only the case names are structural (…/blocked/DeliveryFailure), not ordinal. What the profile does not do: proviso chains — cases are independent, and an exception to an exception is written alongside as an ordinary rule with priority. What it gives in return: a label on each case and no way to mix up the proviso order.

On this page the block is shown as text because expansion is a package dependency: the definition is connected in law.toml under [expansions] and pinned in law.lock, while a literate page has no manifest. Put expand in a package without a manifest and the compiler refuses:

Output
error LDC-E1336: expand ReturnNoticeReceipt: определение
"rebuttable_presumption" не разрешается (§279.1.3)

The diagnostic reads: ‘definition “rebuttable_presumption” does not resolve’.

A proviso that failed to bind the head variable. Remove the article-912 presumption’s public_reward_announced repetition and the produced rule gets a head with an unbound promisor:

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

The diagnostic reads: ‘…head uses unbound variables [promisor] — the rule is not range-restricted: a variable must be bound by a positive established conjunct of a finite source’.

The diagnostic is named after the produced node, …/R2, not after the presumption: an expansion is rejected exactly where a hand-written defeater with the same body would have been rejected.

A proviso on a strict rule. Make SuspensionAfterNotice strict, keeping unless:

Output
error LDC-E4110: SuspensionAfterNotice: `unless` на strict-правиле (§149) —
сделайте правило defeasible либо внесите условие применимости в strict-тело

The diagnostic reads: “‘SuspensionAfterNotice’: unless on a strict rule — make the rule defeasible or move the applicability condition into the strict body”.

The same mutation yields a second refusal, LDC-E4103: the now-strict rule reads return_notice_received, produced by the defeasible R1. A presumption consumer cannot be strict for both reasons at once.

Both refusals belong to the language. Exceptions are written with unless. The compiler rejects an unknown presumption-body item with LDC-E0201 rather than silently skipping it.

Presumption, defeater, and priority exhaust what the core can say about norm against norm. The next page returns to the source: the pinned edition — how to place an article’s bytes next to the package and verify a fragment twice, by address and by content.

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

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

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