RFD 0010 — Negative facts / strong negation

• State: discussion
• Opened: 2026-05-29
• Decides: surface syntax for asserting a fact’s negation as ground truth (distinct from absence-as-unknown under OWA, and distinct from default negation-as-failure in rule bodies); the wire-format mirror; how this composes with the standpoint federation runtime to make Truth4::Both operationally reachable.

Question

Today a pub standpoint X { pub fact Person(alice); } lets standpoint X assert alice ∈ Person as positive ground truth. The federation runtime’s query_dispatch then evaluates this row as Truth4::Is from X and Truth4::Can (implicit absence) from any other contributing standpoint. The AFT info-join Is ⊕ Can = Is, so the row surfaces tagged Is.

There is no current way for a standpoint to assert alice ∉ Person as positive ground truth. This means:

• The bilattice value Truth4::Not (Belnap-Dunn’s F, AFT’s (F, F) pair) is never produced from a fact-derived per-source classification.
• The bilattice value Truth4::Both (Belnap’s B, AFT’s inconsistent (T, F)) is consequently never produced by federate, because Is ⊕ Can ⊕ Can ⊕ ... = Is regardless of contributor count.
• The federation runtime is operationally category-(b) bilattice-traced in the vault’s Bilattice-Native Query Evaluation taxonomy, not the category-(c) bilattice-native outcome the substrate’s proven theorems (federate_eq_both_iff, aft_discharges_T3_obstruction) advertise.

The decision: introduce a surface form for strong negation of facts, lower it to a new wire-format IofRefutation axiom kind, and have the per-standpoint materializer compute Truth4 values per (tuple, source) pair so that the runtime is operationally bilattice-native.

Context

What’s deferred from RFD 0004

RFD 0004 §Future Work explicitly anticipated this work:

Negative facts / classical negation — pub not_fact Person(alice) to assert that alice is not a Person. Useful in OWA / classical contexts; relates to §12.2’s Truth4 bilattice. Defer; orthogonal to this RFD’s positive-only scope.

That deferral is now load-bearing: it gates the operational reachability of the bilattice’s most distinctive value.

The two negations distinction (Gelfond-Lifschitz 1991)

Gelfond and Lifschitz (1991) draw the canonical line between two negations every paraconsistent logic-programming surface must distinguish:

Argon already uses not in rule bodies (NAF, stratified). What it lacks is the declaration-level strong negation. The two are independent: NAF is a reasoning-time operator inferring absence from the current extent; strong negation is a build-time ground-truth assertion of refutation.

What the substrate already supplies

The Lean substrate is fully ready for this:

• Argon.Foundation.Truth4 has the four-valued carrier with all algebraic laws.
• Argon.Foundation.Bilattice.infoJoin is proven associative, commutative, idempotent.
• Argon.Standpoint.Federation.federate is the AFT info-join over List Truth4.
• federate_eq_classify characterizes federate outputs structurally.
• federate_eq_both_iff: federate xs = .both ↔ hasBoth xs ∨ (hasIs xs ∧ hasNot xs) — the precise theorem stating when Both arises.
• aft_discharges_T3_obstruction: sheafClassify contribs = .obstructed ↔ federate contribs = .both.

None of this is reachable by the runtime today because no source ever contributes .not. The Lean theorems are sound but the runtime cannot exhibit the case they characterize.

What the wire format already supplies

AxiomEvent.standpoint_id (set by the standpoint-block elaborator in commit 2776be9) tags each event with its asserting source. The materializer in commit 9aa8c73 (materialize_predicates_for_standpoint) filters per source. The dispatcher in the same commit feeds per-source classifications to query_derive_federated. The shape is right; only the negative half is missing.

The Polarity field is not a negation field

AxiomEvent.op: Polarity ∈ {Assert, Retract} is the time-evolution polarity (asserting vs withdrawing a previous claim under bitemporal extent). It is not the ontological polarity (P(x) vs ¬P(x)). Conflating them would break RP-004’s bitemporal contract. The right move is a new axiom kind for ontological refutation, orthogonal to op.

Decision

Surface (1) — declaration-level strong negation

pub not_fact Person(alice);
pub not_fact Adult(bob);
pub not_fact employed_by(alice, AcmeCorp);

Symmetric to pub fact P(x); syntactically. Lowers to a new wire event variant. Permitted at file level and inside pub standpoint X { ... } blocks; in the latter case the refutation is stamped with X.standpoint_id like positive facts (commit 2776be9’s mechanism applies uniformly).

Wire format (2) — new axiom kind IofRefutation

#![allow(unused)]
fn main() {
pub enum AxiomKind {
    ...,
    IofAssertion,
    IofRefutation,  // NEW
    ...
}
}

Body shape mirrors IofAssertionBody exactly (concept_id + individual_id). The semantic difference is carried in the variant tag, not in body fields. Encoding/decoding follow the same pattern as IofAssertion.

Symmetrically, a relation-tuple refutation lands as RelationTupleRefutation parallel to RelationTuple for the N-ary case. Same body shape; same variant-tag carries the polarity.

Lean drift (3)

Argon.Storage.AxiomKind gains iofRefutation and relationTupleRefutation constructors with @[language_interface] carried. The Lean side reads only the algebraic content; the bilattice/federation machinery is unchanged because it already handles Truth4.not symmetrically.

Materializer (4)

Store::materialize_predicates_for_standpoint is extended:

• Maintain TWO per-source extents: positive: RelationCatalog and negative: RelationCatalog.
• IofAssertion events stamp positive; IofRefutation events stamp negative.
• Symmetric handling for RelationTuple / RelationTupleRefutation.

The output is PerSourceExtents { positive, negative } rather than a single RelationCatalog.

Dispatcher (5)

Store::query_dispatch for federated queries classifies each (relation, tuple) pair via the cross-product of per-source extents:

for each source S:
    in_pos = tuple ∈ positive[S].entry(rel)
    in_neg = tuple ∈ negative[S].entry(rel)
    truth4_S(tuple) =
        match (in_pos, in_neg) {
            (true,  false) => Is,
            (false, true ) => Not,
            (true,  true ) => Both,   // S already contradicts itself
            (false, false) => Can,    // S has no evidence
        }

The full row classification feeds query_derive_federated exactly as before; the AFT info-join over per-source Truth4 values yields the final row tag.

For derived (rule-output) relations, rule evaluation runs against the positive catalog per source as before; Truth4::Not contribution only arises when the rule’s head is one a refutation event positively names — which is unusual for rule heads but legal. Per-source Truth4::Both from a single source is the contradiction-with-self case (pub fact P(a); pub not_fact P(a); inside the same standpoint block) — useful as an internal consistency check; federation then surfaces it as Both.

Soundness

The implementation is the operational discharge of federate_eq_both_iff:

• A federated row surfaces Truth4::Both ⟺ some source’s per-tuple Truth4 is Both, OR some source contributes Is and another contributes Not.
• This is exactly the Lean theorem.

aft_discharges_T3_obstruction then lifts: sheafClassify of the federated row’s contribution list is obstructed ⟺ row tag is Both. The runtime now exhibits the contextuality-detection case the proven theorem characterizes.

Diagnostics

• OE0640 NegativeFactArityMismatch — pub not_fact P(x, y) where P has arity 1 (parallels positive-side checks in RFD 0004).
• OE0641 NegativeFactUndeclaredPredicate — pub not_fact P(x) where P is not a declared concept or relation.
• Stratified-NAF / strong-negation interaction inside rule bodies is out of scope for this RFD: rule bodies admit only not (NAF). A future RFD may add ~ (strong negation) as a body atom, but that work composes cleanly only after IofRefutation exists at the wire level.

Rationale

Why this and not just NAF

NAF is reasoning-time and absent from the wire format. It already exists. The bilattice value Truth4::Not represents positive evidence of refutation — distinct from NAF’s “no positive evidence”. Without strong negation, a standpoint cannot DISTINGUISH “I don’t know whether P(alice) holds” from “I know P(alice) does NOT hold”. These are different epistemic states and the bilattice is designed to track exactly that distinction.

Why a new AxiomKind, not an extension of IofAssertion

Three reasons:

1. Clean Lean drift. @[language_interface] checks variant alignment. Adding a body field forces every existing consumer to handle a new field; adding a sibling variant only forces consumers of the new variant to handle it. RP-004 chose the second pattern (IofAssertion, RelationTuple, PropertyAssertion are all sibling variants), maintaining symmetry.
2. Storage efficiency. A standpoint with mostly positive facts wastes a byte per event encoding polarity: false. A separate kind allows the encoder to omit the discriminator in the common case.
3. Diagnostic and tool surface. axiom-events queries that want all refutations for a standpoint scan by kind == IofRefutation directly. A polarity-field design forces every consumer to decode-and-test.

Why declaration-level, not rule-body

The conflation of strong negation and NAF in rule bodies is a known source of confusion in logic-programming languages (Gelfond-Lifschitz 1991 §1: “the two negations are often conflated in practice, leading to subtle bugs”). Argon’s design discipline is to surface them as distinct categories: NAF as a rule-body operator on the extent at evaluation time, strong negation as a declaration form that ships through the wire format. This RFD keeps to that discipline.

Why now, not as part of RFD 0004

RFD 0004 was scoped to positive ground-truth facts. The federation runtime didn’t exist then; the gap was theoretical. With federation operationally complete (commits 14–16 + standpoint scoping + dispatcher), the gap is now load-bearing: it gates the headline competitive claim (vault: bilattice-native runtime, category C, “production-scale systems do not”). RFD 0004’s deferral was correct then; closing it is correct now.

Why the standpoint federation is the right host for this

The bilattice’s most distinctive value (Both) is a cross-source notion: it requires two sources contributing opposite verdicts on the same proposition. Single-source Both arises only from a source contradicting itself (legal but unusual). Federation is the natural host because federation is where cross-source disagreement is computed. Implementing strong negation as a fact-declaration form makes it composable with the federation runtime already wired.

Alternatives

A1: pub fact !Person(alice);

Reuse pub fact with a ! prefix on the head atom. Closer to logic-programming notation. Rejected: harder to grep, conflates positive/negative in the same surface form, makes the elaborator’s per-form dispatch fuzzier, and reads worse in error messages.

A2: pub fact not Person(alice);

not keyword inline. Rejected: collides with the existing rule-body NAF not, the exact conflation Gelfond-Lifschitz warned against. Different surfaces for different semantics is a feature.

A3: Extend IofAssertion with a polarity: bool body field

Single AxiomKind, body carries polarity. Rejected per §Rationale above (Lean drift symmetry, storage efficiency, tool surface).

A4: Defer until rule-body strong negation is also designed

Bundle both surfaces into a single RFD. Rejected: declaration-level refutation is a complete, independently-useful feature — every modeler can write pub not_fact P(x); and benefit immediately; rule-body strong negation requires non-trivial stratification work (~ P(x) interacts with NAF and defeasible rules in subtle ways and probably needs an answer-set-style semantics). Shipping declaration-level first lets us learn from usage before designing the rule-body half.

Consequences

What modelers gain

pub standpoint internal_audit {
    pub fact employed_by(alice, AcmeCorp);
}

pub standpoint public_record {
    pub not_fact employed_by(alice, AcmeCorp);
}

pub query employment() -> employed_by
    across [internal_audit, public_record];

The query returns (alice, AcmeCorp) tagged Truth4::Both — explicit, runtime-visible, modeler-actionable evidence of cross-source disagreement. Under #[federate(strict)] this surfaces as OE1302 FederationDisagreement (other agent’s renumbering); under default paraconsistent the row surfaces with the Both tag intact.

This is the operational moat Argon claims and nobody else delivers (per the vault note).

What changes for existing code

Nothing breaks. Every existing source compiles unchanged because pub not_fact is a new declaration form parsed by a new branch; existing pub fact lowering is untouched; existing federation queries return identical results when no source uses not_fact (because no Truth4::Not enters the contribution list, so the info-join behaves identically).

What this opens up

• Rule-body strong negation (future RFD): ~ P(x) in rule bodies, with answer-set-style or AFT-stable-pair semantics.
• Refutation rules (future RFD): derive ~ Adult(p) :- Adolescent(p) — deriving negative extents from rules, not just facts.
• Per-relation closure declarations (future RFD): a relation explicitly marked CWA could auto-emit IofRefutation for every tuple not asserted, making CWA reasoning composable with federation.

Open questions

1. Wire-format symmetry with Retract. Should Retract of an IofAssertion event subsequently restate the proposition’s status as Can (no positive evidence; no negative evidence) or as Not (positively refuted)? Retract clearly leans toward Can; the semantic gap with IofRefutation is then preserved. The implementation should treat them distinctly.

2. What happens when a single standpoint asserts both pub fact P(a); and pub not_fact P(a);? Per the dispatcher design above, the per-source Truth4 becomes Both directly; federation then surfaces Both. Should this also be a build-time error (single-source consistency check), or only a runtime tag? RFD position: lower without error; the bilattice tag IS the diagnostic. A separate #[strict_internal] per-standpoint attribute could opt into build-time rejection in a future RFD.

3. Diagnostic emission scope. Should OE0640/OE0641 ALSO be emitted at federation-query time when sources disagree even under #[federate(strict)]? No — the strict-policy case is already covered by OE1302 FederationDisagreement (other agent’s renumbering). OE0640/OE0641 are build-time arity/declared-predicate checks; they don’t need a runtime counterpart.

References

• RFD 0004 §Future Work — “Negative facts / classical negation”
• RFD 0007 — Missing-value semantics (the related distinction between three field intents)
• RFD 0008 — Standpoint-Sheaf Equivalence Proof Roadmap (Path A discharge)
• Argon.Foundation.Truth4 — bilattice carrier with .not constructor
• Argon.Standpoint.Federation.federate_eq_both_iff — proven theorem this RFD makes runtime-observable
• Argon.Standpoint.AFTEquivalence.aft_discharges_T3_obstruction — sheaf-equivalence discharge
• Gelfond, M. & Lifschitz, V. (1991). Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing.
• Belnap, N. D. (1977). A useful four-valued logic.
• Vault: Bilattice-Native Query Evaluation — operationality levels (a/b/c)
• Vault: AFT-Grounded Truth Value Semantics for Argon — the AFT pair correspondence