World assumptions (CWA / OWA)

A world assumption governs how the absence of evidence is interpreted:

• Closed (CWA) — if a fact isn’t derivable, it’s false. Negation-as-failure is total.
• Open (OWA) — if a fact isn’t derivable, it’s unknown. Negation requires positive disproof.

The blessed default is CWA; OWA is a live per-concept opt-in. Every concept Argon evaluates is closed-world unless it carries a #[world(open)] mark: negation-as-failure over the stratified / well-founded fixpoint (Rule atom — fn, derive, query, mutate, check, truth values) treats an unmarked concept’s absent membership as definite-false. The package-level default_world (CWA unless a manifest sets it otherwise) governs every concept without an explicit mark. This default is a deliberate choice: an Argon program is a data system whose extents are the authority for what is true, and CWA is the regime that makes “not in the extent” mean “false”. A modeler who wants the OWL/DL open-world reading for a specific concept opts that concept in with #[world(open)], described below (RFD 0045, #787/#796).

CWA is the operative default because Argon’s primary use is application data — counts, payments, schedules, classifications — where the stored extent is the closed world. Concepts that model genuinely-incomplete knowledge (where “absent” means “unknown”, not “false”) opt into the open-world reading per the surface below.

Per-concept OWA opt-in (#[world(open|closed)]) — live. The surface is a #[world(...)] attribute on an ontologically-classified concept:

#[world(open)]
pub type LegalAgent { mut name: String }   // OWA — `unknown` is distinct from `false`

The world directive is executed (RFD 0045 D2): the elaborator reads the policy word — open or closed, any other word is a loud refusal — records the concept’s world assumption on the per-concept world map (keyed by qualified concept path), and the reasoner stamps that map onto every evaluation catalog so each negated concept-membership atom is read under its own concept’s world. The attribute is concept-only (OE0707 on other placements). Concepts without the attribute inherit the package default_world (CWA by default).

The OWA semantics. The world a concept declares changes how the substrate reads its absence:

Interaction with negation-as-failure (Rule atom — fn, derive, query, mutate, check). Under CWA, not P succeeds whenever P is not derivable. Under OWA, an absent P(x) is unknown, not a definite not — so a closed-world not H whose derivation depends on an open-world negation does not get to read that unknown as false. Rather than silently over-asserting the head, the substrate refuses that genuinely-unsound shape at ox check / ox build (OE1367 NegatedOpenWorldDerived): mark H’s concept open-world too (so not H tolerates the unknown), or restructure so the open-world negation does not flow into a closed-world-negated head. This is world-honest negation-as-failure: the engine honors default_world and each concept’s mark instead of evaluating closed-world unconditionally. The is unknown rule atom (Rule-atom grammar) is reachable under OWA — an open-world concept’s absent membership flows through it as unknown.

Interaction with the write side. A concept’s world governs its compiler-synthesized structural checks. Under the closed-world default a complete/partition covering check fires when no member membership is derivable (OE0241) and a disjoint overlap check refuses a double-classification (OE0240). Under an open-world concept the covering check softens to refuse-on-K3-not — refuse only on a definite violation, tolerating the merely-unknown case — while disjointness stays world-invariant (a positive overlap is definite under any world). This is the RFD 0045 D1/D2 design.

Interaction with the test atom. assert [not] derivable F(x) (Runtime contract) reads F’s world directly: a present row is PASS/FAIL; an absent row under CWA is definite non-derivability (FAIL for derivable, PASS for not derivable); an absent row under OWA is unknown, so closed-world non-derivability is not assertable — the runner reports a distinct, loud INCONCLUSIVE, never a silent pass.

Interaction with refinement (Refinement). The world a concept declares makes iff-derived membership three-valued — unknown does not grant membership, and a primitive where invariant is the dual where only a definite false denies a write — whereas under CWA unknown collapses to false in both directions. The three-valued refinement field-access discipline is a separate mechanism: a refinement predicate reading a field with no recorded value evaluates to unknown rather than failing — the K3 fail-closed boundary of Refinement, orthogonal to the concept-level world assumption. A missing field makes a predicate unknown; the world assumption then decides whether that unknown collapses to false (CWA) or is preserved (OWA).

Required-field completeness under CWA. Under the closed-world default a required field that is unasserted is a schema violation, not an unknown. OE1014 RequiredFieldUnasserted fires for the in-body construction case — a mutate body that classifies an individual with insert iof and populates its fields in the same body — at body end / commit time (see mutate). The construction-time gate for brace construction (insert T { … } missing a required field, OE0207) is unconditional. Under an #[world(open)] concept an unasserted required field is unknown rather than a violation.

Cross-world conservativity (mechanized). A CWA-true result lifts safely into an OWA consumer — positive evidence stays positive when more information may yet arrive. The base transfer theorem is mechanized at TypeSystem/Soundness/CwaOwa.lean (cwa_owa_transfer): a refinement membership established under CWA remains valid when re-evaluated under OWA, and cwa_isCwa_preserved_under_info_increase extends this to a more-informative consistent (K3) state. The reverse is provably not sound (owa_to_cwa_not_sound): a CWA conclusion that holds only via the closed-world collapse of an unknown to false does not transfer. The module is deliberately parameterized over the WorldAssumption — the CWA default is a surface/engine policy, not a substrate theorem, so the mechanization arbitrates the relationship between the two regimes without privileging either. The bitemporal lift of the transfer is in Locality/Temporal.lean.

Module-extraction interaction. Cross-module imports preserve CWA conclusions about the imported signature via ⊥-local module extraction; the Σ-scoped conservativity theorems are in Module extraction (tree-shaking) (Locality/ScopedConservativity.lean, Locality/DomainConservative.lean).

Per-(standpoint, concept), not per-(concept, time). A world assumption is declared per-(standpoint, concept), never per-(concept, time). A modeler needing different closure disciplines across valid-time would declare two or more standpoints with VT-scoped activation conditions and compose them via standpoint federation (Standpoints and modal operators); the substrate WA-map signature has no time argument. Attempting a per-concept closure with an explicit VT scope without standpoint decomposition is refused with OE0810 WorldAssumptionTemporalIndex.