## WFF ‘N Proof, a mathematical-logic game

“WFF ‘N Proof, the Game of Modern Logic”, is a game that I had had in my childhood, though I now only have its rulebook. A WFF (“woof”) is a well-formed formula, one that is syntactically correct, and in the game, one creates proofs with inference rules. The game has dice with operation and variable names on them, and one tries to find WFF’s and proofs that fit what is on the dice. The game also includes an hourglass for timed play.

It was created by Layman Allen in 1962, and he has also created On-Sets, on set theory, and Equations, on arithmetic, both played much like WFF ‘N Proof.

I wish that I could recommend WFF ‘N Proof, but it has several deficiencies.

• It uses a prefix representation for its binary operators, (and) p q, with no attempt to relate it to the more usual infix form, p (and) q.
• It does not use the logical constants (true) and (false), and it does not have truth tables, tables of output values for input values (arguments).
• It does not name the operator properties that it has proofs of, like (and) and (or) being commutative and associative.

After the fold, I will describe the formalism in WFF ‘N Proof in more detail.

The first issue is where to write an operation symbol amidst its operands or arguments, what it works on. There are three possibilities:

• Prefix: op x y
• Infix: x op y
• Suffix: x y op

For a unary operation like negation, infix notation may mean overwriting the operand symbol (slash) or above it (bar). Also, suffix notation is often called postfix notation.

Arithmetic and logical binary operations are usually written in infix form: x + y, x (and) y, though functions are usually written in prefix fashion: f(x,y). But in the early twentieth century, Polish mathematician Jan Łukasiewicz introduced prefix notation, and that is why it is sometimes called Lukasiewicz notation or Polish notation. Hewlett-Packard calculations use suffix notation, and this is why it is called reverse-Polish notation.

WFF ‘N Proof uses prefix notation, and it uses these symbols for logical operations:

• N: negation (not)
• R: repetition and reiteration (using something previously stated)
• K: conjunction (and)
• A: disjunction (or)
• C: implication
• E: equivalence (==)

WFF ‘N Proof uses inference rules, with operation names suffixed with o (out) or i (in). Here they are, in the order in the rulebook that they are introduced:

• Ko: Kpq -> p, q
• Ki: p, q -> Kpq
• Co: Cpq, p -> q
• Ci: (p -> q) -> Cpq
• R: p -> (q -> p)
• Ao: Apq, (p -> r), (q -> r) -> r
• Ai: p -> Apq, Aqp
• No: (Np -> q, Nq) -> p
• Ni: (p -> q, Nq) -> Np
• Eo: Epq -> Cpq, Cqp
• Ei: Cpq, Cqp -> Epq

Here is a proof of the property that conjunction (and) is commutative:

• 1. Kpq … s — stipulation
• 2. p … Ko 1
• 3. q … Ko 1
• 4. Kqp … Ki 3, 2

Thus proving that Kpq implies Kqp, Kpq -> Kqp. Renaming the variables gives Kqp -> Kpq, thus showing that Kpq and Kqp are equivalent.

For disjunction (or), the proof is more complicated:

• 1. Apq … s
• 2a. p … s
• 2b. Aqp … Ai 2a
• 3a. q … s
• 3b. Aqp … Ai 3a
• 4. Aqp … Ao 1, 2, 3

As before, renaming variables completes the proof.

Both proofs are in the rulebook, though they are not named. Proofs of other properties, like associativity, distributivity, double negation, and De Morgan’s inversion laws, are also in the book, and these properties are not named either.

So I find WFF ‘N Proof very disappointing.