Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

RFD 0045 — The world-assumption write-side: refuse-on-K3-not and the #[world] opt-in

  • State: discussion
  • Depends on: RFD 0025 (check discharge — the delta-guard this rides), RFD 0017 (the where/iff refinement split — the owned-vs-derived escape), RFD 0027 (the meta-property plane and the $axis catalog), RFD 0031 (the relation-constraint plane and the D-013 disjoint/complete/partition block surface)
  • Blocks: #627 (set-valued metaxis — its membership read needs the world-side semantics settled), #697 (the breaking-change taxonomy’s closed→open arm), #249 residue, packages/mlt Phase 2
  • Implements: the §6.9 per-concept world assumption (today specified but inert), the meta-plane keystone ruling R1 (#628)

Question

A modeler declares partition Vehicle { Car, Truck } and then inserts a Vehicle that is neither a Car nor a Truck. What happens? Three answers are on the table: refuse the write, derive one of the missing memberships, or cascade some repair. The same question recurs one plane up, on derived membership: a Person becomes an Adult when iff age >= 18 holds — but under open-world, age may be absent, so the refinement is neither true nor false. Does the derived Adult membership get asserted, refused, or left undecided?

These are not taste calls. The substrate already fixes the answer; this RFD records it and builds the one surface that lets a modeler opt out of the default. Concretely: (1) what is the write-side rule when a covering or derived-membership constraint is unmet, and (2) how does a concept declare that it lives under the open-world assumption instead of the closed-world default?

Context

Where we are. Three pieces are already on main, and they constrain the answer.

The world-assumption substrate exists. WorldAssumption (oxc-protocol/src/world_assumption.rs) mirrors the Lean Argon.Schema.WorldAssumption.WorldAssumption — Closed and Open, with WorldAssumptionMap the total function CN → WorldAssumption over a sparse override map plus a default. The type is wired; nothing reads it to change behavior yet.

The #[world] directive parses but is refused. oxc-instantiate/src/directives.rs:520 registers world and rejects it: “per-concept world assumption (§6.9) is specified but not built; the engine evaluates closed-world unconditionally.” So every concept is closed today, unconditionally.

Covering already ships under the closed default. The D-013 block surface (disjoint/complete/partition, RFD 0031) lowers to RFD-0025 checks: OE0240 (overlap), OE0241 (runtime covering, delta-guard-enforced at write), OE0242 (build-time static covering over the <: graph), OE0243 (non-subtype member). A partition whose cover is unmet at write is refused today. The covering question is therefore not whether covering is enforced — it is — but under which world assumption the enforcement should soften.

Why the answer is forced, not chosen. The closed-world write-side rule composes theorems already proven in spec/lean/Argon/, with no new framework and no bridge lemma. The composition was validated against the source, not assumed:

  • cwaCollapse_is_iff (TypeSystem/Soundness/CwaOwa.lean:110) — collapsing a classification yields is only if the input was already is. The closed-world collapse turns can into not, never into is. It cannot fabricate positive evidence.
  • collapse_conclusion_lacks_positive_evidence (CwaOwa.lean:197) — ¬ cwaTrue .can: a conclusion that exists only because the collapse invented a not carries no positive backing.
  • guard_iff (Reasoning/Checks.lean:288) — the RFD-0025 delta-guard passes iff violations post ⊆ violations pre. A write that creates a violation is refused; pre-existing violations are observed but do not block.
  • violations_mono_of_positive (Checks.lean:298) and the Truth4 joins (Foundation/Truth4.lean, can ∨ can = can, is ∨ _ = is) — the closure under which an unmet covering classifies as not and the check fires.

Put together: an unmet covering under the closed default is not, the covering check fires, and the delta-guard refuses the write. Refuse is the closed-world behavior the substrate already enforces; this RFD names it and makes the open-world alternative declarable.

Decision

D1 — The write-side rule: refuse-on-K3-not

When a covering, partition, or derived-membership constraint is unmet at a write under the prevailing world assumption, refuse the write iff the constraint classifies as K3 not (a definite violation). Under the closed default, an unmet covering collapses can → not and is refused — the behavior on main. Under #[world(open)] the same unmet covering stays can and is tolerated (incomplete is not violated; see D2).

This is one rule, applied at two planes:

  • Covering / partition (complete/partition): an instance of the parent whose membership in no declared variant can be established is not under closed-world → refused (OE0241), can under open-world → tolerated.
  • Derived membership (iff, RFD 0017): a computed membership whose refinement lands K3-undefined is not under closed-world → the membership is absent and any check depending on it fires; under open-world the refinement reads three-valued and a membership that would be asserted only by collapsing can → is is refused, never asserted.

Derive is rejected as unsound, not declined as a preference. Deriving the missing membership asserts is where the model only supports can. cwaCollapse_is_iff forbids exactly this move, and a fabricated is does not survive re-evaluation: cwa_owa_transfer (CwaOwa.lean:133) carries genuine is conclusions from closed to open worlds, but a derive-fabricated membership has no is to carry, so an open-world reader would find can. The two planes would disagree about the same fact. Cascade is rejected on a separate ground: a repairing write breaks the fixed-gate constancy theorems and the append-only event log, and it smuggles the same abductive guess into the store.

D2 — #[world(open)] becomes a real per-scope opt-in

Lift #[world(open)] from reserved-and-refused (directives.rs:520) to a real per-scope annotation that writes the concept’s entry in the WorldAssumptionMap.

  • The default stays closed. An un-annotated concept behaves exactly as it does today. Shipping this RFD is observably a no-op until a concept is opted into open. This is forced by the CWA-to-OWA monotone-transfer theorem: closed is the sound default, and opening a concept is the modeler’s explicit declaration that absence means ignorance, not falsity.
  • #[world(open)] on a concept makes its refinement reads three-valued: an absent fact reads can (unknown), not not (false). A where-asserted membership is still admitted (it is owned — D3); an iff-derived membership that lands can is refused (D1).
  • #[world(open)] on a concept governs the generalization sets declared under it. A partition/complete cover under an open concept softens from refuse to K3-tolerate: an instance not yet placed in a variant is can, not a violation. Only covering softens. Disjointness is world-assumption-invariant — a disjointness violation (OE0240) is two memberships that are both is, a positive overlap, and a positive overlap is a definite violation under any world assumption. The keystone rule softens refuse-on-K3-not (covering); it has nothing to tolerate on refuse-on-positive-overlap (disjointness), which is a separate, invariant rule.

D3 — The owned-vs-derived escape already exists: where / iff

No new assertion surface is needed for “I take responsibility for this membership.” RFD 0017 already split it:

  • where = asserted / primitive. The modeler owns the membership; insert iof(x, C) is permitted; violation is OE0668. Under open-world, an absent field permits the write — information-absence is not violation.
  • iff = defined / derived. Membership is computed; explicit insert iof is rejected (OE0211); under open-world it refuses-on-K3-not (D1).

So the modeler’s lever is the refinement keyword they already choose. Use where where the model asserts a membership it owns; expect iff-derived membership to refuse rather than guess when the evidence is absent.

D4 — Scope, attachment, and the relationship to store placement

#[world(open)] attaches to a concept declaration — the surface §6.9 / 06-types.md:230 already documents — giving the directive the real positions it lacks today (directives.rs:520). It writes a per-concept override into WorldAssumptionMap; the default remains Closed. There is no separate per-generalization-set annotation: a concept’s world assumption governs the covers declared under it (D2), so the surface stays exactly what the book scopes — concepts only.

This is the modeling opt-in — a statement about a concept’s domain (is the set of Persons in this model closed, or partial?). It is distinct from, and composes with, the store-side world tiering in RFD 0036 D6 (feat/store-placement-and-world-assumption), where a federated external store may force open-world reads on the data it owns. Where both apply, the store tier and the concept annotation must agree or the existing mixed-world conflict gate (MixedWorldAssumptionConflict) fires.

Coordination hazard — one WorldAssumptionMap writer, not two. This RFD’s per-concept opt-in and RFD 0036 D6’s store-side tiering both write the same WorldAssumptionMap. They must converge on a single writer reconciled through MixedWorldAssumptionConflict; two independent writers would silently disagree. This is a real blocking coupling between the two arcs, not a prose aside — whichever lands second builds on the first’s writer.

The decidability cost is real and must be honored in the tier ladder: mixing closed predicates into an open-world base can push data complexity from PTIME to coNP-hard (Lutz et al. 2013). A per-concept #[world] is not free; the §10 classifier accounts for it.

D5 — Diagnostics

  • OE0706 stays as the general reserved-directive gate — it still serves #[brave], #[intrinsic], and the other reserved directives. Once #[world] is built it simply stops firing for #[world].
  • OE0241 (covering) softens under #[world(open)] rather than being replaced: the same check, evaluated three-valued, tolerates can. OE0240 (disjointness) does not soften — a positive overlap is a definite violation under any world assumption (D2). OE0242 (build-time static covering) is unaffected — it is a catalog-level well-formedness check over the <: graph, independent of instance data and world assumption.
  • No new error code is required. One discretionary micro-call remains (the only piece of this RFD that is preference, not consequence): when a write is tolerated under open-world that would have been refused under closed-world, emit an informational diagnostic or stay silent? Recommended: silent. Opting a scope into open is itself the declaration that incompleteness is intended; a note on every such write is noise. If a lint is ever wanted, it belongs in the allow/warn/deny lint plane (#707), not as a hard diagnostic.

D6 — Lean obligations

The closed-world write-side rule (D1) is already discharged by composition — cwaCollapse_is_iff + guard_iff + violations_mono_of_positive + the Truth4 joins, as walked in Context. No new theorem, no bridge lemma.

The #[world(open)] softening (D2) rides the existing three-valued CwaOwa semantics: tolerating-on-can is the sound direction (it weakens refusal, never strengthens an assertion), so it needs no new framework.

One Lean-catchup item is owed, and it does not gate this RFD (Rust leads the reasoner here). The covering check is implemented in Rust, but its closed-world covering-completeness soundness is not yet mechanized: CwaOwa.lean proves positive-evidence transfer, not “the covering check fires whenever coverage is unmet.” That theorem — sitting between Storage/AxiomBody.lean’s PartitionAxiomBody and Reasoning/Checks.lean — is tracked as #760. File it; proceed on the softening under existing semantics.

Alternatives considered

  • Derive the missing membership. Rejected as unsound (D1): it asserts is from can, which cwaCollapse_is_iff forbids, and the fabricated fact fails cwa_owa_transfer re-evaluation. This is the option a forward-chaining engine cannot take soundly — a covering axiom is an open-world disjunction (“in at least one variant”), and a CWA-NAF engine cannot represent the disjunction, so deriving a specific variant is an abductive guess.
  • Cascade a repair. Rejected: breaks the fixed-gate constancy theorems and the append-only event log, and carries the same abductive guess.
  • Make open-world the default. Rejected: closed is the sound default by the monotone-transfer theorem, and it is the established §6.9 doctrine (“extents are the authority”). Opening is the exception a modeler declares, not the baseline.
  • A new assert-style membership statement for the owned case. Unnecessary: where/iff (RFD 0017) is already the owned-vs-derived lever.

This rule is the integrity-constraints-as-selective-CWA pattern from the description-logic literature (Motik, Horrocks, Sattler 2007; Tao, Sirin, Bao, McGuinness 2010): treat a covering or partition as a CWA-checked integrity constraint — denial-on-violation — layered over an OWA base. Per-concept world assumption is itself prior art (Reiter 1978; the Open/Closed/ClosedWithDefault tiers of earlier systems). The delta-guard-check model is exactly that pattern.

Sequencing

  1. R1 (this RFD) — record the write-side rule; no code change, the closed behavior already ships.

  2. #[world] surface — lift it from reserved (directives.rs:520) to a real per-concept annotation writing WorldAssumptionMap; soften OE0241 (covering) under open, leaving OE0240 (disjointness) invariant; refuse-on-K3-not on the iff path. Sequenced after the meta-plane classifier seat clears oxc-instantiate — one seat in the checker at a time. The same change satisfies the book↔engine drift gate: rewrite §6.9 / 06-types.md’s “refuses today” language to the built behavior.

    Prerequisite — the reasoner must consult the world assumption for negation (a live gap). The package-wide default_world is already a reachable manifest field (oxc-workspace/src/lib.rs:385, "open"/"closed", RFD 0036 D5), but the reasoner consults it nowhere — NAF is evaluated unconditionally closed-world. Under default_world = "open", NAF over a catalog-closed axis relation ($axis, and $setAxis once #627 lands) wrongly reads not where the open world demands can. Threading WorldAssumptionMap into the oxc-reasoning executor so NAF over these relations is world-gated (v ∉ S ⇒ not under closed, can under open) is a prerequisite this RFD’s open softening rests on, and it closes the pre-existing single-valued $axis gap at the same time. The soundness condition is already mechanized (AxisRelation.lean’s “K3-honest only under CWA”; the set analogue in Scratch/SetValuedAxis.lean’s setMembership_k3_honest); the executor is the catch-up.

  3. #760 Lean-catchup — mechanize covering-completeness soundness, ahead of or alongside the softening.

  4. #627 set-valued metaxis — now unblocked on the world-side semantics; its own set-membership K3 soundness is mechanize-first scratch-Lean, separate from this RFD.

Relationship to existing issues

  • #628 / R1 — this RFD is the ruling that issue tracks as gating the meta-plane keystone.
  • #627 — the membership read over a set-valued axis needs D1/D2 settled; this RFD settles them. The set machinery itself is #627’s own work.
  • #697 — closed → open is now a real per-concept property, so the breaking-change taxonomy’s world-flip arm is definable (a flip is breaking iff a NAF clause depended on the closed collapse).
  • #760 — the owed covering-completeness Lean-catchup (D6).
  • RFD 0036 D6 — the store-side world tiering composes with the per-concept opt-in via the existing mixed-world conflict gate (D4).