WFF 'N PROOF: The Game of Modern Logic

WFF 'N PROOF:
The Game of Modern Logic
By Layman E. Allen
Professor of Law and Senior Research Scientist, University of Michigan

The Tarski Short Cut
(for testing whether a candidate WFF is a provable theorem)

Suppose the candidate to be false, and see whether that supposition leads to contradiction. If it does, the candidate is a provable theorem. In effect, this is using the No Rule (indirect proof).

Truth Table Formulation of Two-Valued Propositional Logic

Definitions of K, A, N, C, and E

p q	Kpq	Apq	Np	Cpq	Epq
1 1	1	1	0	1	1
1 0	0	1	0	0	0
0 1	0	1	1	1	0
0 0	0	0	1	1	1

Three Different Decision Procedures

1. Long Form of Truth Table on Candidate: C-Cpq-CNqNp

p q	Cpq	Nq	Np	CNqNp	C-Cpq-CNqNp
1 1	111	01	01	10101	1-111-10101
1 0	010	10	01	01001	1-010-01001
0 1	101	01	10	10110	1-101-10110
0 0	100	10	10	11010	1-100-11010

Since the candidate (Column 6) is true for all combinations of p and q, it is a provable theorem.

2. Short Form of Truth Table on Candidate: C-Cpq-CNqNp

C-Cpq-CNqNp

1-111-10101

1-010-01001

1-101-10110

1-100-11010

Since the candidate is true for all combinations of p and q, it is a provable theorem.

3. Shortest Form: The Tarski Short Cut on Several Candidates

Example 1: C-Cpq-CNqNp

Candidate	Comments
C-Cpq-CNqNp 0 110 01001 0	Suppose the candidate to be false, and see if that leads to contradiction by the definitions of its operators. It does: Cpq=1 and Cpq=0. The candidate is a theorem. C-Cpq-CNqNp = 1.
1 267 34756 8	The numbers to the left indicate the order in which the truth values, 0 and 1, are assigned to the letters in the candidate expression by the supposition and the definitions of the operators.

Example 2: C-NCpq-KpNq

Candidate	Comments
C-NCpq-KpNq 0 1010 0110 1	By supposing C-Cpq-CNq-Np = 0, KpNq=0 and KpNq=1; therefore C-Cpq-CNq-Np = 1.
1 2456 3576 8	The numbers to the left indicate the order in which the truth values, 0 and 1, are assigned.

Example 3: E-NApq-KNpNq

Candidate	Comments
E-NApq-KNpNq 0 1 0 Case 1 000 11010 1 2456 37586 9 0 1 Case 2 1000 1010 1 2867 34657 9	E-NApq-KNpNq can be false in two different ways: (1) NApq=1 and KNpNq=0, and (2) NApq=0 and KNpNq=1. Thus, two cases must be considered, and both must be contradictory. In Case 1 supposing E-NApq-KNpNq=0 leads to KNpNq=0 and KNpNq=1, and in Case 2 supposing it leads to NApq=0 and NApq=1. Thus, E-NApq-KNpNq=1.

Example 4: C-CKpqr-ACprCqr

Candidate	Comments
C-CKpqr-ACprCqr 0 11111 0010010 1	Supposing C-CKpqr-ACprCqr=0 leads to r=0 and r=1. Thus, C-CKpqr-ACprCqr=1.
1 29687 3467587 10 10	Order of assignment of truth values.

Example 5: C-CNpq-Apq

Candidate	Comments
C-CNpq-Apq 0 1100 000 0	Supposing C-CNpq-Apq=0 leads to CNpq=1 and CNpq=1. Thus, C-CNpq-Apq=1.

The Tarski Short Cut and Derivable Rules

Testing Derivability of a Rule Candidate

Not only is the Tarski Short Cut a powerful tool for ascertaining whether or not a WFF is a theorem, but it can also be used to determine whether a rule candidate is a derivable rule. With every rule candidate there is an associated C-WFF. If its associated C-WFF is a theorm, then the rule candidate is derivable, and vice versa, that is:
Associated C-WFF is Theorem **----** Rule Candidate is Derivable.
So, to test whether a rule candidate is derivable, test its associated C-WFF for theoremhood.

Rule Candidate's Associated C-WFF

The C-WFF associated with a rule candidate is the C-WFF such that its antecedent is the conjunction of the rule candidate's premisses and its consequent is the rule candidate's conclusion.

Thus, the associated C-WFF for the rule candidate:
p, Ars --? KrAsp
is:
C-KpArs-KrAsp.

When the Tarski Short Cut is used to test C-KpArs-KrAsp, it turns out not to be a theorem; so, the rule candidate is not derivable.
C-KpArs-KrAsp
0 11101 00111
Thus, C-KpArs-KrAsp=0 when p=1, r=0, and s=p; there is no contradiction. The rule candidate is not derivable: p, Ars --o KrAsp

On the other hand, when the associated C-WFF to the rule candidate:
     p, q, CArqs --? KAsrp
is tested, it turns out to be a theorem:
   C-K.Kpq.CArqs-KAsrp
   0 1 111 11 11 011 1
                 1
   1 2 467 58 79 3 9
                                        10
                 11
So, the rule candidate is a derived rule: p, q, CArqs --** KAsrp

And WFF 'N PROOF players should be able to construct a proof of this new derived rule, that is, that p,q,CArqs/Ai,Co,Ki is a Solution for the Goal, KAsrp.

Advice to Coaches and Players of Adventurous WFF 'N PROOF

Thorough familiarity with the Tarski Short Cut contributes remarkably to the quality of strategy that players are equipped to bring to bear upon their play in pursuit of the Leslie Nielsen Scholarship award. --LEA

WE WELCOME YOUR SUGGESTIONS for improving this web site. Send them directly to: laymanal@umich.edu. Please include the URL above (web address) of the page to which your comment refers.