Modal operators: box and diamond

Area: Modal operators Teaches: the necessity (box) and possibility (diamond) operators in a rule body, and v0.1’s rigid-default discharge — over a rigid type, both box(P) and diamond(P) reduce to P at the current world. The classifier promotes a rule carrying a modal operator to tier:modal. Prerequisites: concepts, 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)); register 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. In v0.1 the semantics are rigid-default: for a rigid type — the UFO default, e.g. kind and struct — membership does not vary across worlds, so necessity and possibility both collapse to truth at the current world. This is the correct static-discharge answer for a rigid type, and conservative-degenerate for anti-rigid types until the Kripke evaluator lands.

What to read in governance.ar

One rigid type, wrapped in each operator by a separate rule:

pub type Citizen;

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

pub derive possibly_eligible(p) :- diamond(Citizen(p));

box(Citizen(p)) and diamond(Citizen(p)) both discharge to p: Citizen because Citizen is rigid. The classifier promotes both rules to tier:modal, and the build admits them.

A mutation supplies the citizens, and two queries read the modal derives:

pub mutate register(p: Citizen) {
    insert iof(p, Citizen);
}

pub query who_necessarily_eligible() -> necessarily_eligible;
pub query who_possibly_eligible() -> possibly_eligible;

Running it

The package ships no seed facts, so against the empty store both derives are empty:

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

Membership comes from register. Registering one citizen (alice) and reading the two queries shows the discharge:

query who_necessarily_eligible: 1 row(s)   → alice
query who_possibly_eligible:    1 row(s)   → alice

Both queries return exactly alice, the registered Citizen — and nothing else. That is the whole point of rigid-default discharge: over a rigid type, box and diamond agree, and they agree with plain membership. An unregistered individual matches neither rule, since there is no iof(_, Citizen) for the modal body to discharge against.

Honest caveats (what runs today)

• v0.1 is rigid-default. box and diamond collapse to current-world truth. The full Kripke evaluator — where the two operators genuinely diverge over anti-rigid types — is future work; today the surface is wired and the discharge is sound for rigid types.
• The package ships no demo.toml, so a bare ox derive reads the empty store. To reproduce the rows above, register 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 rigid-default box/diamond discharge — both operators matching the registered Citizen and nothing else — is pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs).