An alert rule reads 'latency of service s exceeds the budget' with s never quantified: what has it actually asserted?

## Bound, free, and what a formula without quantifiers is In a quantified sentence, each variable is either **bound** or **free**: - A variable is **bound** when it falls inside the **scope** of a quantifier that ranges over it - the `j` in *for every job `j`, `acknowledged(j)`*. - A variable is **free** when nothing binds it - the `s` in *`latency(s)` exceeds the budget*. The distinction decides what kind of object you are holding. A formula with no free variables is a **proposition**: it is true or false outright, and you can put it in a specification and argue about it. A formula with a free variable is an **open formula** - a **predicate** - which has a truth value only relative to an assignment of a value to that variable. `latency(s) > budget` is true of some services and false of others; on its own it is neither. So the honest answer about the alert rule is that it has asserted a property, not a claim. To turn it into a claim you must do one of three things, and they are not interchangeable: 1. **Bind it universally** - *for every service `s`, `latency(s) > budget`* - which is true only in the disastrous case where nothing is within budget. 2. **Bind it existentially** - *for some service `s`, `latency(s) > budget`* - which is what an alert almost always means: fire when at least one service breaches. 3. **Instantiate it** - fix `s` to one named service, giving a claim about that service alone. The gap between (1) and (2) is the whole risk. They differ in exactly the way a universal and an existential always differ - one is refuted by a single witness, the other confirmed by one - so a rule that leaves `s` free leaves the reader to guess which system behaviour was meant. ## Why conventions do not rescue it Mathematical writing often reads a standalone formula with free variables as **implicitly universally quantified** - its *universal closure*. That convention is real and useful, but relying on it in a specification has a cost: the sentence now means whatever the reader's convention says, and a reader who expects the existential reading (the natural one for an alert) gets the opposite claim. The fix is not to pick a convention; the fix is to write the quantifier. ## Scope, shadowing, and renaming A few further properties of bound variables come up when specifications get nested: | Property | Statement | Consequence | |---|---|---| | Scope | a quantifier binds its variable only inside its own body | the same name outside that body is a different variable | | Renaming | a bound variable's name carries no meaning | *for every job `j`* and *for every job `k`* say the same thing, provided the new name does not collide with one already in use | | Shadowing | an inner quantifier may reuse an outer name | the inner one wins inside its body, and the outer variable becomes unreachable there - a common source of misreading | | Relativity | freeness is relative to the formula you consider | `j` is free in *there is a worker who handled `j`* and bound in *for every job `j`, there is a worker who handled `j`* | That last row is worth dwelling on, because it explains a frequent confusion: people ask whether a variable "is" free as though it were an intrinsic property of the symbol. It is a property of the symbol **in a given formula**. A subformula quoted out of its enclosing quantifier acquires free variables that the whole sentence did not have - which is exactly what happens when someone copies the inner half of a specification sentence into a review comment and it stops meaning anything definite. ## What to do about it in practice - When a written condition mentions a name, ask **what binds it**. If nothing does, the condition is not yet a claim. - State the **domain** along with the quantifier: *for every service in the current deployment* rather than *for every service*, since an unstated domain is the second half of the same problem. - Be suspicious of a sentence whose meaning changes when you read it aloud with *every* and then with *some*. If both readings are grammatical, the quantifier is missing rather than obvious. - When quoting part of a specification, carry its binder with it or say explicitly what the loose variable ranges over. The practical value of the free/bound distinction is not terminological. It is a fast test for a sentence that looks like a specification, passes review because everyone reads it their own way, and turns out to have committed to nothing at all.