RFD 0054 — Set-valued, characterization-relative composition over standpoints

• State: discussion

Question

A record holds more than one rival way of characterizing the same underlying facts, and the domain genuinely permits more than one (a transaction read as a sale vs. a financing; a party read as an owner vs. a conduit). The two readings are not two values on a shared axis — they are outputs of two different deterministic theories over the same brute facts: one yields a recognized gain, the other a loan balance and an interest schedule. The honest computation carries every rival characterization through derivation independently and hands back the set of characterization-indexed results — never a single reconciled answer, because collapsing to one silently relocates the choice onto the machine.

How does Argon represent and evaluate this — holding a set of rival characterizations un-collapsed, deriving each independently, and reading a sound qualitative floor across them — and exactly which part is already in the substrate, which is a small addition, and which genuinely needs a model engine?

This RFD does not redefine the standpoint surface (§11), the federation semantics (Standpoint/Federation.lean), the decidability ladder (§10), or the world-assumption gates (RFD 0036). It sits on top of them and fixes the composition primitive and its evaluation strategy.

Summary of the answer

A characterization is a standpoint — not by analogy but by identity: a standpoint is a context carrying its own facts and rules, related by a <: lattice, with each standpoint internally consistent (strict default) and disagreement preserved across standpoints. That is exactly “within a fixed frame the collapse is determinate fact-finding; across frames, hold the set.”

The substrate already does most of the work. The deterministic core needs one small addition (a non-collapsing, standpoint-indexed read), and the modal boundary read is ordinary stratified Datalog for the decidable fragment. A model engine (tableau over std::kripke) is genuinely required, but only for the intractable / infinite / unstratified fragment, and a refusal gate holds its place soundly until it lands.

Verified ground truth

Every claim below is read from source; the design rests on these.

1. Federation does not collapse rival values. Store::query_derive_federated keys the AFT info-join on the full tuple (encode_tuple), so distinct per-characterization values are distinct tuples that each survive as Is. What federation discards is the standpoint index (it folds over (_standpoint, rows)). Truth4::Both arises only for the identical tuple asserted positively in one standpoint and negatively in another (Federation.lean::federate_eq_both_iff; AFTEquivalence.lean T3: both ⟺ no consistent global K3-section).

2. Standpoints are the characterization carrier. A standpoint scopes facts and derive rules (§11). Each standpoint is internally K3-consistent under the default strict consistency policy; cross-standpoint disagreement is preserved at federation regardless of policy (Consistency.lean). The <: lattice is an enforced DAG (OE1211), so the cross-standpoint fold always stratifies stratum-by-stratum (Stratification.lean, Vennekens-Gilis-Denecker 2006). The per-standpoint evaluation context is materialized today by materialize_predicates_for_standpoint (DEFAULT layer ∪ stamped-s facts; the runtime side of Visibility.scoped_view_eq_default_union_own).

3. Modal over the standpoint frame is finite ∀/∃, and compiles to Datalog. box w P = ∀w'. accessible w w' → P w'; the standpoint frame is S4, worlds = standpoints, accessibility = the <: reflexive-transitive closure (Reasoning/Modal.lean). Gómez-Álvarez, Rudolph & Straß (KR 2023) prove Standpoint-EL+ compiles to ~30 pure Datalog rules (PTIME), worlds reified as standpoint IDs, accessibility as explicit transitive closure, with box via stratified negation or count-equality. The <: ancestor closure is already precomputed (standpoint_lattice.rs::ancestors, global-control.standpoint_ancestor_sets).

4. The intractable fragment is sharp. Adding empty standpoints (NP-hard), rigid roles (coNP-hard), or nominals (EXPTIME-hard) each independently breaks PTIME (IJCAI 2023); modal⊗temporal cross-nesting is already refused (OE0712). These, plus the rigidity frame over infinite configuration worlds and unstratified modal recursion, are the fragment that needs a model engine.

5. There is no single “modal engine” — evaluation is a compile-time strategy choice (translation to Datalog vs. tableau-on-demand). The decidability ladder places modal as its own tier (cost modal+FOL) that dispatches: static discharge, else an external reasoner over std::kripke (Decidability/Modal.lean).

6. Two gaps are live in the implementation. (a) AtomIR::Modal{op,inner} is frame-blind and is stripped to inner at compile (compile/rule.rs), while being classified Tier::Modal and admitted — so a box/diamond program builds, runs, and is confidently wrong for anything but the rigid-default case (a live silent-wrong). (b) std::kripke is not built (no package), and there is no standpoint-frame discharge in the Lean (only the rigidity-frame fixed discharge in StaticDischarge.lean).

Design

D1 — The reification surface: the across binder

The across clause on a query gains an optional binder:

federation-clause ::= 'across' (Ident 'in')? '[' standpoint-ref (',' …)* ']'

• across [S₁, S₂] (no binder) — federate: the existing AFT info-join. Preserved unchanged; it is the right tool for genuine same-proposition disagreement detection (the Both read).
• across s in [S₁, S₂] (binder) — enumerate: bind s to each standpoint in turn, evaluate the body in standpoint s’s view, and project s as a first-class Standpoint-typed column. The result is the rival-set, indexed by characterization — held un-collapsed.

The binder/no-binder distinction is the enumerate/federate switch: local, syntactic, no new keyword. The runtime already computes the per-standpoint contributions (materialize_predicates_for_standpoint per sid, then the dispatcher); enumerate keeps the sid as a result column instead of folding it away. This is the product/relational Kripke-frame strategy (“add a world variable to every predicate”) realized at the query boundary.

A Standpoint value is a reflective name (the sid: NameRef the runtime already carries), in the family of the reflective TypeRef (RFD 0027 / the reflective-name surface). It is an ordinary value: downstream rules join on it.

D2 — The boundary read: qualitative □ / ◇, never counted

With the standpoint reified as a column on a relation R(s, …), the characterization-relative reads are ordinary, already-wired aggregates:

• □ (necessity / sound floor) — forall s in frames: R(s, …) — survives under every admissible characterization. forall lowers to count-equality (count{s : P} == count{s : frame}), which is a boolean, not a ratio.
• ◇ (possibility / contestable frontier) — exists s in frames: R(s, …).
• qualitative worst-case — ◇(¬survives): is there an admissible frame under which it fails (the adversary’s move). Wired via NAF + exists.

The discipline is structural: the natural encoding produces a qualitative verdict, never a measure. A count of frames (count{surviving}/count{frames} → a probability over worlds) is an off-path, deliberate construction — the forbidden scalarization, and not what □/◇ produce. The sound floor is a meet computed as a read that leaves the held set intact; it is never the AFT info-join (which would replace the set with one tag). The numeric min/ argmin over a value codomain is not a substrate read: it is the optimizer’s move on the held set, human-invoked, and lives above the language.

Soundness of □-as-forall over the frame set rests on the frame set being closed and complete — which it is: the across set together with its <: ancestors is fully known (the closed-world-over-a-closed-set condition the federation gates already enforce, §6.9 / RFD 0036).

D3 — Standpoint-frame box / diamond translation

For box/diamond appearing in a rule body over the standpoint frame (frame root recovered from the enclosing standpoint block via the lowering context, or the across set for a query — see D7), lowering translates to stratified Datalog over the reified relations and the standpoint accessibility relation reach:

diamond_s P(x̄)  ≡  ∃ s'. reach(s, s') ∧ P(s', x̄)
box_s     P(x̄)  ≡  ¬ ∃ s'. reach(s, s') ∧ ¬ P(s', x̄)      (stratified NAF)

reach(s, s') is the <: reflexive-transitive closure (the precomputed ancestor sets), exposed as a reasoning relation. P(s', x̄) is P reified with the world column — materialized per standpoint and tagged (the product reification). Tiers: closure (the <: closure) + recursive (the stratified aggregate). This is the KR-2023 reduction; the box-as-NAF form is sound because the frame set is closed (D2).

D4 — The dispatch and the silent-wrong fix

box/diamond lowering becomes frame-aware, replacing the unconditional strip:

This closes the live silent-wrong: a program that the engine cannot soundly evaluate refuses loudly rather than silently stripping to rigid-default.

D5 — Determinacy-mode is a user enum

The tripartite determinacy-mode {indeterminate-by-law | unknown-by-data | low-confidence} is a flat user-level enum column on the per-characterization facts, carried through derivation and dispatched on by the D2 aggregates (e.g. □(survives ∧ mode ≠ indeterminate-by-law)). It is not a truth-value algebra: Truth4 is not extended, and the determinacy-mode is orthogonal to both Truth4 (cross-standpoint agreement) and well-founded-undefined (derivability). Argon’s enum values (struct/enum value carriers) already model it; this is near-commodity and needs no substrate change.

D6 — The model engine (held by the refusal gate)

The non-translatable fragment (D4 “refuse” row) is served by a tableau model engine over a built std::kripke carrier (World, Entity, iof, accessible, current). This is the genuine tier:modal backend. It is the one large build; the OE11xx refusal makes deferring it sound (loud refusal, never silent wrong). It is not “purely mechanical mechanization of well-understood math,” so it carries its own design and (when built) its own Lean obligations — it is out of scope for the Lean deferral that covers D3’s finite-frame reduction.

What does not change

• Truth4 stays four-valued. Both is genuine same-proposition contradiction (= no consistent global section), orthogonal to rival values.
• Federation default stays Paraconsistent (no-binder across). Enumerate is the new, additive, lossless peer; federation remains the lossy opt-in for disagreement detection.
• The <: DAG, the consistency policies, the world-assumption gates are untouched.

Decidability placement

• D1 enumerate + D2 reads + the decidable D3 translation: tier:closure (<: closure) + tier:recursive (stratified aggregates / NAF). Executable on the existing semi-naive engine.
• D4 “refuse” / D6: tier:modal. Refused until the engine lands.

Implementation plan (dependency-sorted)

• Phase A — the unblocking core. D1 binder (grammar + lowering + the enumerate readout keeping sid) + the Standpoint-typed column + D2 reads as ordinary forall/exists. End-to-end testable; delivers hold-the-rival-set + the qualitative floor with no engine.
• Phase B — soundness + mid-body. D4 frame-aware dispatch (discharge / refuse, killing the silent-wrong) + D3 standpoint-frame translation (reach relation + the box/diamond lowering). Requires D7 below.
• Phase C — the escape hatch. D6 tableau engine + std::kripke package.

D7 — Prerequisites surfaced by verification

• AtomIR::Modal frame recovery: determine the frame at lowering (where ctx.standpoint_id / the across set / “is inner a classifier atom” are available) and emit translated/​discharged ordinary AtomIR, so AtomIR::Modal survives only for the tableau-bound case. This avoids a wire/IR shape change.
• Query lowering order: thread the across set into the lowering context before body lowering (today it is extracted after). Derives already carry the enclosing standpoint via ctx.standpoint_id.
• Expose reach(s, s') (the precomputed <: ancestor closure) as a reasoning relation for D3.

Lean note

Per a one-time, explicitly-authorized deferral (this primitive is blocking a dependent project and D3’s reduction is the proven KR-2023 finite-frame result, not novel mathematics): the soundness proof of the D3 standpoint-frame discharge is deferred. The data-shape mirror that the oxc-protocol drift gate enforces is not deferred — any IR change stays in lockstep with the Lean @[language_interface] inductives. D6 (the model engine) is out of this deferral.

References

• Verified sources: spec/lean/Argon/Reasoning/{Modal,StaticDischarge}.lean, spec/lean/Argon/Decidability/Modal.lean, spec/lean/Argon/Standpoint/{Federation,Consistency,AFTEquivalence,Stratification}.lean, compiler/crates/oxc-runtime/src/lib.rs (query_derive_federated, materialize_predicates_for_standpoint), compiler/crates/oxc-oxbin/src/sections/standpoint_lattice.rs, spec/reference/src/semantics/decidability.md, spec/reference/src/semantics/standpoints-and-federation.md.
• Gómez-Álvarez & Rudolph (2021), Standpoint Logic (JELIA): polytime reduction to OWL 2 by reification.
• Gómez-Álvarez, Rudolph & Straß (2023), A Datalog reasoner for Standpoint-EL+ (KR): ~30 Datalog rules, PTIME; intractability boundaries (IJCAI 2023).
• Vennekens, Gilis & Denecker (2006), Splitting an Operator: stratified fixpoint over a DAG of strata.
• Belnap (1977); Denecker, Marek, Truszczyński (2000), Approximation Fixpoint Theory.