WFF 'N Proof -- mathematical-logic game

[lpetrich]

WFF 'N Proof -- "The Game of Modern Logic" -- one uses mathematical-logic constructions and inference rules in it, like try to find valid inferences.

I had the game once, and all that I now have left is its rulebook. The WFF in it 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.

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, a convenience in proofs.

 

[lpetrich]

I'll now prove various Boolean-algebra identities.

K: "and"

K is commutative:
1. Kpq ... s -- stipulation
2. p ... Ko 1
3. q ... Ko 1
4. Kqp ... Ki 3, 2

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

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

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

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

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

 

[Wiploc]

I remember liking the dice.

 

[lpetrich]

Distributive rules:

1. K-Apq-Apr ... s
2. Apq ... Ko 1
3. Apr ... Ko 1
4a. p ... s
4b. A-p-Kqr ... Ai 4a
5a. q ... s
5b. Apr ... R 3
5c1. p ... s
5c2. A-p-Kpr ... Ai 5c1
5d1. r ... s
5d2. q ... R 5a
5d3. Kqr ... Ki 5d2 5d1
5d4. A-p-Kqr ... Ai 5d3
5e. A-p-Kqr ... Ao 5b 5c 5d
6. A-p-Kqr ... Ao 2, 4, 5

1. A-Kpq-Kpr ... s
2a. Kpq ... s
2b. p ... Ko 2a
2c. q ... Ko 2a
2d. Aqr ... Ai 2c
2e. K-p-Aqr ... Ki 2b 2d
3a. Kpr ... s
3b. p ... Ko 3a
3c. r ... Ko 3a
3d. Aqr ... Ai 3c
3e. K-p-Aqr ... Ki 3b 3d
4. K-p-Aqr ... Ao 1 2 3

 

[lpetrich]

N: "not"

Excluded middle (p, Np -> q):

1. p ... s
2. Np ... s
3a. Nq ... s
3b. p ... R 1
3c. Np ... R 2
4. q ... No 3

N is an involution (repeating it gives the original value):

1. NNp ... s
2a. Np ... s
2b. Np ... R 2a
2c. NNp ... R 1
3. p ... No 2

De Morgan's rules (and <-> or with not)

1. K-Np-Nq ... s
2a. Apq ... s
2b1. p ... s
2b2. p ... R 2b1
2c1. q ... s
2c2. K-Np-Nq ... R 1
2c3. Nq ... Ko 2c2
2c4. p ... excl mid 2c1 2c3
2d. p ... Ao 2a 2b 2c
2e. K-Np-Nq ... R 1
2f. Np ... Ko 2e
3. N-Apq ... Ni 2 (a, d, f)

1. A-Np-Nq ... s
2a. Np ... s
2b1. Kpq ... s
2b2. p ... Ko 2b1
2b3. Np ... R 2a
2c. N-Kpq ... No 2b
3a. Nq ... s
3b1. Kpq ... s
3b2. q ... Ko 3b1
3b3. Nq ... R 3a
2c. N-Kpq ... No 3b
3. N-Kpq ... Ao 1 2 3

 

[lpetrich]

Now for implication.

Anything implies itself.

1a. p ... s
1b. p ... R 1a
2. Cpp ... Ci 1

Now for relating implication to the previous operators. P implies Q == (not P) or Q

1. Cpq ... s
2a. N-A-Np-q ... s
2b1. Np ... s
2b2. A-Np-q ... Ai 2b1
2b3. N-A-Np-q ... R 2a
2c. p ... No 2b
2d. Cpq ... R 1
2e. q ... Co 2d 2c
2f. A-Np-q ... Ai 2e
2g. N-A-Np-q ... R 2a
3. A-Np-q ... No 2

1. Apq... s
2a. Np ... s
2b. Apq ... R 1
2c1. p ... s
2c2a. Nq ... s
2c2b. p ... R 2c1
2c2c. Np ... R 2a
2c3. q ... No 2c
2d1. q ... s
2d2. q ... R 2d1
2e. q ... Ao 2b 2c 2d
4. C-Np-q ... Ci 2


This is as far as I want to go. Most of the proofs are mine, though for a few of them, I cheated and looked in the book.

 

[lpetrich]

There are curious deficiencies in that book.

The book does not relate its notation to more typical sorts of mathematical-logic notations. I'll do what I can with ASCII characters:
Kpq ... p and q
Apq ... p or q
Cpq ... p impl q, p -> q
Epq ... p eqv q, p == q
Np ... ~p, not p

The book also does not name the properties that it proves. It has proofs of:
K commutative (p 54), associative (p 57, 58)
A commutative (p 148), associative (p 150)
A distributive over K (p 151, 152), K distributive over A (p 152, 153)
Non-contradiction (definitions of No and Ni)
Excluded middle (p 160)
Negation as involution (p 160, 168)
De Morgan's rules (p 172, 173, 174)

However, it has proofs for both directions of inference, while I'd given proofs for only one direction.


Here is a proof that () -> ApNp (another statement of excluded middle):

1a. NApNp ... s
1a1. Np ... s
1a2. ApNp ... Ai 1a1
1a3. NApNp ... R 1a
1b. p ... No 1a
1c. ApNp ... Ai 1b
1d. NApNp ... R 1a
2. ApNp ... No 2

 

[lpetrich]

Now for the opposite-direction proofs.

For K and A commutative, the proofs work in both directions. For K and A associative, one may use their commutative property to get reverse-direction proofs.

Distributive is more difficult.

1. A-p-Kqr ... s
2a. p ... s
2b. Apq ... Ai 2a
2c. Apr ... Ai 2a
2d. K-Apq-Apr ... Ki 2b 2c
3a. Kqr ... s
3b. q ... Ko 3a
3c. r ... Ko 3a
3d. Apq ... Ai 3b
3e. Apr ... Ai 3r
3f. K-Apq-Apr ... Ki 3d 3e
4. K-Apq-Apr ... Ao 1 2 3

1. K-p-Aqr ... s
2. p ... Ko 1
3. Aqr ... Ko 2
4a. q ... s
4b. p ... R 2
4c. Kpq ... Ki 4b 4a
4d. A-Kpq-Kpr ... Ai 4c
5a. r ... s
5b. p ... R 2
5c. Kpr ... Ki 5b 5a
5d. A-Kpq-Kpr ... Ai 5c
6. A-Kpq-Kpr ... Ao 4 5 6

Negation being an involution:

1.p ... s
2a. Np ... s
2b. p ... R 1
2c. Np ... R 2a
3. NNp ... Ni 2

De Morgan's rules cover opposite directions, to within negations.

I'd already covered both directions for implication.

 

[lpetrich]

Why mention commutative, associative, and distributive properties? To show that it is not just arithmetic that has them.

One may also connect logic with arithmetic with true = 1, false = 0.
The "not" operator is easy: not x = 1 - x

However, the "and" and "or" operators are anything but unique. Here are three sets that satisfy commutativity, associativity, identity, zero, and De Morgan:

x and y = x*y
x or y = x + y - x*y

x and y = min(x,y)
x or y = max(x,y)

x and y = max(x+y-1,0)
x or y = min(x+y,1)

By using truth values between 0 and 1, one gets "fuzzy logic", and that has gotten a lot of use in device-control applications and artificial intelligence.

 

[fromderinside]

Eyup. Used conjoint scaling to accomplish it as well. The best approach for getting from ordinal data to interval measurement.*

* Theory of conjoint measurement

 

[lpetrich]

Eyup. Used conjoint scaling to accomplish it as well. The best approach for getting from ordinal data to interval measurement.*

* Theory of conjoint measurement

I couldn't figure out what that is.

 

[lpetrich]

A note about the notation that WFF 'N Proof uses. It uses prefix notation for its binary operators, operator before operands, instead of infix notation, operator between operands, what one usually does in mathematical logic. Early 20th cy. mathematical logician Jan Łukasiewicz introduced this notation, and because of his nationality, it is sometimes called Polish notation.

That is why suffix notation, with the operator after operands, is sometimes called reverse Polish notation. HP calculators use it.

But there is a big user of prefix notation, though a behind-the-scenes one. Computer CPU's. Their instructions are expressed in the form
(opcode) (operands)
where "opcode" is short for "operation code" and the operands are what the operation works on -- data values (immediate) or locations of data values or even locations of locations of data values.

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

 

[lpetrich]

Another deficiency in WFF 'N Proof's notation is not using "true" and "false" values directly. That makes it hard to express directly certain properties involving them:

Identity:
true and x = x
false or x = x

Zero or Annihilator:
false and x = false
true or x = true

Non-Contradiction and Excluded Middle:
x and (not x) = false
x or (not x) = true

There are two remaining properties, the absorption ones, and I will construct WFF 'N Proof proofs for them:
x or (x and y) = x
x and (x or y) = x

1. A-p-Kpq ... s
2a. p ... s
2b. p ... R 2a
3a. Kpq ... s
3b. p ... Ko 3a
4. p ... Ao 1 2 3

1. p ... s
2. A-p-Kpq ... Ai 1

1. K-p-Apq ... s
2. p ... Ko 1

1. p ... s
2. Apq ... Ai 1
3. K-p-Apq ... Ki 1 2

 

[lpetrich]

Layman Allen, creator of WFF 'N Proof, has created some similar mathematical games, On-Sets and Equations, about set theory and arithmetic. Both are played much like WFF 'N Proof, where players must find set-theory and arithmetic expressions within various constraints. Unlike WFF 'N Proof, 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

 

[lpetrich]

There are some other properties of Boolean algebra that I should mention:

Super Absorption
x and ((not x) or y) = x and y
x or ((not x) and y) = x or y

Equivalence
x eqv x = 1
x eqv (not x) = 0
(not x) eqv (not y) = x eqv y
x eqv y = (x and y) or ((not x) and (not y)) = (x or (not y)) and ((not x) or y)

-

Absorption has this interrelationship, a consequence of distributivity and idempotence:

x and (x or y) = (x and x) or (x and y) = x or (x and y) = (x or x) and (x or y) = x and (x or y)

Proof of absorption with special cases:
x and (x or 0) = x and x = x
x and (x or 1) = x and 1 = x
x or (x and 0) = x or 0 = x
x or (x and 1) = x or x = x

Super absorption can be proved with distributivity and NCEM:

x and ((not x) or y) = (x and (not x)) or (x and y) = 0 or (x and y) = x and y
x or ((not x) and y) = (x or (not x)) and (x or y) = 1 and (x or y) = x or y

-

A typo in the first distributive proof:
5c2. A-p-Kpr ... Ai 5c1
should be
5c2. A-p-Kqr ... Ai 5c1

 

[fromderinside]

I think my current post and your post to which this response applies should be in your thread on almost integer numbers.

I couldn't figure out what that is.

Argument for a process used to move multidimensional ordinal data to interval data using statistical ranking methods in social sciences and soft engineering like pilot aircraft performance and workload evaluations.

... never ending story of how to make observations more usable and testable.

Imagine a two dimensional ranking approach with followup ranking of elements in both categories (joint) resulting an advancing the data from two ordinal scales to one multidimensional interval scale.

As few as seven well trained individuals, pilots, could first rank each dimension with five levels each, workload and effort say, then rank the overall rankings in order yielding arguably an interval ranking of workload-effort.

The result would combine physical or neural effort, say oxygen uptake, and perceived level or one's capacity to perform a mental/physical task into something measured in oxygen uptake rate since effort and workload both contain a perceptual component and oxygen uptake with the perceptual cancelling out.

The thought was triggered in me by your separate discussion of number.

 

[lpetrich]

Now for WFF 'N Proof still proofs of the super absorption properties

1. K-p-ANpq ... s
2. p ... Ko 1
3. ANpq ... Ko 1
4a. Np ... s
4b1. Nq ... s
4b2. p ... R 2
4b3. Np ... R 4a
4c. q ... No 4b
4d. p ... R 2
4e. Kpq ... Ki 4d 4c
5a. q ... s
5b. p ... R 2
5c. Kpq ... Ki 5a, 5b
6. Kpq ... Ao 3, 4, 5

1. Kpq ... s
2. p ... Ko 1
3. q ... Ko 1
4. ANpq ... Ai 3
5. K-p-ANpq ... Ki 2, 4

1. A-p-KNpq ... s
2a. p ... s
2b. Apq ... Ai 2a
3a. KNpq ... s
3b. q ... Ko 3a
3c. Apq ... Ai 3b
4. Apq ... Ao 1, 2, 3

1. Apq ... s
2a. p ... s
2b. A-p-KNpq ... Ai 2a
3a. q ... s
3b. ApNp ... excl mid
3c. Apq ... R 1
3d. K-ApNp-Apq ... Ki 3b 3c
3e. Ap-KNpq ... distrib 3d
4. A-p-KNpq ... Ao 1, 2, 3