Modal operators: box

Area: Modal operators Teaches: the necessity (box) operator in a rule body, and the fixed-introduction discharge — over a type whose introducing metatype is fixed, box(P) reduces to P at the current world (box_fixed_discharge). The classifier promotes a rule carrying a modal operator to tier:modal. Prerequisites: concepts, metatypes (the fixed modifier), and derive rule bodies (see first-class relations). Run: ox build examples/modal_box_diamond && ox derive examples/modal_box_diamond necessarily_eligible — this reads the empty store (0 tuple(s)); construct a citizen first to see the discharge (see Running it).

Modal logic distinguishes what must hold from what may hold. box(P) reads “necessarily P” — P at every accessible world; diamond(P) reads “possibly P” — P at some accessible world. Argon exposes both as operators usable inside a rule body.

The engine performs exactly one sound reduction: the forward-rigidity discharge box(x : T) → x : T when T is introduced by a fixed metatype. Fixed classification is decided at construction and never changes, so a fixed-member is a member at every accessible world — necessity and plain membership coincide. Everything else is refused (OE1104) rather than silently stripped to the inner atom (which would be a wrong answer for anti-rigid or dynamic classification):

• diamond is not discharged, even over a fixed type. Under the open-world assumption a current non-member could be constructed into the fixed type in a reachable world, so diamond(x:T) can hold where x:T is currently false — reducing it to x:T would under-derive. There is no diamond_fixed_discharge theorem, so diamond is refused.
• A box over a non-fixed type (whose membership can change across worlds), a box(not (x:T)) (a fixed type discharges necessary membership, never necessary non-membership — the polarity is asymmetric), and any standpoint-frame modal are all refused too.

The standpoint-frame translation and the tableau model engine over a Kripke carrier are future work; until they land the refusal holds the place soundly. This example therefore demonstrates the one case that runs today: box over a fixed type.

What to read in governance.ar

One fixed-introduced (frame-rigid) type, wrapped in box:

pub fixed metatype status = { };

pub status Citizen;

pub derive necessarily_eligible(p) :- box(Citizen(p));

box(Citizen(p)) discharges to p: Citizen because Citizen is introduced by the fixed metatype status. The classifier promotes the rule to tier:modal, and the build admits it. (A diamond(Citizen(p)) rule would be refused with OE1104.)

A mutation mints the citizens, and a query reads the modal derive:

pub mutate register() -> Citizen {
    let c = insert Citizen { };
    c
}

pub query who_necessarily_eligible() -> necessarily_eligible;

Because Citizen is fixed-introduced, membership is decided at construction — register constructs a citizen (an insert iof(p, Citizen) re-classification would be refused, OE0234). That is exactly what makes the discharge sound: a citizen is a citizen at every accessible world.

Running it

The package ships no seed facts, so against the empty store the derive is empty:

$ ox derive examples/modal_box_diamond necessarily_eligible
derive(necessarily_eligible): 0 tuple(s)

Citizens come from register. Constructing two citizens and reading the query shows the discharge:

query who_necessarily_eligible: 2 row(s)

The query returns exactly the constructed citizens — and nothing else. That is the whole point of the fixed-introduction discharge: over a frame-rigid type, box agrees with plain membership. An individual that was never constructed as a citizen does not match, since there is no iof(_, Citizen) for the modal body to discharge against.

Honest caveats (what runs today)

• Only box over a fixed-introduced type discharges. A diamond (any frame), a box over a non-fixed type, a box(not (x:T)), or a standpoint-frame modal is refused (OE1104) rather than stripped — the full Kripke / standpoint-frame evaluator, where the operators genuinely diverge, is future work.
• The package ships no demo.toml, so a bare ox derive reads the empty store. To reproduce the rows above, construct a citizen first (the corpus test drives governance::register programmatically; from the CLI, a one-line scenario file with a [[mutate]] entry for governance::register does the same via ox run-scenario).

This example is compiled and run in CI; the fixed-introduction box discharge — matching the constructed citizens and nothing else — is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Modal operators (`box` / `diamond`, spec §11.2).

mod governance;

governance.ar

//! Modal operators (`box`, spec §11.2).
//!
//! The necessity operator `box` over a Kripke frame. The engine
//! performs the sound forward-rigidity discharge `box(x : T) → x : T`
//! ONLY when `T` is introduced by a `fixed` metatype (§10.2: a
//! fixed-member is a member at every accessible world, so `box φ` and
//! `φ` coincide) — this is `box_fixed_discharge`, the only proven
//! reduction.
//!
//! `diamond` is NOT discharged, even over a `fixed` type: under OWA a
//! current non-member could be constructed into the fixed type in a
//! reachable world, so `diamond(x:T)` can hold where `x:T` is false —
//! reducing it to `x:T` would under-derive. So `diamond`, a `box`
//! over a non-`fixed` type, a `box(not (x:T))`, and any
//! standpoint-frame modal are all refused with OE1104 rather than
//! silently stripped to the inner atom (stripping would be a wrong
//! answer for anti-rigid / dynamic classification).
//!
//! `Citizen` is introduced by the `fixed` metatype `status`, so a
//! citizen's membership is decided at construction and never changes
//! — that is exactly what makes the `box` discharge sound.
//!
//! Demonstrates:
//!   * `box(Citizen(p))` in a rule body — necessity over a
//!     fixed-introduced (frame-rigid) type. Discharges to
//!     `p: Citizen` (always-true at every accessible world).
//!   * The classifier promotes the rule to `tier:modal`;
//!     the build admits it after the frame-aware dispatch.
//!
//! Expected runtime behavior:
//!   a constructed citizen → necessarily_eligible
//!   any other individual  → not (no matching iof)

pub fixed metatype status = { };

pub status Citizen;

// ANCHOR: modal
pub derive necessarily_eligible(p) :- box(Citizen(p));
// ANCHOR_END: modal
// `Citizen` is `fixed`-introduced: membership is decided AT
// CONSTRUCTION and never re-classified (`insert iof(p, Citizen)`
// would be the refused re-classification, OE0234). A citizen is
// minted by constructing one; the constructed individual is returned
// so a caller can read it back.
pub mutate register() -> Citizen {
    let c = insert Citizen { };
    c
}

pub query who_necessarily_eligible() -> necessarily_eligible;