Post

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.

This post is licensed under CC BY 4.0 by the author.