Aspects of Linear Logic in a Game called Wff-n-Proof
I’ve been writing some experiments in computer logic processing, when I thought of a certain game I ran across in my youth called Wff-n-Proof. Amazingly, this game is still around, as you can see from clicking the link, even though I am sure I hadn’t thought of it since the 1960’s or 70’s at the latest.
It’s a beautiful little game for teaching kids symbolic logic. You roll some dice that have symbols for propositions and symbols for combinators on them, then you try to make Well-Formed-Formulas (WFFs) by arranging the dice. That’s just the beginning, though, because you also learn rules of Inference for combining your WFFs, and there is a sequence of twenty-one games of increasing challenge until one arrives at the point where one has free use of a really broad collection of rules and conventions.
One attractive aspect of this game for my experiments is that the rules-of-the-game statement in the instruction manual is almost precise enough that one can write a computer simulation of the game effortlessly. A few things were slightly underspecified, and that would not be surprising for a game meant for manual play, not automatic play. However, the lacunae were so minor that the fixes are obvious. In particular, some of the rules of inference are non-deterministic, and simulating them in a computer requires additional information, outside the strict rules of the game, about how to handle such.
The game is based on the “CAKEN” subset of the Lukasievicz “Polish” notation for logic. The dice give you the symbols p, q, r, and s for propositions and the symbols C, A, K, E, and N for combinators. It’s by looking at one of the combinators, namely K for Konjunction that I noticed that the game has something of the Resource Interpretation of Linear Logic built in.
Generally, in the game, a WFF of the form Kpq means that our dice have given us an assertion that both p AND q are true, hence the Konjunction moniker for the combinator K. We are also given a rule of inference called Ko,for K-out, that allows us (by non-deterministic player choice) to deduce either p or q. One can then use p and q via another rule, called Ki for K-in, to re-deduce Kpq.
Now, what’s the tie-in to Resource Interpretation? Naturally, in a game about symbolic logic, we are not allowed to cross the boundary between interpretation and inference. We are NOT allowed to construct something as trivial as “both p and p are true”, that is, Kpp, from a mere statement that p is true. Even though this is completely obvious to us, it’s only so at the interpretation level: the rules of the game DO NOT permit you to construct Kpp unless you have rolled TWO ps on your proposition dice and a K on your combinator dice. Get that, TWO ps. Even using the rules of inference, to apply Ki to p and p, you have to apply Ko twice to Kpp to get two ps. There’s no way out of the fact that mentioning a proposition “uses it up” in a sense.
Isn’t that interesting? It’s as though the seeds for Linear Logic were already floating around this cute little game about Polish notation.