Standpoints and modal operators

Standpoint declaration and federation

standpoint-decl ::= attribute* 'pub'? 'standpoint' Ident ('<:' TypeExpr (',' …)*)?
                     '{' mod-item* '}'

pub standpoint USFederalTax {
    pub type TaxableIncome <: Money;
    pub derive owes_tax(p: Person) :- p.income: TaxableIncome, p.income > 0;
}

pub standpoint California <: USFederalTax {
    pub derive state_owes_tax(p: Person) :- /* … */;
}

pub standpoint ContestedClaims { /* … */ }

A standpoint is a namespace-bearing module: items declared inside are accessible as StandpointName::ItemName (e.g., USFederalTax::owes_tax). The <: relation between standpoints declares lattice membership (federation ancestor for across [...] queries), not namespace inheritance — a child standpoint does not automatically see the parent’s items; explicit use is required to bring items into scope. Cross-standpoint federation via the across [...] annotation on queries; results may carry Truth4 values.

Nested standpoint declarations are not admitted — lattice edges come from <:, not from textual containment. Submodules (mod) and impl blocks inside a standpoint are permitted.

Federation conflict policy is chosen per query, not per standpoint: a federated across [...] query is paraconsistent by default — disagreement surfaces as Both (see truth values) — and may request strict projection. Conflict policy is a per-query projection, not a standpoint-level declaration.

Visibility composition. Facts are scoped by where they are asserted. A fact/not_fact declared inside a standpoint s { … } block is local to s; one declared at file/module scope, outside any standpoint block, sits in the DEFAULT (unscoped) layer. The two compose by the sheaf reading (Sheaf-theoretic semantics for standpoint federation):

• The DEFAULT layer restricts into every view. An unscoped assertion is visible to an unfederated query, to every standpoint-scoped query, and to every standpoint in an across [...] federation — it is the broadest perspective, and the sheaf restriction maps carry it into every stalk.
• A standpoint-scoped fact is invisible outside its standpoint. It does not appear in an unfederated (unscoped) query, nor in a query scoped to a different standpoint. Reading a scoped fact requires explicitly selecting its standpoint — via across [...], box/diamond (Modal operators), or a bridge rule (Bridge rules).

So an unfederated query (pub query q() -> P;) reads exactly the DEFAULT layer; a single-standpoint federation (across [s]) reads the DEFAULT layer unioned with s’s own facts; a multi-standpoint federation info-joins those per-standpoint views (Sheaf-theoretic semantics for standpoint federation). Derive rules, checks, and the mutation delta-guard all evaluate over the DEFAULT-layer (base) view — a scoped fact never silently becomes global truth. A federated query that names a standpoint with no declaration is refused (OE1103 UndeclaredStandpointInAcross) rather than contributing an empty extent that would mask the typo. Mechanized at spec/lean/Argon/Standpoint/Visibility.lean: view_of_base_eq_default_layer (base = DEFAULT layer), scoped_view_eq_default_union_own (scoped = DEFAULT ∪ own standpoint), default_visible_everywhere, scoped_invisible_to_base, and scoped_invisible_to_other.

Modal operators

box(P) and diamond(P) are rule atoms (Rule-atom grammar) admitted at tier:modal. They are interpreted over a Kripke frame; the frame is determined by the surrounding context.

Frames. Argon recognizes two intrinsic frames:

• Standpoint frame. Worlds are standpoints; the accessibility relation is the reflexive-transitive closure of <: over the standpoints in scope (extended by the explicit set of any enclosing across [...] clause). box(P) at standpoint s holds iff P holds at every s' reachable from s along the frame.
• Classification frame. Worlds are configurations in which an individual exists (store states reachable by mutations). A type introduced by a fixed metatype (metatype, RFD 0027 D6) carries forward rigidity: once an individual is a member, the mutate mutation gate preserves that membership forward along accessibility (Argon.Runtime.ModifierGates.runMutation_fixed_iof_constant). This is one-directional, not two-way constancy — a current non-member can still later be constructed into a fixed type, so fixed pins membership going forward but says nothing about future gains. A type introduced by an unmodified (dynamic) metatype carries no such guarantee. This is the standard Guizzardi/UFO modal characterization of rigidity, realized operationally by the ontology-neutral fixed bit rather than by reading any vocabulary’s rigidity axis.

diamond(P) is dual: it holds when P holds in at least one accessible world.

Static discharge. When P is a positive type-classification atom over a target introduced by a fixed metatype, forward rigidity preserves membership across accessible worlds and the elaborator can discharge the modal at compile time without consulting a reasoner (Argon.Reasoning.StaticDischarge.box_fixed_discharge). The discharge is polarity-asymmetric: forward rigidity grips box(x : T) but gives no grip on the negation box(¬(x : T)), since a current non-member may still be constructed into the type later (Argon.Reasoning.StaticDischarge.isRigidIn_does_not_discharge_box_neg).

Atoms that survive static discharge are routed to a modal reasoner over the std::kripke carrier; the choice of backend (tableau, resolution, bounded model-checking) is implementation-defined.

std::kripke. Exported from the stdlib for explicit modal modeling — e.g., writing forall w: World where accessible(current, w), P@w inside unsafe logic { }. The carrier is minimal:

// in std::kripke
pub struct World;
pub struct Entity;
pub fn iof(e: Entity, t: Top, w: World) -> Bool;            // instance-of-in-world
pub fn accessible(w1: World, w2: World) -> Bool;            // frame accessibility
pub fn current() -> World;                                   // the current world

The surface operators box(P) and diamond(P) are syntactic forms — not function calls — and desugar to FOL over World:

Where P@w denotes the rule atom P evaluated at world w (i.e., relativized to w’s extension). Modelers using only the surface operators need not import std::kripke directly; the desugaring threads through the elaborator. There are no Box / Diamond runtime functions — modal operators reduce to quantification over worlds.

Federation interaction. Inside a query annotated across [s₁, s₂, …], the standpoint frame is extended to the named set; box(P) reads “P holds in every listed standpoint” and may return Both, Can, or Not per truth values when the standpoints disagree. Classification-frame box/diamond atoms compose with federation by being evaluated independently at each listed standpoint, then info-joined via the FDE lattice.

Lowering. box(P) and diamond(P) lower to AtomIR::Modal and classify at tier:modal. Cross-nesting a modal with a temporal operator is refused by the tier classifier. examples/modal_box_diamond.ar exercises both operators end-to-end.

Bridge rules

Bridge rules thread information explicitly between standpoints. Where across [...] composes standpoints lattice-wise (FDE info-join over <:), a bridge rule is a directional, named, typed inference that moves a conclusion from one standpoint to another, optionally applying a domain mapping.

Status. pub bridge is refused at ox check / ox build with OE1102 (audit doc-04 / issue #151). Bridge rules parse, lower to wire events, resolve, and pass well-formedness checks — but the federation fixpoint never fires them, so a built artifact’s bridge bodies would silently never contribute to their target standpoint. Rather than ship that inert surface, a bridge declaration is refused loudly; model the cross-standpoint inference with an explicit derive / pub fact for now. Bridge evaluation is the post-stable flagship standpoint deliverable: the parse / lower / wire / decode surface is retained intact (Module::bridges_targeting, the BridgeDecl codec) so the work resumes without a grammar or wire-format change. The semantics below is the committed design.

bridge-decl ::= attribute* 'pub'? 'bridge' Ident
                  '(' standpoint-ref '->' standpoint-ref ')'
                  '{' bridge-rule (';' bridge-rule)* ';'? '}'
bridge-rule ::= rule-body '=>' bridge-head
bridge-head ::= predicate-call                           // direct assertion into target
             |  predicate-call 'mapping' mapping-clause  // with domain map
mapping-clause ::= '{' (Ident '=' expr (',' …)*)? '}'    // src-var ↦ dst-expr
standpoint-ref ::= path                                  // resolves to a standpoint

pub bridge USCitizens(US::Tax -> International::Legal) {
    Person(p), p.citizenship == "US"
        => LegalEntity(q) mapping { q.jurisdiction = "US", q.person_ref = p };
    Person(p), p.passport != null
        => Verified(p);
}

The -> between standpoint references in the bridge head encodes the direction; existing -> operator (function return arrow) is reused with no new lexer token.

Directionality (key property). A bridge from s₁ to s₂ does not imply a bridge from s₂ to s₁. The asymmetry is what makes bridges different from equality / equivalence axioms; without it, bridge composition would collapse standpoints and destroy their contextual scoping. This is the standard discipline across DFOL (Ghidini-Serafini), DDL / C-OWL (Borgida-Serafini-Bouquet), and MCS (Brewka-Eiter) — see the vault notes on bridge-rule semantics for the comparative landscape.

Body and head. The rule body uses the standard rule-atom grammar (Rule-atom grammar) evaluated at the source standpoint. The head is a predicate call evaluated at the target standpoint. If source and target have different domains (e.g., a tax-jurisdiction Person vs. an international-law LegalEntity), an explicit mapping { … } clause specifies how source variables map to target-domain values; without a mapping clause, the bridge is identity (source variable = target argument).

Negation-as-failure in bridge bodies. Bridge bodies admit NAF (not atom) over the source standpoint’s predicates — matching the MCS form. The bridge graph (nodes = standpoints; edges = bridges) must be stratified for the federation fixpoint to be unique; cycles in the bridge graph emit OE1101 BridgeCycle.

Composition with across [...]. A query annotated across [s₁, s₂] composes lattice federation (via <:) and any bridges between s₁ and s₂ in scope. Both contributions are info-joined via the FDE lattice; conflicts surface as Both per truth values.

Mechanization. The standpoint-frame sheaf semantics (Sheaf-theoretic semantics for standpoint federation) treats bridges as restriction maps on the perspectival sheaf — see that section. Diagnostic codes for malformed bridges live in the OE11xx range (Standpoints / perspectival config).

Bridges under temporal extent (Temporal substrate). When bridges cross modules with bitemporal extent, the substrate admits only temporal-uniform bridges at tier: recursive: a bridge rule consults facts only at the same valid-time at which it fires. Bridges that consult facts at different times (bridge m s t reading s _ t' with $t’ \ne t$) require tier: fol and an explicit temporal-bridge-monotonicity axiom in the module’s prelude. The sheaf-equivalence theorems of Sheaf-theoretic semantics for standpoint federation lift pointwise under temporal-uniform bridges with no new axioms; non-uniform bridges require a new axiom and are out of the conservativity envelope. Diagnostic: OE0720 NonUniformBridgeRefused. Mechanized at spec/lean/Argon/Locality/Temporal.lean (sheaf_equivalence_bitemporal_uniform).

Sheaf-theoretic semantics for standpoint federation

The standpoint lattice carries a sheaf-theoretic semantics — the formal grounding of why across [...] federation, bridge rules (Bridge rules), and box/diamond modal operators all compose coherently.

The sheaf. Treat the standpoint lattice as a base for a Grothendieck topology: open sets are downward-closed subsets of the <: lattice. The perspectival sheaf 𝓕 assigns to each open set U a stalk 𝓕(U) — the local knowledge (set of derivable facts, three-valued atoms, evidence accumulations) available to the standpoints in U. Restriction maps 𝓕(U) → 𝓕(V) for V ⊆ U encode how broader perspectives specialize to narrower ones; explicit bridge rules (Bridge rules) lift to additional restriction maps wherever the bridge graph reaches.

Substrate theorems. The correspondence is proved over a finite model at spec/lean/Argon/Locality/SheafEquivalence.lean — no axioms, no sorry: bottom_up_is_equilibrium, equilibrium_is_global_section, and equilibrium_is_minimal_section. Stated informally: the bottom-up evaluation of the federated standpoint system produces an MCS-style equilibrium, and that equilibrium is a minimal global section of the perspectival sheaf. The full categorical construction — a genuine Grothendieck topology with general restriction maps — is open research (it would unify two independent formalizations of perspectival reasoning; see the vault note “Topology of Understanding”). The finite-model theorems are the substrate commitment.

Consequence (H¹ interpretation). When across [s₁, s₂] yields Both(a, b) (the FDE conflict outcome), the first cohomology H¹(𝓕) carries a non-trivial generator. The two witnesses a, b are cohomologically distinct — they witness an irreducible perspectival disagreement that no global section can unify. This is the formal content behind the #[consistency(paraconsistent)] policy: the substrate makes the disagreement explicit rather than collapsing it.

Consequence (sheaf cohomology as diagnostics). Future tooling may surface H¹(𝓕) generators as a diagnostic class — “your federation disagreement is reducible (cohomologous to zero, fixable by a bridge rule) or irreducible (a non-trivial cohomology generator, requiring paraconsistent acceptance).” This is research-grade; the substrate axioms are the commitment.

Lift under bitemporal extent. When the standpoint federation runs over modules with bitemporal extent (Temporal substrate), the three sheaf-equivalence theorems lift pointwise without new axioms — provided bridges are temporal-uniform (Bridge rules). The bitemporal BeliefAssignment, BridgeEval, and LocalFixpoint become time-indexed functions; at each time slice, the canonical theorem applies. Mechanized at spec/lean/Argon/Locality/Temporal.lean (bottom_up_is_equilibrium_bitemporal, equilibrium_is_global_section_bitemporal, equilibrium_is_minimal_section_bitemporal, bundled as sheaf_equivalence_bitemporal_uniform). Non-uniform bridges (consulting facts at different VTs) require a new temporal-bridge-monotonicity axiom and are out of the conservativity envelope.