Results 1 to 8 of 8

Thread: WFF 'N Proof -- mathematical-logic game

  1. #1
    Join Date
    Nov 2001
    Posts
    789

    WFF 'N Proof -- mathematical-logic game

    "WFF 'N Proof: The Game of Modern Logic" -- I found its rulebook when I recently did some housecleaning.

    In summary, I wish I could recommend it, but I can't. That is because (1) it uses a formalism very different from the more usual presentations of symbolic logic and Boolean algebra, and (2) it does not try to relate its formalism to those formalisms.

    WFF is short for Well-Formed Formula, and in Backus-Naur form, it is given by
    <WFF> ::= <primitive> | <unary operation> | <binary operation>
    <unary operation> ::= <unary operator> <WFF>
    <unary operator> ::= N
    <binary operation> ::= <binary operator> <WFF> <WFF>
    <binary operator>::= C | A | K | E

    The operators are
    N = negation (not)
    C = implication
    A = disjunction (or)
    K = conjunction (and)
    E = equivalence (==)
    There is no exclusive or in the game, but that is simply negation of equivalence.

    They are all prefixes, in a notation sometimes called Lukasiewicz notation or Polish notation, after early-20th-cy. mathematical logician Jan Lukasiewicz. That is where "reverse Polish" gets its name -- it is suffix notation. The usual way of writing mathematical-logic formulas is prefix notation for negation and infix notation for the others: p and q, etc.

    There is no discussion of truth tables in the game. These are tables of returned results for the range of function arguments. Thus, for "and", the truth table is
    - F T
    F F F
    T F T
    T = True, F = False

    The operators have these inference rules, where o = out and i = in:
    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

    R is reiteration and repetition, a convenience in proofs.

  2. #2
    Join Date
    Nov 2001
    Posts
    789
    The rulebook has proofs of several properties without naming those properties.

    K: "and"

    K is commutative:
    1. Kpq ... s -- stipulation
    2. p ... Ko 1
    3. q ... Ko 1
    4. Kqp ... Ki 3, 2
    (does both directions)

    K is associative:
    1. K-Kpq-r ... s
    2. Kpq ... Ko 1
    3. p ... Ko 2
    4. q ... Ko 2
    5. r ... Ko 1
    6. Kqr ... Ki 4, 5
    7. K-p-Kqr ... Ki 3, 6
    (commutativity gives the reverse direction)

    K is idempotent (args the same -> that arg):
    1. Kpp ... s
    2. p ... Ko 1 (both args)
    -
    1. p ... s
    2. Kpp ... Ki 1, 1

  3. #3
    Join Date
    Nov 2001
    Posts
    789
    A: "or"

    A is commutative:
    1. Apq ... s
    2a. p ... s
    2b. Aqp ... Ai 2a
    3a. q ... s
    3b. Aqp ... Ai 3a
    4. Aqp ... Ao 1, 2, 3
    (does both directions)

    A is associative:
    1. A-Apq-r ... s
    2a. Apq ... s
    2b1. p ... s
    2b2. A-p-Aqr ... Ai 2b1
    2c1. q ... s
    2c2. Aqr ... Ai 2c1
    2c3. A-p-Aqr ... Ai 2c2
    2d. A-p-Aqr ... Ao 2a 2b 2c
    3a. r ... s
    3b. Aqr ... Ai 3a
    3c. A-p-Aqr ... Ai 3b
    4. A-p-Aqr ... Ao 1 2 3
    (commutativity gives the reverse direction)

    A is idempotent:
    1. App ... s
    2a. p ... s
    2b. p ... R 2a
    3a. p ... s
    3b. p ... R 3a
    4. p ... Ao 1 2 3
    -
    1. p ... s
    2. App ... Ai 1

  4. #4
    Join Date
    Jan 2002
    Location
    The Valley of the Sun
    Posts
    9,536
    I bought that game in the 1970's but never played it. I might still have it around here somewhere.

  5. #5
    Join Date
    Nov 2001
    Posts
    789
    It had an hourglass and some dice. The dice came in two colors, red and blue, and each set had some capital-letter dice (C, A, K, E, N, R) and some small-letter ones (p, q, r, s, I forget the rest). One rolls the dice and then decides whether each roll has parts of statements and/or proofs.

    Layman Allen, the game's creator, had also created some similar mathematical games, On-Sets and Equations, both played much like it. However, On-Sets and Equations both use familiar formulations of their subject matter.

    WFF N Proof Academic Games Leagues of America -- mathematical logic
    On-Sets Academic Games Leagues of America -- set theory
    Equations Academic Games Leagues of America -- arithmetic
    LinguiSHTIK Academic Games Leagues of America -- parts of speech and grammar rules
    Presidents Academic Games Leagues of America -- US ones
    Propaganda Academic Games Leagues of America -- bad arguments and how to recognize them
    Theme Academic Games Leagues of America -- research various historical issues and answer questions about them
    Current Events Academic Games Leagues of America -- do that with current events

    This organization sponsors tournaments in these games: Academic Games Leagues of America AGLOA | Promoting Excellence Through Academic Competition

  6. #6
    Join Date
    Jan 2002
    Location
    The Valley of the Sun
    Posts
    9,536
    In the copy I got, the dice were protected by a sheet of foam rubber with holes in it for the dice. Decades later the foam rubber crumbled when I touched it. Now I can't find it at all, but I should still have it.

  7. #7
    Join Date
    Nov 2001
    Posts
    789
    I found that out also -- that foam plastic disintegrated.

    I'm not Layman Allen, but if I was like him, I'd make a Boolean-algebra version of WFF 'N Proof -- something like Equations or On-Sets.

    Boolean algebra? We start with its two variable values:
    True = T = 1, False = F = 0

    Also its main operations: negation (not), conjunction (and), disjunction (or), implication (->), and equivalence (==).
    Code:
    not   and     or      ->      =
    . .   . F T   . F T   . F T   . F T
    F T   F F F   F F T   F T T   F T F
    T F   T F T   T T T   T F T   T F T
    One can define the last two in terms of the first three:
    x -> y is (not x) or y
    x = y is (x and y) or ((not x) and (not y)) is (x or (not y)) and ((not x) or y)

    There are lots of interesting interrelationships between negation, conjunction, and disjunction (not, and, or), and they are easy to prove using these operations' truth tables.

    Commutativity: x and y = y and x ... x or y = y or x
    Associativity: x and (y and z) = (x and y) and z ... x or (y or z) = (x or y) or z
    Like addition and multiplication, conjunction and disjunction can be expressed in multiargument, orderless fashion

    Distributivity: x and (y or z) = (x and y) or (y and z) ... x or (y and z) = (x or y) and (x or z)
    Both operations are distributive over each other, more than what one gets with arithmetic.

    Identity: T and x = x ... F or x = x
    Zero or Annihilator: F and x = F ... T or x = T
    While both addition and multiplication have identities, only multiplication has a zero.

    Idempotence: x and x = x or x = x
    Absorption: x and (x or y) = x or (x and y) = x

    Introducing negation, it has a property familiar from arithmetic:
    Involution (self-undoing): not (not x) = x

    Non-contradiction: x and (not x) = F (both cannot be true)
    Excluded middle: x or (not x) = T (at least one must be true)

    DeMorgan's inversions: not (x and y) = (not x) or (not y) ... not (x or y) = (not x) and (not y)

    Super absorption (my name): x and ((not x) or y)) = (x and y) ... x or ((not x) and y) = (x or y)

    As one can tell, there is a remarkable symmetry between conjunction and disjunction, with negation interchanging them. That is very hard to see from WFF 'N Proof's formalism.
    Last edited by lpetrich; 2018-Dec-12 at 11:27 PM.

  8. #8
    Join Date
    Nov 2001
    Posts
    789
    If one does Boolean algebra, one can easily introduce multivalued logics, with truth values in addition to true and false. A simple one is to add "maybe" or M, a truth value that is either true or false: (T, F). How to evaluate with it: not (T, F) = (not T, not F) = (F, T) = (T, F). T and (T, F) = (T and T, T and F) = (T, F). F and (T, F) = (F and T, F and F) = (F, F) = F. Its truth tables:
    Code:
    not   and       or        ->        ==
    . .   . F M T   . F M T   . F M T   . F M T
    F T   F F F F   F F M T   F T T T   F T M F
    M M   M F M M   M M M T   M M M T   M M M M
    T F   T F M T   T T T T   T F M T   T F M T
    One finds all of the Boolean-algebra properties except for non-contradiction (M and M = M, not F), excluded middle (M or M = M, not T), and super absorption.

    This is a special case of fuzzy logic, where one defines truth values between true (1) and false (0).

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
  •