Separation Logic and Forall
It has been confusing for me to tell the difference between “all” and “any” as an English learner. But at least in this scenario, I am confident they are different:
“Given one ticket, you can redeem for (all the items)/(any item) in the inventory. “
If we use “all”, then we should be able to clear the inventory, while using “any” only grants one item.
On the other hand, in logic, we call the universal quantifier “∀”, either “for all” or “for any”. Then, for that English sentence, a naive way of expressing it could be
“ticket → ∀x ∈ Inventory, Redeem(x)”,
which does not quite specify how many we can redeem, unless we provide a more concrete interpretation of “ticket” and “Redeem”.
However, if we rewrite it using the magic wand
“ticket -∗ ∀x ∈ Inventory, Redeem(x)”,
then it looks closer to the “any” case.