lpetrich
Contributor
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.
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.