Worlds

The closed world

A world assumption decides what the absence of a fact means. Under the closed-world assumption an absent fact is false: if a membership is not derivable, it does not hold. Under the open-world assumption an absent fact is unknown: absence is the lack of evidence, not its denial. The reference fixes both under world assumptions.

Argon is closed-world by default. A program is a data system whose extents are the authority for what is true, and closed-world is the regime that makes “not in the extent” mean “false” rather than “not yet known”. With Alice’s hours unrecorded, “is Alice a FullTime?” is not — she is not a full-timer until her hours say so. A package may set its default_world in the manifest, but every concept without an explicit mark inherits the closed default.

A concept whose knowledge is incomplete by nature opts out, one concept at a time, with #[world(open)]:

#[world(open)]
pub type LegalAgent { mut name: String }

The attribute is executed, not decorative. The elaborator reads the policy word — open or closed, any other word a loud refusal — records the concept’s world on a per-concept map keyed by its qualified path, and the reasoner stamps that map onto every evaluation. Each negated membership atom is then read under its own concept’s world. The attribute is concept-only; placing it elsewhere is rejected.

World-honest negation

Negation-as-failure is the closed-world inference: not P succeeds when P is not derivable. Under an open-world concept that inference is unsound — an absent P(x) is unknown, not a definite not, so reading the absence as false would assert more than the evidence supports.

Argon refuses to draw the unsound conclusion rather than draw it silently. A closed-world not H whose derivation depends on an open-world concept’s negation does not get to read that unknown as false; the substrate refuses the shape at ox check and ox build with OE1367. The fix is stated in the diagnostic: mark H’s concept open-world too, so not H tolerates the unknown, or restructure so the open-world negation never flows into a closed-world-negated head. The default stays closed-world for every concept without the mark. R(args) is unknown reads only R’s completed well-founded-undefined rows; it does not enumerate ordinary open-world absence. A recursive read before R completes refuses with OE1441. This is world-honest negation-as-failure: the engine honors each concept’s mark instead of evaluating closed-world unconditionally.

The same honesty reaches the test surface. assert derivable F(x) and assert not derivable F(x) read F’s world directly. A present row is a definite pass or fail; an absent row under the closed world is definite non-derivability; an absent row under an open-world concept is unknown, so closed-world non-derivability is not assertable — the runner reports a distinct, loud INCONCLUSIVE, never a silent pass.

A CWA-true result lifts safely into an open-world consumer: positive evidence stays positive when more information may yet arrive. The Lean mechanizes this transfer (cwa_owa_transfer, cwa_isCwa_preserved_under_info_increase) and proves the reverse unsound (owa_to_cwa_not_sound) — a conclusion that holds only by collapsing an unknown to false does not transfer the other way. The full three-valued lift of open-world membership into downstream derive heads — letting an open-world can row materialize in a derived extent — is the well-founded-semantics catch-up; today the substrate refuses the unsound interaction rather than evaluating it. The wired surface is negation-as-failure, the structural write-side guards, and the derivability test.