RFD-0037 — AFT-grounded truth-value semantics — bilattice substrate, K3/FDE/Boolean lattice contexts, fail-closed projection, per-standpoint consistency policy

Question

What is the truth-value semantics under which Argon evaluates refinement membership, query results, rule bodies, and cross-standpoint federated queries? When does the inconsistent value both arise; when does it not; and how does the language guarantee that “K3 contexts cannot accidentally observe both” without losing the ability to express genuine cross-source disagreement?

Context

RFD-0016 ratified that refinement membership under OWA is three-valued (Kleene-Belnap), with success requiring true. The MetaValue (IS/CAN/NOT) implementation in meta-property-fixpoint realizes this directly. The Lean 4 mechanical proof at argon-formal/ (804 lines, zero sorrys) establishes flow-typing soundness over the K3 fragment.

Two pressures push beyond the original D-113 framing:

1. Standpoint federation. RFD-0034 and RFD-0035 commit to per-standpoint composition with cross-standpoint queries as a first-class operation. When a federated query aggregates results from multiple standpoints that genuinely disagree (e.g., federal-irs says T while state-ca-ftb says F), the K3 truth-value space has no value to record the disagreement — it can only collapse to unknown, losing the structural information that distinguishes “no source had evidence” (Belnap N) from “sources disagreed” (Belnap B).
2. Terminology rigor. The phrase “Kleene-Belnap three-valued” is informal: K3 (Kleene strong, 1952) is three-valued; Belnap-Dunn FDE (1977/1976) is four-valued. The literature converges on the synthesis that the natural restriction of Belnap’s logic to an OWA single-source setting is K3 — but the original RFD-0016 didn’t pin this down, leaving room for future inconsistency (e.g., RFD-0035 §12 originally claimed “four-valued Kleene-Belnap” before this RFD’s correction).

Approximation Fixpoint Theory (Denecker, Marek & Truszczynski 2000; refined 2004) is the published, peer-reviewed framework that subsumes K3, FDE, Boolean, and every CWA variant Argon could plausibly want — under one bilattice algebra. AFT has been proven to capture: logic programming with negation-as-failure, default logic, autoepistemic logic, abstract dialectical frameworks, hybrid MKNF (Liu & You 2019, the most direct match for our setting), active integrity constraints, distributed AEL, higher-order LP via weak bilattices, and fuzzy LP. Stratification across modules (Vennekens, Gilis & Denecker 2006) handles cross-standpoint composition by construction.

This RFD adopts AFT as Argon’s truth-value semantic foundation, ratifies the bilattice substrate, and specifies how the K3/FDE/Boolean lattice contexts emerge as type-level constraints over a single uniform storage layer.

Decision

Argon adopts a bilattice-parametric truth-value semantics grounded in Approximation Fixpoint Theory. Storage is the Belnap-Dunn FDE four-valued bilattice; observable values are determined by lattice context, a type-level constraint that restricts which Truth4 values an expression may carry. Three named contexts:

1. The Truth4 lattice (FDE)

The substrate is Truth4, the four-valued Belnap-Dunn bilattice:

Two orderings (Fitting 1991):

• Truth ordering ≤_t: not ≤_t (can | both) ≤_t is. can and both are incomparable in truth.
• Information ordering ≤_k: can ≤_k (is | not) ≤_k both. is and not are incomparable in information.

Four operations: truth meet ∧_t, truth join ∨_t, negation ¬, information meet ⊗ (consensus, drops disagreement to can), information join ⊕ (gullibility, accumulates conflict to both). The bilattice algebra is settled by Fitting 1991.

2. Lattice contexts as type-level constraints

Three named contexts restrict observable values:

Subtyping is information-precision: Boolean ⊑ K3 ⊑ FDE. The K3-context typecheck guarantees that both is statically unreachable — not silently hidden behind a default — because the consistent-pair constraint excludes (T, F) by construction.

3. K3 closure under the K3 operations

The K3 fragment is closed under {∧_t, ∨_t, ¬, ⊗} and not closed under ⊕. The escape witness is is ⊕ not = both — exactly the federation-across-disagreeing-sources case. This is the formal characterization of “K3 contexts can use the truth-side connectives and consensus, but federation/gullibility produces FDE.”

(Mechanical proof in ArgonFormal/Foundation/LatticeContext.lean: theorems truthMeet_inK3, truthJoin_inK3, neg_inK3, infoMeet_inK3, infoJoin_escapes_K3.)

4. K3 ↔ MetaValue isomorphism

The existing MetaValue (IS/CAN/NOT) is exactly the K3 fragment of Truth4. The bidirectional embedding MetaValue ↔ {v : Truth4 // v.inK3} is constructive and an information-ordering isomorphism. Every existing MetaValue theorem lifts to a K3-fragment Truth4 theorem; every Truth4 theorem on the K3 fragment specializes to a MetaValue theorem. The existing flow-typing soundness proof transfers verbatim.

(Mechanical proof: ArgonFormal/Foundation/LatticeContext.lean, ofMetaValue_infoLe_iff, ofMetaValue_toMetaValue, toMetaValue_ofMetaValue.)

5. World-assumption modes are AFT operators

Each per-standpoint world-assumption mode maps to a specific AFT approximator construction:

These are operator choices, not lattice choices. The lattice context (Boolean/K3/FDE) determines what’s observable; the AFT operator determines how knowledge propagates.

6. Per-standpoint stratified composition

Each standpoint declares its world-assumption operator. Cross-standpoint composition is stratified AFT (Vennekens-Gilis-Denecker 2006): when the standpoint dependency graph is a DAG, the global well-founded fixpoint computes standpoint-by-standpoint. Inflationarity of each per-standpoint operator implies inflationarity of the cross-standpoint fold; narrowings established at any earlier standpoint persist through the composition.

(Mechanical proof: ArgonFormal/Standpoint/Stratification.lean, theorems crossStandpointFold_inflationary, narrowing_preserved_across_standpoints, stratified_cross_standpoint_soundness.)

7. Cross-standpoint federation = AFT info-join

A federated query aggregates per-standpoint results via AFT information join (gullibility). The federated result reads:

The federation operator’s signature is Federate<FDE> — federated results live in the FDE context. K3 consumers must explicitly project (see §8).

(Mechanical proof: ArgonFormal/Standpoint/Federation.lean, theorems federate_eq_classify, federate_eq_both_iff, federate_inK3_of_agreement.)

8. Fail-closed projection FDE → K3 with explicit policy

When an FDE value flows into a K3-typed consumer, the user must specify a projection policy. The language does not silently collapse both to can. Four built-in policies:

The treatAsError projection succeeds iff the input is in the K3 fragment — this is the formal “fail-closed” property that the type system enforces on top of the policy decision.

(Mechanical proof: ArgonFormal/Foundation/Projection.lean, theorems project_inK3, project_treatAsError_iff, roundtrip_K3_FDE_K3.)

A future cut may add a syntax-level shorthand (analogous to Rust’s ?) for the most common policy, declared at the module level. The shorthand is purely additive and does not change the type rule; the projection remains visible at the source in some form.

9. Per-standpoint consistency policy

Each standpoint declares a ConsistencyPolicy controlling within-standpoint append-time behaviour:

Cross-standpoint disagreement is always preserved regardless of policy because it manifests at federation join time, not at within-standpoint append time. Different standpoints with different policies coexist in one workspace without cross-contamination.

(Mechanical proof: ArgonFormal/Standpoint/Consistency.lean, theorems append_strict_inK3, append_strict_fails_iff, strictFold_from_can_inK3.)

10. Refinement membership in K3 with Pietz-Rivieccio designation

Refinement membership under OWA defaults to the K3 lattice context with the Exactly True Logic designation (Pietz & Rivieccio 2013): only is is designated. can and both (the latter is statically unreachable in K3 contexts) both fail the membership check; the call site sees a refinement-violation diagnostic.

This is the rigorous restatement of D-113’s “success requires true, not ‘anything but false’” rule. Pietz-Rivieccio is the published anchor for the designation choice; Belnap (1977) supplies the philosophical motivation; Kleene (1952) supplies the value space and connective truth tables.

11. K3 vs Łukasiewicz Ł3 — K3 chosen

The two classical three-valued logics differ on the conditional: K3 maps U → U to U; Ł3 maps U → U to T. K3 is chosen because Ł3’s rule makes p → p a tautology even when p is unknown — silently passing checks the system cannot verify. K3’s pessimistic propagation is the fail-closed move that matches the rest of the design.

K3 truth tables (strong Kleene; the propagation rule for the Truth4 truth meet/join restricted to K3):

∧ | T  U  F        ∨ | T  U  F        ¬ |
T | T  U  F        T | T  T  T        T | F
U | U  U  F        U | T  U  U        U | U
F | F  F  F        F | T  U  F        F | T

The conditional is currently not a primitive in Argon’s refinement-body surface; if/when it lands, it inherits K3’s semantics by default.

12. CWA collapse soundness witness

D-113 states that under CWA modules, unknown collapses to false. The soundness of this collapse rests on a syntactic restriction: refinement bodies in the current implementation admit only meta-property predicates over a finite type graph (the Horn-restricted fragment per book/src/ch02-06-the-type-system.md:129). Reiter (1978)’s warning that CWA can introduce inconsistency in non-Horn theories does not bite because the refinement language is Horn. Lutz et al. 2013’s coNP-hardness result for closed-predicate DL-Lite is the formal warning: any future extension that admits non-Horn refinement bodies must re-argue soundness.

The Lean 4 proof at ArgonFormal/TypeSystem/Soundness/CwaOwa.lean covers the existing K3 case (cwa_narrowing_into_owa); the new framework’s per-standpoint policies preserve this property by construction (strict-policy K3 standpoints contain only K3-fragment cells; the existing soundness theorem applies).

13. Forward compatibility

The framework is naturally extensible without breaking the K3/FDE/Boolean contracts:

• Refined approximation spaces (Vanbesien et al. 2025) — beyond intervals; relevant if confidence-weighted reasoning lands.
• Non-deterministic AFT (Heyninck et al. 2022) — disjunctive extension; relevant for explicit choice-point reasoning.
• Higher-order LP via weak bilattices (Charalambidis et al. 2024) — for nested-rule contexts.
• Continuous truth-value lattices for soft constraints / probabilistic reasoning.

None of these require breaking the K3/FDE/Boolean lattice contexts; they add new contexts on top of the same AFT substrate.

14. Diagnostic codes introduced

Codes register in oxc-protocol::core::codes via the existing inventory::submit! registry.

15. CLI surface

This RFD does not introduce new top-level commands. The lattice-context type parameter shows up in:

• ox query NAME — defaults to --lattice K3. --lattice fde opts into federation behavior. --lattice boolean is the CWA-only path (Horn-restricted bodies only).
• ox query NAME across [s1, s2, ...] — federated query, returns FDE by default.
• ox check and ox test — typecheck the lattice-context constraints.
• ox doc and ox inspect — surface the lattice context of each declared query/mutation/rule.

Per-standpoint consistency policy is declared in the standpoint’s manifest entry (e.g., [standpoints.federal-irs] consistency = "strict").

Rationale

Three reasons AFT is the right substrate:

1. Convergent literature. AFT (Denecker, Marek, Truszczynski 2000; refined 2004) is the published peer-reviewed framework that subsumes every CWA variant Argon could plausibly want. The connections are well-traced in the literature: LP/NAF, default logic, AEL, MKNF+WFS, ADFs, AICs, fuzzy LP, distributed AEL — all are AFT instances. Stratification (Vennekens-Gilis-Denecker 2006) handles cross-standpoint composition by construction.

2. The “carry B as None when it can’t arise” intuition is literal. The AFT pair (x, y) with consistency constraint x ≤ y is exactly what the K3 lattice context enforces. The both value (T, F) is statically unreachable, not silently hidden. This is the cleanest possible realization of the design intuition: type-level capability restrictions on a uniform storage layer.

3. The per-context lattice = the right value space for the right job. Refinement membership wants K3 (success requires positive evidence; fail-closed). CWA modules want Boolean (Horn-restricted; can statically eliminable). Cross-standpoint federation wants FDE (both is meaningful; provenance witnesses source disagreement). Forcing one truth-value space everywhere either weakens the system (just K3, lose federation expressiveness) or burdens single-source contexts with a value they can’t produce (just FDE, type-pollution). Lattice-parametric is the right shape.

Why supersede RFD-0016 rather than amend. D-113 / RFD-0016’s decision — refinement membership under OWA is three-valued, success requires T — is unchanged. What changes is the framing: the rigorous published name (K3, motivated by Belnap’s question-answering argument), the Pietz-Rivieccio designation, the CWA-collapse soundness witness (Horn), the K3-vs-Ł3 conditional choice, and the placement of the K3 case as one fragment of the broader bilattice. This is more than a clarification edit. Per rfd/README.md’s lifecycle, supersession is the honest move when the new RFD names the prior position as a special case of a broader framework.

Why fail-closed projection. Argon follows Rust’s “simple, powerful rules, and a compiler that helps you” convention. Silent collapse from FDE to K3 (B → U with no syntactic mark) is exactly the silent-error-handling pattern Rust rejects via Result / ?. A K3 consumer of an FDE value must declare its policy; the call site is visible; reviewers can ask “should this be BothToUnknown or BothToError?” without remembering a global default. The ergonomic cost is one method call (or future shorthand operator) at the federation→K3 boundary, paid only by users who actually run federated queries.

Why per-standpoint consistency policy. The “Argon rejects invalid writes” instinct (Sharpe’s preferred mode) and the “persist source disagreement for repair” instinct (multi-source-KG mode) are both legitimate. Forcing one would either burden Sharpe with paraconsistent semantics it doesn’t want or prevent multi-source-KG users from declaring a paraconsistent standpoint. Per-standpoint declaration scopes the choice to the natural unit (the standpoint is the “single consistent perspective” by definition); cross-standpoint disagreement is preserved regardless of policy because it manifests at federation, not at append.

Why mechanical verification before commit. The new framework subsumes a settled RFD’s behaviour; getting that subsumption wrong is a class of bug that’s hard to catch by inspection. The Lean 4 proof at argon-formal/ (now extended by 1528 lines, zero sorrys, eight new theorems) pins the structural soundness — particularly that the K3 fragment is closed under the K3 operations, that strict-policy folds preserve K3, and that the new framework reproduces D-113’s K3 result exactly when restricted to single-standpoint strict-Horn settings. The proof IS the soundness witness; it’s not aspirational.

Consequences

• oxc-protocol::core::truth_value — new module carrying the typed Truth4 enum, lattice-context predicates (inK3, inBool, inFDE), ProjectionPolicy, ConsistencyPolicy, and the wire-shapes for federation results. Drift-gated through oxc-codegen.
• crates/nous — ExprResult (currently {Satisfied, NotSatisfied, Incomplete}) becomes a parametric EvalResult<T, L> where L : LatticeContext. The K3 case (L = K3) reduces to the existing three-valued shape; the FDE case adds Inconsistent { conflict_witness }. This is a structural change with codegen ripple.
• MetaValue — unchanged at the implementation level; positioned as the K3 fragment of the new Truth4. The Truth4.ofMetaValue embedding bridges the two without breaking any existing code path.
• Per-standpoint manifest — [standpoints.<name>] consistency = "strict" | "paraconsistent" is added to the standpoint declaration grammar. Default strict; existing standpoints inherit the default with no migration needed.
• Federation operator — new query primitive query NAME across [s1, s2, ...] returns EvalResult<T, FDE>. K3 consumers pipe through explicit .project(<policy>).
• Diagnostic codes — OE0610, OE0611, OE0612, OW0613 register in oxc-protocol::core::codes.
• RFD-0016 supersession — rfd/0016-refinement-under-owa-is-three-valued.md flips to state: superseded, with superseded_by: 0036. Body is preserved verbatim per the lifecycle rule.
• Book chapter sweep — ch02-06-the-type-system.md (refinement types), ch02-04-rules-and-reasoning.md (occurrence typing), ch05-01-metatype-calculus.md, ch05-02-defeasibility.md, ch05-04-standpoints-bitemporal.md, book/src/for-agents/glossary.md, appendix-c-diagnostics.md — update to cite RFD-0037 and the K3 / FDE / Boolean lattice-context terminology. Pin “K3” and “FDE” as glossary terms.
• AGENTS.md — argon/AGENTS.md:57 line on three-valued semantics tightens to “K3 (Kleene strong three-valued) refinement membership; cross-standpoint federation in FDE; see RFD-0037.”
• CHANGELOG entry — under the next argon release, document the framework adoption + the parametric EvalResult type.
• Diagnostic-message strings — oxc/src/diagnostics/codes.rs:579, 1369, oxc/src/diagnostics/rendering.rs:513, oxc/src/elaborate/validate.rs:974 — replace “Kleene-Belnap three-valued semantics” with “K3 (Kleene strong three-valued) semantics; see RFD-0037.” (Per RFD-0024’s anti-pattern rule against citing decision IDs in user-facing diagnostic strings, the RFD reference goes in the explain-text, not the message body.)
• Lean 4 proof obligation discharged. argon-formal/ extended by Truth4.lean, LatticeContext.lean, Projection.lean, StandpointStratification.lean, Federation.lean, Consistency.lean, BackwardCompat.lean. 1528 lines added, zero sorrys. The mechanical-proof reference goes into the new RFD plus the D-113 frontmatter.
• Forward-compatibility statement on file. Refined approximation spaces (Vanbesien 2025), non-deterministic AFT (Heyninck 2022), higher-order via weak bilattices (Charalambidis 2024), and continuous-confidence lattices all extend the framework additively. Not committed today; not closed off.
• RFD-0038 (discussion-shape) opened in parallel. Runtime capability advertisement — how OxbinRuntime::capabilities() (RFD-0035 §14) reports supported AFT operators per the framework above. Open questions, not commitments. Dedicated design session before drafting any answers.

Historical lineage

• Approximation Fixpoint Theory — Denecker, Marek, Truszczynski (2000). Approximations, Stable Operators, Well-Founded Fixpoints, and Applications in Nonmonotonic Reasoning. Refined in (2004) Ultimate Approximation. The substrate.
• Stratification of approximators — Vennekens, Gilis, Denecker (2006). Splitting an Operator: Algebraic Modularity Results for Logics with Fixpoint Semantics. The cross-standpoint composition tool.
• Hybrid MKNF as AFT approximator — Liu & You (2019). The bridge to OWA + rule-CWA hybrids. Argon’s per-standpoint world-assumption mode generalizes this.
• Bilattice algebra — Fitting (1991). Bilattices and the Semantics of Logic Programming. The two-orderings algebra Argon’s Truth4 realizes.
• Belnap-Dunn FDE four-valued logic — Belnap (1977) A Useful Four-Valued Logic; Dunn (1976) Intuitive Semantics for First-Degree Entailments and ‘Coupled Trees’. The FDE value space; motivation for needing N vs B distinction in multi-source settings.
• Kleene strong three-valued K3 — Kleene (1952) Introduction to Metamathematics §64. The K3 fragment Argon uses for refinement membership and per-standpoint queries.
• Exactly True Logic / “only T designated” — Pietz & Rivieccio (2013) Nothing but the Truth. The rigorous published anchor for the fail-closed designation.
• CWA / NAF foundations — Reiter (1978) On Closed World Data Bases; Clark (1978) Negation as Failure. The classical CWA framework, captured by AFT’s stratified-negation operator.
• LCWA — Denecker et al. (2010). The parameterized-window CWA generalization, captured as an AFT instance.
• Closed predicates in DL-Lite — Lutz et al. (2013). The forward-compatibility warning: non-Horn extensions to refinement bodies require re-argument.
• Forward-compatibility extensions — Vanbesien et al. (2025) refined approximation spaces; Heyninck et al. (2022) non-deterministic AFT; Charalambidis et al. (2024) higher-order via weak bilattices.

The K3-as-restriction-of-FDE synthesis is not invented here — it’s the consensus reading the literature converges on (Fitting 1991 and Belnap 1977 are the canonical statements; the relationship is flagged explicitly across the survey literature). Argon’s contribution is the design realization: making the lattice-context constraint a first-class type-level discipline, with explicit fail-closed projection and per-standpoint consistency policy as the architectural surfaces.

The mechanical Lean 4 proof at argon-formal/ is the soundness witness. Eight new theorems extend the existing 804-line proof by 1528 lines with zero sorrys. The proof is the literal verification that this RFD’s commitments are internally consistent and that the new framework reproduces RFD-0016’s K3 case exactly under the stated restriction.

D-113 (the prior decision identifier) remains the historical anchor; its body is preserved verbatim. The new RFD is its formalization, not its replacement.