Quantifier Scope and Undefined Terms in Requirement Statements

A requirement written in a natural language sentence carries a logical form that the sentence does not display. “All users can see their orders” has at least four readings, and they differ in who is quantified, over what set, and with which modality. Reviewers approve the sentence because each of them reads a different one and none of the readings is obviously wrong.

The ambiguity is not a failure of care. It is structural: natural languages leave quantifier scope, quantifier domain, and the force of modal verbs implicit, and readers resolve them from context that the author never wrote down. Making the logical form explicit is the only reliable repair, and it is expensive enough that it should be reserved for the statements that will be implemented.

Four readings of one sentence

Take the sentence as a formula with three candidate quantifiers: over users, over orders, over time.

Reading one: for every user $u$, for every order $o$ belonging to $u$, $u$ can read $o$. This is the plain reading, and it is the one most authors intend.

Reading two: for every user $u$, there exists a set of orders visible to $u$, and that set includes $u$‘s own. Weaker: it does not require the user to be able to see each of their orders, only that the visible set is non-empty and contains at least one.

Reading three: there exists a user $u$ such that for every order $o$, $u$ can read $o$. This is an administrator, not a customer. The sentence is compatible with it, because “all users can see their orders” does not pin the quantifier order.

Reading four: for every user $u$ and every order $o$, if $o$ belongs to $u$ then $u$ can read $o$ — the same as reading one, but with the possessive read as a condition rather than a domain restriction. The difference appears when an order has no owner, or two owners: reading one quantifies over an empty set and is vacuously true, reading four has a defined truth value for the unowned case.

Only reading one and reading four differ in a way that a test can distinguish, and only under inputs the test suite probably does not contain. That is the characteristic shape of scope ambiguity: it survives review, survives testing, and surfaces when a user with a shared order or a deleted account exercises the edge.

Domain restriction is where the real question hides

The phrase “their orders” restricts the quantifier to orders belonging to the user. That restriction presupposes a relation — ownership — that the requirement never defines. Ownership could be the account that placed the order, the account that paid, the account currently responsible, or the set of accounts granted access.

Each choice produces a different system, and the difference is not cosmetic. If ownership means “placed”, a transferred order disappears from the original account and appears in the new one. If it means “granted access”, the original account keeps visibility after transfer. If it means “paid”, an order paid by a parent for a child is visible to the payer and invisible to the child, which is the opposite of what most people expect from the sentence.

The requirement does not contain an error. It contains an undefined term, and the term’s definition is a separate requirement that nobody wrote. This is why glossaries in requirements documents exist: not as vocabulary decoration, but because the domain predicates are the actual content, and a predicate used without a definition is a free variable.

The repair is mechanical once the term is noticed. Define owns(account, order) as a predicate over a stated relation, then restate the sentence in terms of it. The definition is longer than the sentence, and it is the part that determines behaviour.

Modality: can, must, and will

The modal verb in “can see” is doing work that is rarely examined. It may mean the capability exists — the interface permits the read and returns the data if asked. It may mean the system guarantees the read succeeds — no error, no timeout. It may mean the read is permitted by policy — the data is visible if the request is authorised.

These are three different requirements with three different implementations. Capability is satisfied by an endpoint that returns the data when the caller is authorised and an error otherwise. Guarantee requires availability and consistency properties that the endpoint alone does not provide. Permission requires an authorisation model, and the sentence says nothing about who else is denied.

RFC 2119 addresses exactly this problem for protocol documents by reserving MUST, SHOULD, MAY, and their negations, and by defining what each obliges. The convention exists because a sentence that uses “can” or “should” without a defined force is not actionable: an implementer cannot tell whether a deviation is a defect or a permitted variation. Requirements documents that adopt the convention gain a checkable property — every normative statement uses a reserved term — and lose the ability to write sentences whose force the author has not decided.

The loss is the point. A sentence whose force is undecided is a decision that has been deferred to whoever implements it, and that person will decide based on what is convenient.

Universal claims that are really existential

The most common scope error in the other direction is a universal claim that the author meant as an example. “The system supports exporting to CSV” reads as a capability claim: there exists a path by which a CSV export is produced. It is satisfied by an export that works for small tables and fails above a size limit, because the sentence quantifies over nothing.

The distinction is checkable if the statement is rewritten with its quantifiers exposed. “For every table, an export produces a file containing all rows” is a universal claim with a per-table obligation, and it forces the question of size limits. “There exists a table for which an export produces a file” is trivially true of any system with a test fixture.

Two rewrites make the difference visible, and the choice between them is a requirement, not a wording preference. A specification that contains only existential claims is satisfiable by almost any implementation, which is why specifications assembled from capability lists tend to be satisfiable and useless.

What formalisation buys and what it costs

Writing the statement in a formal notation removes the ambiguity, and the notation has to be chosen carefully: first-order logic over the domain predicates is expressive enough for most requirements and decidable only in fragments, which matters if the intent is to check the specification mechanically. A statement with quantifiers over unbounded collections is not decidable, and a checker will either time out or require bounds.

The cost is legibility. A formula with nested quantifiers is not readable by the people who must agree to the requirement, and a requirement that its stakeholders cannot read is a requirement that will be wrong in a way nobody catches. The compromise that works is to write the sentence in prose and the logical form beside it, and to treat disagreement between the two as the signal to stop: if the prose and the formula disagree, the author’s intent was not settled.

There is also a class of statement that formalisation cannot repair, because the ambiguity is in the domain rather than in the logic. “The report shows recent activity” has no quantifier problem; it has an undefined predicate, and no notation fixes it. The two failure modes need different responses — rewrite the logic, or define the term — and conflating them produces specifications that are formally precise about the wrong predicate.

The habit that pays is narrow: for each statement that will be implemented, name the quantifiers, name the domain of each, define every predicate used, and fix the force. Statements that will not be implemented can stay in prose. Where the statement turns out to be a policy over a fixed set of facts, the rewritten form usually lands directly in a decision table, whose columns make the case analysis explicit and whose coverage check catches the combinations the prose never enumerated. This is the same discipline that state machine specifications impose on transitions, applied to the sentences from which the transitions are derived, and it is a prerequisite for the kind of observational comparison described in refinement: a specification whose sentences have several readings has several trace sets, and no implementation refines all of them.