Skip to content
docs
Arxo ↗

Negation and truth statuses: pitfalls

For LLMs9 sections

Wrong forms, silent outcomes, LDC-E diagnostics, typical mistakes of formalizers and AI agents, and how to detect them.

1. when not p(x) without a negativity source — Not established, not refuted forever

Section titled “1. when not p(x) without a negativity source — Not established, not refuted forever”

The body needs Refuted, and there is nowhere to take it from: no then not p head, no negative fact, no closure. The formalizer’s most frequent mistake. The form is named — LDC-E4113, a warning: the predicate is declared in this package, its kind is neither empirical nor judgment, and the package holds not one negativity producer. Warning level, not rejection: the negativity may arrive as another package’s head or as an accepted refuting support, which statics does not read. Detection: ask who produces not p — a head, a fact, or a closure. If “not otherwise established” but there is no completeness holder — not_known(p(x)) is needed, not not p(x). Corpus debt — 81 places in 25 packages.

not_known(P) 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. The AI agent likes writing not_known “to make it work”, losing the difference between “checked, absent” and “not checked”.

LDC-E1307 on both check and lower. predicate, domain, snapshot, complete_as_of are mandatory; complete_as_of is a moment, not a date: @2026-03-01 is rejected under the same code; the domain is a predicate name, not a call. A domain of different arity is LDC-E2114, at runtime NON_EXECUTABLE_CLOSURE and Not established, not refuted.

4. derive_explicit_negative false — a closure without negatives

Section titled “4. derive_explicit_negative false — a closure without negatives”

The engine skips such a policy whole: p(x) for a domain member without a record stays Not established, not refuted, as without a closure. The form is lawful (the source is declared, there are no negations), but a reader expecting Refuted gets silence. Detection: read the flag next to closure, don’t assume it.

5. not (A and B) — negation only over an atom

Section titled “5. not (A and B) — negation only over an atom”

LDC-E1305: the not scope is one atom. The compiler applies no De Morgan, no excluded middle, no double-negation elimination. Write not A or not B or introduce a named predicate with a rule and negate it.

LDC-E4101: refuted(p(x)), established(p(x)), and bare negation do not bind variables. A positive literal binding the head variables must stand nearby. The same mistake in an unless clause: lowering makes a rule of its own of it, and the range-restriction requirement applies to it separately.

7. A cycle through not_known or a status test

Section titled “7. A cycle through not_known or a status test”

LDC-E4102 with a [default] or [status] edge: A if not_known B; B if not_known A is unstratifiable. A strict not_known(P) reader over a defeasible P producer is LDC-E4103 LATE_STATUS_PRODUCER: the reader must be defeasible.

A strict negative head against a positive fact gives Contradiction, and both readers — p(x) and not p(x) — stay silent. If the refusal must win, the conflict is resolved by priority between defeasible rules (see the priority page). Silent outcome: the case answers Not established, not refuted where the author expected the refusal to win.

9. Reserved statuses; not_known in the head

Section titled “9. Reserved statuses; not_known in the head”

opposed, conflicted, no_evidence are reserved past 0.2: 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.1. not_known in the head is warning LDC-E1302: the node is skipped, no rule reaches the compiled output.

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

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