RFD-0018 — where clauses, unsafe blocks, modal operators — one mechanism per concern

Question

Argon needs to express structural constraints on concepts, escape hatches for full FOL, and modal axioms (necessity / possibility). Should each get its own dedicated syntax, or are there unifying mechanisms?

Decision

Structural constraints via where clauses. A concept’s body admits where { … } blocks containing the constraint expressions. There is no @requires decorator alongside where; one mechanism, structural goes in the concept body.

Group axiom declarations (disjoint, complete, partition) admit dedicated declaration forms when the constraint involves multiple concepts symmetrically. These compose with where for per-concept refinement.

FOL escape via unsafe { … } blocks. When a constraint can’t be expressed within the structural / closure / recursive tiers, an unsafe logic { … } block lifts to tier:fol (RFD-0004). Inside an unsafe block, the full FOL expression grammar is admitted; the block’s body inherits the same expression grammar (RFD-0005) — no new syntax. The block annotation declares the expressivity cost.

Modal axioms via box() / diamond(). Necessity (box(P) — “in every accessible world, P”) and possibility (diamond(P) — “in some accessible world, P”) are first-class operators in the language. Modal axioms compose with the rest of the expression grammar; no separate modal sublanguage.

Rationale

One mechanism per concern reduces surface area. Multiple decorators that did almost-the-same-thing produced “which one do I use here” questions. Picking where for structural constraints and reserving decorators for orthogonal concerns (theorem marking, transitivity) makes the choice mechanical.

unsafe is the right metaphor. Like Rust’s unsafe, the block does not change syntax — it changes the obligations of the author. An unsafe logic block admits expressions whose evaluation cost may be unbounded or undecidable; the author is acknowledging that and accepting the responsibility.

Modal operators as first-class. Modal logic is too useful to bury behind a sublanguage barrier. box() and diamond() integrate with rule bodies, query bodies, mutation preconditions — anywhere a propositional expression appears. The compiler enforces modal axiom rules at tier:modal.

Group axioms admit dedicated forms when the constraint is symmetric. disjoint(A, B, C) is clearer than three pairwise where clauses; the dedicated form is a sugar that lowers to the equivalent where constraints. Structural sugar is a feature, not a leak.

Consequences

• Concept declarations admit where { … } blocks; no @requires decorator.
• disjoint, complete, partition are reserved declaration-form keywords for group axioms.
• unsafe logic { … } is the FOL escape; the block’s tier is tier:fol.
• box() and diamond() are reserved operators; modal axioms compose with the rest of the grammar.
• The decidability classifier auto-classifies expressions into the appropriate tier; expressions outside unsafe blocks that exceed the surrounding tier produce OE0604 TierViolation.