RFD 0007 — Missing-value semantics under OWA

• State: discussion
• Opened: 2026-05-28
• Decides: what field: T (required), field: T? (optional), and field: Truth4Of<T> (epistemic) each mean under CWA and OWA; what happens when the value isn’t asserted; how Option<T> lifts (or doesn’t) inside rule-body comparison atoms; the diagnostic surface that forces the modeler to pick an intent rather than guess one.

Question

Argon today lets a modeler write pub kind Person { age: Nat? }. What does the ? mean? Two readings, both defensible, both produce different rule-evaluation outcomes:

• Reference-ontology reading. Some persons genuinely have no age — the field’s absence is a positive fact about the world. None is on a par with Some(0) as a piece of information.
• Implementation reading. Every person has an age, but the KB may not yet record it — the field’s absence is epistemic uncertainty. None means unknown, not no age.

The OWL/SHACL ecosystem keeps these apart by treating cardinality (owl:FunctionalProperty, sh:minCount) as TBox/SHACL-shape declarations and treating ABox-incompleteness as a property of the knowledge graph, not of the property. Argon, today, conflates them: T? is the only surface, the spec doesn’t say which intent it expresses, and §5.1 line 42 — “yield Option::None if the field’s declared type is T?, else error” — forces modelers to reach for T? whenever the KB might be incomplete, even when the modeler means the implementation reading. That’s a real loss of expressivity, and it forces the rule-evaluation semantics to invent an ad-hoc lift rule for Option<T> >= T that the spec never actually specifies.

This RFD picks the semantics, picks the surface, and documents the elaborator’s lifting discipline.

Context

The motivating thread (Almeida + Almeida, 2026-05-28)

Gustavo Ladeira (Sharpe) asked:

pub kind Person { age: Nat? }

pub derive Adult(p: Person) :- p: Person, p.age >= 18;
pub derive Minor(p: Person) :- p: Person, not Adult(p);

“In OWA, can a derive resolve to CAN? Does p.age >= 18 lift to Can if age isn’t present? And then is not Adult(p) for a person with no age Is(true) (so Minor fires erroneously) or Can (so Minor stays unknown)?”

João Paulo Almeida (UFES) sharpened the framing:

“There is a key issue here to flesh out. Optionality in this form (in an implementation) is usually ambiguous. If we are building a reference ontology (about the world), an optional age would mean there [are] people without age (so, this would be a bad modeling choice). But when this is about an implementation, we’d also like to know whether within the knowledge base this information (about age) is optional. In the RDFS/OWL world, this is partially addressed with age being a functional data property (thus every person has an age even though we might not know it), and then might be SHACL constraints to clarify whether the knowledge graph must have information about age.”

JPA’s distinction is the question this RFD answers.

What the substrate already mechanizes (and what it doesn’t)

Foundation/Truth4.lean + Foundation/Projection.lean mechanize the bilattice Truth4 = {Is, Not, Can, Both} and the Pietz–Rivieccio Exactly-True projection. Reasoning/Fixpoint.lean is K3-aware: rule-body conjunction (§6.10.5 truth table) and Kleene negation (¬Is = Not, ¬Not = Is, ¬Can = Can) are the operators the stratified fixpoint already uses.

§6.9 verbatim: “The substrate enforces this by lifting the derive/query evaluation into Truth4 under OWA and projecting to Boolean only at refinement membership / if / match boundaries.” §12.2 verbatim: “Boolean projections: Can → false. Only Is(true) is designated.”

What the substrate does not specify:

1. How field: T under OWA behaves when no value is asserted. §5.1 line 42 says “error.” But the OWL functional-property pattern — every Person has an age; the KB may not know it — requires this to lift to Can, not error.

2. How Option<T> comp_op T evaluates in a rule-body atom. No rule. Today the elaborator type-errors, the parser accepts it, and the runtime would have to invent a coercion. The Gustavo trace above implicitly assumed None >= 18 lifts to Can; that assumption isn’t anywhere in the spec.

3. Whether structural-optional and epistemic-optional have separate surfaces. §6.6 says T? ≡ Option<T>. That’s the structural reading. The implementation reading currently has no surface — and §5.1’s “else error” forecloses it.

Three real gaps. JPA’s question lands on all three.

OWL / SHACL precedent

The reference systems handle JPA’s distinction with separation of concerns:

• TBox (OWL). Cardinality declarations (owl:FunctionalProperty, owl:minCardinality, owl:maxCardinality) state what is true of the world: every Person has an age. ABox-incompleteness does not contradict TBox cardinality under OWA — it means the missing fact is unknown.
• SHACL shapes. Constraints over the knowledge graph (sh:minCount, sh:maxCount, sh:datatype) state what must hold of the KB. A SHACL violation means the KB is incomplete, not that the world is malformed.

Argon’s existing machinery already has the analogous parts:

• TBox-cardinality analog. Field declarations on concepts. age: Nat says every Person has an age (OWL functional + min 1). age: Nat? says some Persons may genuinely lack an age.
• SHACL-shape analog. where { … } refinement clauses (§6.3) and #[intrinsic] (§5.2). These constrain the KB, not the world.

The pieces are in place. What’s missing is the lift discipline that connects them under OWA.

Decision

Decision pending ratification (2026-06-12, PR #289). This RFD is in discussion state, and its OE1014 story (Decision table row 1 / the lift rule below) places the required-field-completeness diagnostic at field-access / evaluation time — a query reading an unasserted required field under CWA is the schema violation. PR #289 needed a completeness gate for the insert iof(x, T) classification side-door (audit ufo-mut-06), and shipping the evaluation-time emitter is a larger build (it lifts every required-field read into a CWA cardinality check). So #289 decides and implements a narrower, complementary site: an in-body-vs-staged discriminator at commit time. A mutate body that classifies x into T and writes fields of x in the same body is constructing x in-body; completeness is judged at body end (read-your-writes, RFD 0019 RC2) and OE1014 refuses atomically if a required field is left unset. A body that only classifies — no in-body field writes to x — is staged construction and is permitted to defer (this RFD’s “ABox-incompleteness is fine”); it currently produces no diagnostic. Rationale: a blanket write-time / construction-time refusal would break staged construction across mutations (the legal_norms_can_vote::register and keystone add_sat → set_cap patterns), which this RFD explicitly blesses; keying on whether the same body populates the individual is the discriminator that lets both shapes stay green. This is a fresh design decision owned by #289, not a clause this RFD already settled — the RFD specifies the opposite site (field-access). The field-access-time / evaluation-channel emitter (Decision table row 1 CWA column, the lift rule’s state lacks ... CWA → OE1014 line) remains the open half of this RFD and is unbuilt; it is tracked at #292, and this RFD still needs ratification to lock both halves.

Three surfaces, three distinct intents

These three surfaces correspond exactly to JPA’s distinction (rows 1+3 are the implementation reading; row 2 is the reference-ontology reading), plus an escape hatch for modelers who want the bilattice shape directly. The default T row matches OWL functional-property + min-cardinality 1 under OWA; the T? row matches Rust-style structural Option.

The lift rule (the load-bearing piece)

In rule-body atom context, a field access p.field evaluates as follows:

For field: T (required, ontologically present):

state has hasField(p, v)        → Is(v) at the Truth4 level; surface value is v
state lacks hasField(p, _), OWA → Can at the Truth4 level
state lacks hasField(p, _), CWA → model-level error OE1014 (cardinality violation)

For field: T? (structurally optional):

state has hasField(p, v)         → Some(v)
state lacks hasField(p, _), any  → None  (a positive fact; no Truth4 lift)

For field: Truth4Of<T>:

state has hasField(p, v)         → Is(v)
state has not_hasField(p)        → Not        (explicit negative assertion)
state lacks both                 → Can

Surface comparison atoms use the resulting Truth4 / Option / value:

p.age >= 18          // T:    Is(true) | Not | Can per the trace above
                     // T?:   TYPE ERROR — see below
                     // T4Of: Is(true) | Not | Can — same as T, but explicit

Option<T> in comparison atoms is a type error

Option<T> comp_op T (and Option<T> comp_op Option<T>, and friends) is rejected by the elaborator: OE0612 OptionComparisonRequiresHandling with a diagnostic that suggests three explicit forms:

// 1. Pattern in the rule body — preferred when None should fail-closed
p.age is Some(a), a >= 18

// 2. Helper method on Option<T>
p.age.is_some_and(|a| a >= 18)

// 3. Match with explicit unknown handling
match p.age {
    Some(a)    => a >= 18,
    None       => false,           // pick: false / true / Truth4Of::Can
}

The first form (is Some(a)) compiles to a guarded match that fails the conjunction (binds nothing) on None — a positive fact about absence. The second is sugar for the same. The third lets the modeler explicitly say what None means in their model.

This is JPA’s point made structural: if you wrote T?, the language refuses to guess what None should mean in a comparison; you must say.

Required-field-under-OWA: the lifted access rule

§5.1 line 42 amends to:

No value present at field access — under OWA, lift to Can at the Truth4 level (the surface returns the field’s declared type via the K3 fail-closed projection: false for Bool, omitted for collections); under CWA, emit OE1014 RequiredFieldUnasserted (the schema declared this field present; the KB must record it). At construction time, the existing OE0207 IntrinsicPropertyMissing rule for #[intrinsic] fields is unchanged.

The asymmetry — construction strict, query OWA-lifted — is intentional and matches OWL: TBox cardinality requires presence, ABox completeness is a separate (SHACL) concern.

Diagnostic codes

Spec edits

Lean mechanization

The theorem statement is roughly:

theorem field_access_owa_lift
    {P : Program} {p : Individual} {f : RequiredField}
    (h_no_assertion : ¬ ∃ v, P.state.has (hasField p f v))
    (h_owa : P.worldAssumption f.declaringConcept = .open) :
    P.accessField p f = (Truth4.can, default)

with the CWA branch as a separate (sharper) statement: under CWA, h_no_assertion is provably false for any iof(p, concept) ∈ P.state (the schema mandates a value), so the case is unreachable and the elaborator’s OE1014 is sound.

The Gustavo trace, after this RFD lands

With Gustavo’s code as written (age: Nat?):

pub kind Person { age: Nat? }
pub derive Adult(p: Person) :- p: Person, p.age >= 18;
//                                         ^^^^^^^^^^^ OE0612

The elaborator rejects the comparison at OE0612, asking the modeler to pick. Gustavo then makes the modeling choice JPA was asking him to make — either:

// Reference-ontology reading: people with no age aren't adults; Minor fires
pub derive Adult(p: Person) :- p: Person, p.age is Some(a), a >= 18;
pub derive Minor(p: Person) :- p: Person, not Adult(p);
// carol (no age) → Adult = Not (the `is Some(a)` fails) → Minor = Is

or:

// Implementation reading: every person has an age; KB may not know it
pub kind Person { age: Nat }     // required, OWA-aware lift handles the gap
pub derive Adult(p: Person) :- p: Person, p.age >= 18;
pub derive Minor(p: Person) :- p: Person, not Adult(p);
// carol (no age asserted, OWA) → p.age lifts to Can
//   → Adult body = Is ⊓ Can = Can
//   → not Adult(carol) = ¬Can = Can
//   → Minor(carol) = Is ⊓ Can = Can
// Minor's extent at Bool projection: carol omitted. At Truth4Of<Person>: shown as Can.

JPA’s two intents are no longer conflated; the elaborator has forced the choice; the Truth4 lift handles whichever choice the modeler made; the diagnostic carries the explanation.

Rationale

Why three surfaces instead of two

A naive design would keep just T and T? and let OWA do all the work. That collapses JPA’s two intents into one surface (T?), reproducing today’s ambiguity. Truth4Of<T> adds a third surface for the specific case where the modeler wants the bilattice value exposed in storage — relatively rare, but exactly what one needs when modeling, e.g., a clinical-trial endpoint where “patient response = unknown” is a first-class data point separate from “patient response = no.”

Three surfaces is the minimum that lets every modeler intent be expressed cleanly:

• T: TBox cardinality 1 + OWA-tolerant ABox.
• T?: structural optionality (no TBox cardinality assertion).
• Truth4Of<T>: explicit four-valued storage.

Why type-error on Option<T> comp_op T

JPA’s “ambiguous” is the load-bearing observation. If the elaborator silently coerces None to false (Reading C, SQL-style), the modeler never confronts the ambiguity and the model’s semantics drifts from intent. If the elaborator silently lifts None to Can (Reading A, Truth4-style), the modeler is again not consulted. The type error is the modeler-respecting move: ask the modeler what they mean.

The cost is one extra ceremony at every Option<T> comparison site (is Some(a), a >= 18 instead of a >= 18). The benefit is no silent ambiguity, no quiet semantic drift, and a diagnostic that doubles as documentation.

Why required-field-under-OWA lifts to Can (not errors)

Without this lift, the spec is internally inconsistent. §6.9 promises OWA semantics (knowledge is open; absence is uncertainty); §5.1 promises construction-time strict checks (required fields must be set). Today these collide: under OWA, an iof(carol, Person) axiom can be asserted with no hasAge tuple, but accessing carol.age errors out — which contradicts §6.9’s premise that absence is uncertainty.

The fix preserves both intents by separating their layers. Construction (the axiom event being inserted) stays strict — you can’t write Person { name: "carol" } without age because the construction is a single axiom and missing required fields are malformed at the event level. Query (subsequent field access on a possibly-incomplete KB) lifts to Can under OWA, matching OWL functional-property semantics exactly: every Person has an age (TBox), but we may not know it (ABox-incompleteness is fine under OWA).

CWA does not tolerate this: under CWA, an iof(carol, Person) with no hasAge(carol, _) is a schema violation, and OE1014 is correct.

Why OW1015 OptionalFieldAmbiguousIntent

The warning catches the JPA case at declaration time: a modeler writes f: T? without saying which intent they mean. The warning links to the table in §5.1.x and suggests either #[doc] documentation, an explicit #[intent(structural)] attribute, or migration to T + OWA. It can be silenced per-field. The warning is off by default in the prelude (std::* legitimately uses T? for plumbing types like Option<Person> returned from one { ... } queries) and on by default in user code with #[intent(...)] available as the disambiguator.

Alternatives considered

A. Implicit lift of Option<T> to Truth4 in rule bodies (Reading A)

Auto-translate None → Can, Some(v) → standard comparison verdict. Rejected. Silently picks the implementation reading; loses the reference-ontology reading entirely. Modelers who wrote T? to mean “some persons have no age” would find their rules treating those persons as unknown instead of positively-not-an-adult — a semantic regression that’s invisible at the source. Fails JPA’s framing.

B. Option<T> comp_op T returns Option<Bool> via functor lift (Reading C)

Auto-translate None comp_op v → None, Some(a) comp_op v → Some(a comp_op v). Force the modeler to write match on the result. Rejected. Type system gets noisier without solving the underlying ambiguity; modelers will reflexively write match { Some(b) => b, None => false } and the SQL-NULL silent collapse returns. The type-error path (Decision) forces the choice earlier where the modeler still remembers the intent.

C. Only two surfaces: T + OWA and T?

Drop Truth4Of<T> as a field type. Rejected. Loses the explicit-epistemic case (clinical-trial endpoints, audit fields marking “unknown” as a first-class value). The marginal cost of admitting Truth4Of<T> as a field type is low — it’s an existing stdlib type — and the expressivity is meaningful for medical / legal / scientific modeling.

D. Defer the entire question; leave §5.1’s “else error” rule as-is

Wait for more modelers to hit the wall. Rejected. Two of the language’s core consultants (Gustavo, JPA) hit it on day one of working through a temporal model. The substrate is Truth4-aware; the spec gap is at the surface; the cost of resolving is small (~5 elaborator checks + the diagnostic codes). Deferring would let modelers internalize ad-hoc workarounds and would force oxc-instantiate to ship without crisp Option-handling semantics.

E. Adopt OWL/SHACL syntax wholesale (#[functional], #[min_count], #[max_count])

Map TBox-cardinality + SHACL-shape vocabulary to attributes on field declarations. Rejected as the primary surface. Argon’s T / T? distinction is more ergonomic than OWL’s flat-property + cardinality-restriction model; adopting OWL vocabulary as the primary surface would be a Rust-aesthetic regression (per the user-memory directive defaulting to Rust/Cargo aesthetic). The OWL/SHACL pattern is reachable as a target via the field-type decision matrix above, without forcing modelers to write #[functional, min_count = 1] at every field site.

Consequences

Source-level

• A pub kind Person { age: Nat } model becomes feasible under OWA where today the spec forces Nat?.
• Option<T> comp_op T rule-body atoms must be rewritten with is Some(a) / is_some_and / match. The Cargo-style ecosystem migration: one-shot cargo ox fix rewrite per repo.
• Truth4Of<T> becomes available as a field type. Modelers who want OWL-style four-valued storage have a first-class surface.

Substrate-level

• Two new variants on FieldDecl (intent kind: required / optional / epistemic).
• One new branch in accessField: returns (Truth4, Value) instead of Value. Hot-path impact: one extra tag byte in the tuple-encoding, negligible.
• relation_tuple axiom kind unchanged; the lift happens at the accessField level, not in storage.

Runtime-level

• The K3 truth tables (§6.10.5) are already mechanized and used; this RFD adds no new operators.
• Query results returning collections now omit Can-valued field rows under K3 fail-closed projection — already the spec, but newly exercised at scale.

Diagnostic-level

• Five new codes (OE0612, OE0613, OE1014, OW1015, OE1016).
• One existing code (OE0207 IntrinsicPropertyMissing) keeps its current semantics; the new OE1014 covers the disjoint case of required-non-intrinsic absence under CWA.

Compatibility

T? retains its current Option<T> semantics — modelers who already use it for structural optionality see no behavior change. The new OE0612 may flag existing rule bodies; the suggested fix is purely mechanical (is Some(a), insertion). T under OWA gains new expressivity that didn’t exist before. No silent semantic changes to any existing well-typed program.

Open questions

OQ1 — Truth4Of<T> as field type interactions with mutation

A field declared f: Truth4Of<T> can be set to Is(v), Not, Can, or Both(v1, v2) via insert. What is the storage representation? Likely two relations: hasField_pos(p, f, v) and hasField_neg(p, f). Both is encoded as both relations holding simultaneously. The mapping is mechanical but worth specifying before implementation.

OQ2 — Interaction with refinement clauses

A refinement pub subkind Adult <: Person where { self.age >= 18 } over a required age: Nat field, under OWA, evaluates to Is | Not | Can per §6.9. Does the refinement-classification machinery in TypeSystem/Soundness/FlowTyping.lean handle the Can case? Spot-check needed: I expect yes (the existing OWA branch already covers it), but the new lifting rule introduces a Can source the type system didn’t previously consider.

OQ3 — Aggregate semantics over Can-valued cells (resolved — see RFD 0011)

What does sum { p.age | p: Person } evaluate to when some p.age lift to Can? Resolved by RFD 0011: monotone aggregators (sum non-negative, count, set_collect) evaluate to Truth4Of<T> with interval bounds [lower, upper] where lower = aggregate over filter-Is-true cells and upper = aggregate over filter-Is-true-or-Can cells; non-monotone aggregators (min, max, avg, string_join, percentile) propagate Can (any Can-cell in the filter set → whole result is Can). The Truth4 result is projected at the typed boundary per §12.2’s K3 fail-closed rule; the projection is observable via diagnostic OW0613 (info in query/fn, warning in derive, error in check) and an always-present aggregation-metadata envelope on query results carrying the interval bounds and Can-cell counts. The motivating Gustavo Ladeira / J.P. Almeida thread (2026-05-28 → 2026-05-29) is the worked example; the full design and rationale lives in RFD 0011.

OQ4 — Path traversal under Can-valued intermediate steps

For alice.parent.spouse.age, if alice.parent lifts to Can, does the full chain short-circuit to Can or does it propagate through the K3 conjunction of step verdicts? Existing field-path semantics in Reasoning/Rule.lean treats path steps as conjunctions; this would give natural propagation. Confirm.

OQ5 — #[intent(structural)] / #[intent(epistemic)] as the disambiguator

The proposed attribute makes the modeler’s intent explicit at declaration time. Should it be required for T? declarations in non-prelude modules? Two readings: (a) required (zero-ambiguity policy; matches Argon’s “no implicit override” philosophy from §5.2); (b) optional with OW1015 warning (gentler migration). Default to (b); revisit if modelers report confusion.

OQ6 — Migration path for existing UFO vocabulary

The UFO stdlib package declares several optional fields in its concept catalog (Person, Organization, …). Are these structural-optional or epistemic-optional? A scan of ufo/src/*.ar is needed to assign intents per-field before this RFD lands; this is a UFO-package PR, not an argon PR.

References

• §5.1 (struct/concept field declarations, OE0207), §5.2 (concept supertype clauses), §6.3 (refinement, three-valued membership), §6.6 (T? ≡ Option<T>), §6.9 (CWA/OWA), §6.10.5 (strong-Kleene truth tables), §7.3.1 (rule-atom grammar, is unknown outcome-suffix), §12 (Truth4 + Pietz–Rivieccio projection) — spec/reference/src/
• Foundation/Truth4.lean, Foundation/Projection.lean, Reasoning/Fixpoint.lean, Reasoning/State.lean — substrate mechanization
• oxc-instantiate (elaborator), oxc-reasoning::compile::Value (runtime carrier) — implementation sites
• W3C OWL 2 Web Ontology Language Direct Semantics, §2.3.3 (functional property axioms)
• W3C SHACL §3 (Shape constraints)
• Pietz, A. & Rivieccio, U. (2013). Nothing but the truth. Journal of Philosophical Logic — the Exactly-True semantics underlying §12.2’s K3 fail-closed projection.
• Belnap, N. (1977). A useful four-valued logic. — the underlying bilattice.
• Almeida, J.P.A. (UFES) and Ladeira, G. (Sharpe), Slack thread, 2026-05-28 — the motivating discussion.