RFD-0016 — Refinement under OWA is three-valued (Kleene-Belnap)

Superseded. RFD-0037 supersedes this RFD by formalizing it as the K3 special case of an AFT-grounded bilattice framework. The decision of this RFD — that refinement membership under OWA is three-valued, success requires true — is preserved verbatim and proven mechanically in ArgonFormal/Standpoint/BackwardCompat.lean. The new RFD adds: rigorous K3 / FDE / Boolean lattice contexts, Pietz-Rivieccio Exactly True designation, fail-closed FDE→K3 projection with explicit policies, per-standpoint consistency policy, cross-standpoint federation via AFT info-join, and the K3-vs-Ł3 conditional choice. Read RFD-0037 for the current commitment; this RFD is preserved for historical record.

Question

When a module operates under the Open World Assumption (OWA), refinement-type membership checks have a third possible answer: not true, not false, but unknown (the system has insufficient information). How does the language treat unknown results in refinement contexts?

Decision

Refinement membership under OWA is three-valued (Kleene-Belnap). The three values are true, false, and unknown. Membership succeeds only on true. unknown does not satisfy the refinement; the call site sees a refinement-violation diagnostic, not a refinement-pass.

Under CWA (Closed World Assumption), unknown collapses to false. A CWA-mode module’s refinement check returns true or false only.

A module’s world assumption is part of its declaration; refinement contexts inherit the surrounding module’s mode.

Rationale

Three values match the underlying semantics. OWA is the assumption that absence of evidence is not evidence of absence. A refinement check that doesn’t know the answer can’t conclude false; it has to admit unknown. Forcing two-valued logic under OWA would have either silently treated unknown as true (unsafe; admits unverified facts) or silently as false (over-restrictive; rejects valid facts that just weren’t proven yet).

Success requires true, not “anything but false.” The unknown value represents “we don’t have enough information.” A refinement-typed value carrying unknown membership is one whose claim hasn’t been verified. The refinement should not pretend it has been verified; it should fail closed and let the author decide whether to add evidence or relax the refinement.

CWA collapse is automatic. When a module declares CWA, the standard interpretation is “facts not asserted are false.” unknown is meaningless in that mode; collapsing to false matches the modal commitment. This means CWA modules can use refinement membership as classical two-valued logic without writing out the collapse.

Consequences

• Refinement membership returns a Kleene-Belnap value. Type checking treats unknown as a violation.
• Diagnostic codes distinguish “definitely violates” (OE0606 MetaxisRefinementViolation) from “cannot verify” (an OW0 warning when a CWA-style audit would have admitted, but OWA cannot).
• Patterns that build on refinement (membership-conditioned narrowing, cardinality assertions) inherit the three-valuedness.
• Module declarations carry world-assumption metadata (world: open / world: closed); refinement evaluation reads that metadata.