RESOURCE DESCRIPTION FRAMEWORK
FOR MUCOSAL SURFACE PATHOLOGY.
APPENDIX H. ZEMAN'S MODAL LOGIC. CHAPTER 2.
DRAFT COPY ONLY.
3/7/2008.

G. William Moore, MD, PhD.
Grace F. Kao, MD.
Lawrence A. Brown, MD.
http://www.netautopsy.org/mucordfh.htm
http://www.netautopsy.org/mucordfh.ppt


Dr. Moore     Dr. Kao     Dr. Brown

Send comments and correspondence to: George.Moore4@va.gov


1. DISCLAIMER.

United States Government Work, uncopyrighted, public-domain, DRAFT COPY ONLY. This document does not necessarily represent the views or policies of any United States Government agency. This document is provided "as is", without warranty of any kind, express or implied, including but not limited to the warranties of merchantability, fitness for a particular purpose and non-infringement. In no event shall the authors be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of, or in connection with the document or the use or other dealings made with the document.

2. TABLE OF CONTENTS.

1. Disclaimer.
2. Table of Contents.
3. Introduction, References.
27. Appendix H. Symbolic Logic Theorems.

3. INTRODUCTION, REFERENCES.



48. Zeman J.
Modal Logic, The Lewis-Modal Systems.
Oxford: Oxford at the Clarendon Press. 1973;:.
ISBN not stated, 302 pages.

49. Moore GW, Miller RE, Hutchins GM.
Microcomputer translator for medical text: Theorem verification for Chapter Two of Zeman's Modal Logic.
Adv Math Comput Med. 7:1621-1633, 1986.

27. APPENDIX H.
THEOREMS, FROM
ZEMAN'S MODAL LOGIC.
CHAPTERS 1,2.

NOTES. Zeman's logic expressions are written in parenthesis-free, so-called Polish notation (Łukasiewicz,.......). where operators: 
             LOGIC OPERATORS
   Zeman       Our
 notation    notation        Description
     C          ⇒           IMPLIES
     K          &            AND
     A          |            INCLUSIVE_OR, ALTERNATION
     E          ⇔           EQUALS
     K          -            NOT
In traditional symbolic logic notation, the operators are INFIXed between the subject and object, i.e., subject OPERATOR object. For example, p IMPLIES q, denoted p ⇒ q; or p AND q, denoted p & q.

In Polish notation, the operators PREFIX the subject and object, i.e., OPERATOR subject object. For example, IMPLIES p q, denoted ⇒pq; or AND p q, denoted & p q.

Thus, expression 1.2 is represented as
p ⇒ (q ⇒ p).
in traditional notation, and
CpCqp
in Polish notation.

Proofs consist of translating Polish notation into in traditional notation (for easier readability); then translating the traditional notation into NANDSETs. If all nandsets are vacuous, then the theorem is proved.

Proof tricks:

--p ⇔ +p (Double Negative).
(+p ⇒ +q) ⇔ nandset {+p,-q} (Nandset).
(+p ⇒ +q) ⇔ (-p | q) (Whitehead_Russell Transformation).
(+p = +q) ⇔ (+p ⇒ +q) and (+q ⇒ +p) (Equivalence).
(+p | +q) ⇔ -(-p & -q) (DeMorgan's Rule).
(+p & +q) ⇔ -(-p | -q) (DeMorgan's Rule).
((+p & +q) | +r) ⇔ ((+p & +r) | (+p & +r)) (Distributive Rule).
((+p | +q) & +r) ⇔ ((+p | +r) & (+p & +r)). (Distributive Rule).
EXPANSION THEOREM. 
 +p                       +p
    +q         ⇔            +q
                             +q
                             ...

Proof: IF. (+p ⇒ +q) ⇒ (+p ⇒ (+q | +q |...)).
Nandsets {-p,+p,-q,-q} and {+q,+p,-q,-q} are vacuous.

ONLY IF. (+p ⇒ (+q | +q |...) ⇒ (+p ⇒ +q).
Nandsets {-p,+p,-q}, {+q,+p,-q}, and {+q,+p,-q} are vacuous.

BACKTRACK THEOREM. 
 +p                 +p
    +q      ⇔         +s
    ...                   +r
    +s                       +q
                             ...
Proof: It suffices to show:
(1) that ((+p ⇒ +q) & (+p ⇒ +s) & ((+p & +s) ⇒ +r)) ⇒ (+p ⇒ +s)
(2) that ((+p ⇒ +q) & (+p ⇒ +s) & ((+p & +s) ⇒ +r)) ⇒ ((+p & +s) ⇒ +r)
and (3) that ((+p ⇒ +q) & (+p ⇒ +s) & ((+p & +s) ⇒ +r)) ⇒ ((+p & +s & +r) ⇒ +q)

Proof (1): Nandsets 

 {-p,-p,-p,+p,-s},
 {-p,-p,-s,+p,-s},
 {-p,-p,+r,+p,-s},
 {-p,+s,-p,+p,-s},
 {-p,+s,-s,+p,-s},
 {-p,+s,+r,+p,-s},
 {+q,-p,-p,+p,-s},
 {+q,-p,-s,+p,-s},
 {+q,-p,+r,+p,-s},
 {+q,+s,-p,+p,-s},
 {+q,+s,-s,+p,-s}, and
 {+q,+s,+r,+p,-s}
are vacuous.

Proof (2): Nandsets 

 {-p,-p,-p,+p,+s,-r},
 {-p,-p,-s,+p,+s,-r},
 {-p,-p,+r,+p,+s,-r},
 {-p,+s,-p,+p,+s,-r},
 {-p,+s,-s,+p,+s,-r},
 {-p,+s,+r,+p,+s,-r},
 {+q,-p,-p,+p,+s,-r},
 {+q,-p,-s,+p,+s,-r},
 {+q,-p,+r,+p,+s,-r},
 {+q,+s,-p,+p,+s,-r},
 {+q,+s,-s,+p,+s,-r}, and
 {+q,+s,+r,+p,+s,-r}
are vacuous.

Proof (3): Nandsets 

 {-p,-p,-p,+p,+s,+r,-q},
 {-p,-p,-s,+p,+s,+r,-q},
 {-p,-p,+r,+p,+s,+r,-q},
 {-p,+s,-p,+p,+s,+r,-q},
 {-p,+s,-s,+p,+s,+r,-q},
 {-p,+s,+r,+p,+s,+r,-q},
 {+q,-p,-p,+p,+s,+r,-q},
 {+q,-p,-s,+p,+s,+r,-q},
 {+q,-p,+r,+p,+s,+r,-q},
 {+q,+s,-p,+p,+s,+r,-q},
 {+q,+s,-s,+p,+s,+r,-q}, and
 {+q,+s,+r,+p,+s,+r,-q}
are vacuous.

INTERCALATION THEOREM. 
 +p                       +p
    +q         ⇔            +s
       +r                       +r
       ...                      ...
    +q
       +s
       ...
Proof: It suffices to show that: (((+p & +q) ⇒ +r) & ((+p & +q) ⇒ +s)) ⇒ ((+p & +q) ⇒ +r)
Nandsets 

 {-p,-p,+p,+q,-r},
 {-p,-q,+p,+q,-r},
 {-p,+s,+p,+q,-r},
 {-q,-p,+p,+q,-r},
 {-q,-q,+p,+q,-r},
 {-q,+s,+p,+q,-r},
 {+r,-p,+p,+q,-r},
 {+r,-q,+p,+q,-r}, and
 {+r,+s,+p,+q,-r}
are vacuous.

RETIREMENT THEOREM. 
 +p                 +p
    +q      ⇔         +s
       +r                 +r
    +q
       +s
    +q
       -s
Proof. IF. It suffices to show that: (((+p & +q) ⇒ +r) & ((+p & +q) ⇒ +s) & ((+p & +q) ⇒ -s)) ⇒ ((+p & +q) ⇒ +r).
Nandsets 

 {-p,-p,-p,+p,+q,-r},
 {-p,-p,-q,+p,+q,-r},
 {-p,-p,-s,+p,+q,-r},
 {-p,-q,-p,+p,+q,-r},
 {-p,-q,-q,+p,+q,-r},
 {-p,-q,-s,+p,+q,-r},
 {-p,+s,-p,+p,+q,-r},
 {-p,+s,-q,+p,+q,-r},
 {-p,+s,-s,+p,+q,-r},
 {-q,-p,-p,+p,+q,-r},
 {-q,-p,-q,+p,+q,-r},
 {-q,-p,-s,+p,+q,-r},
 {-q,-q,-p,+p,+q,-r},
 {-q,-q,-q,+p,+q,-r},
 {-q,-q,-s,+p,+q,-r},
 {-q,+s,-p,+p,+q,-r},
 {-q,+s,-q,+p,+q,-r},
 {-q,+s,-s,+p,+q,-r},
 {+r,-p,-p,+p,+q,-r},
 {+r,-p,-q,+p,+q,-r},
 {+r,-p,-s,+p,+q,-r},
 {+r,-q,-p,+p,+q,-r},
 {+r,-q,-q,+p,+q,-r},
 {+r,-q,-s,+p,+q,-r},
 {+r,+s,-p,+p,+q,-r},
 {+r,+s,-q,+p,+q,-r}, and
 {+r,+s,-s,+p,+q,-r}
are vacuous.

Proof. ONLY IF. It suffices to show that: ((+p & +q) ⇒ +r) ⇒ (((+p & +q) ⇒ +r) & ((+p & +q) ⇒ +s) & ((+p & +q) ⇒ -s)).
Nandsets 

 {-p,-q,+r,+p,+p,+p},
 {-p,-q,+r,+p,+p,+q},
 {-p,-q,+r,+p,+p,+s},
 {-p,-q,+r,+p,+q,+p},
 {-p,-q,+r,+p,+q,+q},
 {-p,-q,+r,+p,+q,+s},
 {-p,-q,+r,+p,-p,+p},
 {-p,-q,+r,+p,-p,+q},
 {-p,-q,+r,+p,-p,+s},
 {-p,-q,+r,+q,+p,+p},
 {-p,-q,+r,+q,+p,+q},
 {-p,-q,+r,+q,+p,+s},
 {-p,-q,+r,+q,+q,+p},
 {-p,-q,+r,+q,+q,+q},
 {-p,-q,+r,+q,+q,+s},
 {-p,-q,+r,+q,-p,+p},
 {-p,-q,+r,+q,-p,+q},
 {-p,-q,+r,+q,-p,+s},
 {-p,-q,+r,-r,+p,+p},
 {-p,-q,+r,-r,+p,+q},
 {-p,-q,+r,-r,+p,+s},
 {-p,-q,+r,-r,+q,+p},
 {-p,-q,+r,-r,+q,+q},
 {-p,-q,+r,-r,+q,+s},
 {-p,-q,+r,-r,-p,+p},
 {-p,-q,+r,-r,-p,+q}, and
 {-p,-q,+r,-r,-p,+s}
are vacuous.

STRICT ALTERNATIVE THEOREM. In a simplified model of cytogenetics, let there be exactly two genders, female and male (i.e., no gender variants); and consider the presence_or_absence of the y_chromosome. Then: 
 +cytogenetics
    +male
       +y_chromosome
    -male
       -y_chromosome
Alternatively: 
 +cytogenetics
    +y_chromosome
       +male
    -y_chromosome
       -male
According to the Strict Alternative Theorem, these two expressions are equal. In a more general expression: 
 +p                      +p
    +q                      +r
       +r        ⇔             +q
    -q                      -r
       -r                      -q
Proof. IF. It suffices to show that
(1A): (((+p & +q) ⇒ +r) & ((+p & -q) ⇒ -r)) ⇒ ((+p & +r) ⇒ +q)); and that
(1B): (((+p & +q) ⇒ +r) & ((+p & -q) ⇒ -r)) ⇒ ((+p & -r) ⇒ -q)).

Proof. 1A. Nandsets 

 {-p,-p,+p,+r,-q},
 {-p,+q,+p,+r,-q},
 {-p,-r,+p,+r,-q},
 {-q,-p,+p,+r,-q},
 {-q,+q,+p,+r,-q},
 {-q,-r,+p,+r,-q},
 {+r,-p,+p,+r,-q},
 {+r,+q,+p,+r,-q}, and
 {+r,-r,+p,+r,-q}
are vacuous.

Proof. 1B. Nandsets 

 {-p,-p,+p,-r,+q},
 {-p,+q,+p,-r,+q},
 {-p,-r,+p,-r,+q},
 {-q,-p,+p,-r,+q},
 {-q,+q,+p,-r,+q},
 {-q,-r,+p,-r,+q},
 {+r,-p,+p,-r,+q},
 {+r,+q,+p,-r,+q}, and
 {+r,-r,+p,-r,+q}
are vacuous.

Proof. ONLY IF. It suffices to show that (2A): (((+p & +r) ⇒ +q) & ((+p & -r) ⇒ -q)) ⇒ ((+p & +q) ⇒ +r)); and that (2B): (((+p & +r) ⇒ +q) & ((+p & -r) ⇒ -q)) ⇒ ((+p & -q) ⇒ -r))

Proof. 2A. Nandsets 

 {-p,-p,+p,+q,-r},
 {-p,+r,+p,+q,-r},
 {-p,-q,+p,+q,-r},
 {-q,-p,+p,+q,-r},
 {-q,+r,+p,+q,-r},
 {-q,-q,+p,+q,-r},
 {+r,-p,+p,+q,-r},
 {+r,+r,+p,+q,-r}, and
 {+r,-q,+p,+q,-r}
are vacuous.

Proof. 2B. Nandsets 

 {-p,-p,+p,-q,+r},
 {-p,+r,+p,-q,+r},
 {-p,-q,+p,-q,+r},
 {-q,-p,+p,-q,+r},
 {-q,+r,+p,-q,+r},
 {-q,-r,+p,-q,+r},
 {+r,+r,+p,-q,+r}, and
 {+r,-q,+p,-q,+r}
are vacuous.

Here are Zeman's theorems stated in Polish and conventional notation:

1.1. CCpCqrCCpqCpr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+p ⇒ +q) ⇒ (+p ⇒ +r)).
1.2. CpCqp. Restated: +p ⇒ (+q ⇒ +p).
1.3. CCpqCpp. Restated: (+p ⇒ +q) ⇒ (+p ⇒ +p).
1.4. Cpp. Restated: (+p ⇒ +p).
1.5. CCpqCCqrCpr. Restated: (+p ⇒ +q). ⇒ ((+q ⇒ +r) ⇒ (+p ⇒ +r)).
1.6. CCCCqrCprsCCpqs. Restated: ((+q ⇒ +r) ⇒ ((+p ⇒ +r) ⇒ +s)) ⇒ ((+p ⇒ +q) ⇒ +s).
1.7. CCpCqrCCsqCpCsr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+s ⇒ +q) ⇒ (+p ⇒ (+s ⇒ +r))).

C1. CCpCqrCCpqCpr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+p ⇒ +q) ⇒ (+p ⇒ +r)).
C2. CpCqp. Restated: +p ⇒ (+q ⇒ +p).
2.1. CCpqCpp. Restated: (+p ⇒ +q) ⇒ (+p ⇒ +p).
2.2. Cpp. Restated: (+p ⇒ +p).
2.3. CpCqr, Cpq, p ├ r. Restated: ((+p ⇒ (+q ⇒ +r)) & (+p ⇒ +q)) ⇒ (+p ⇒ +r).
2.4. p, q ├ p. Restated: +p ⇒ (+q ⇒ +p).
2.5. CsCCpCqrCCpqCpr. Restated: (+s ⇒ (+p ⇒ (+q ⇒ +r))) ⇒ ((+q ⇒ +r) ⇒ (+q ⇒ +r)).
2.6. CCsCpCqrCsCCpqCpr. Restated: (+s ⇒ (+p ⇒ (+q ⇒ +r))) ⇒ (+s ⇒ ((+p ⇒ +q) ⇒ (+p ⇒ +r))).
2.7. CCqrCpCqr. Restated: (+q ⇒ +r) ⇒ (+p ⇒ (+q ⇒ +r)).
2.8. CCqrCCpqCpr. Restated: (+q ⇒ +r) ⇒ ((+p ⇒ +q) ⇒ (+p ⇒ +r)).
2.9. CCCqrCpqCCqrCpr. Restated: ((+q ⇒ +r) ⇒ (+p ⇒ +q)) ⇒ ((+q ⇒ +r) ⇒ (+p ⇒ +r)).
2.10. CCpqCCqrCpq. Restated: (+p ⇒ +q) ⇒ ((+p ⇒ +q) ⇒ (+p ⇒ +r)).
2.11. CCpqCCqrCpr. Restated: (+p ⇒ +q) ⇒ ((+q ⇒ +r) ⇒ (+p ⇒ +r)).
2.12. CCCpqrCqr. Restated: ((+p ⇒ +q) ⇒ +r) ⇒ (+q ⇒ +r).
2.13. CCCCqrCprsCCpqs. Restated: (((+q ⇒ +r) ⇒ (+p ⇒ +r)) ⇒ +s) ⇒ ((+p ⇒ +q) ⇒ +s).
2.14. CCpCqrCCsqCpCsr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+s ⇒ +q) ⇒ (+p ⇒ (+s ⇒ +r))).
2.15. CCpCqrCqCpr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ (+q ⇒ (+p ⇒ +r)).
2.16. CpCCpqq. Restated: p ⇒ (p ⇒ q) ⇒ q)).
2.17. CCpqCCpCqrCpr. Restated: (+p ⇒ +q) ⇒ ((+p ⇒ (+q ⇒ +r)) ⇒ (+q ⇒ +r)).
2.18. CCpCpqCpq. Restated: (+p ⇒ (+p ⇒ +q)) ⇒ (+p ⇒ +q).
2.19. CCCpqqCCqpCCpqp. Restated: ((+p ⇒ +q) ⇒ +q) ⇒ ((+q ⇒ +p) ⇒ ((+p ⇒ +q) ⇒ +p)).
2.20. CCqpCCCqppp. Restated: (+q ⇒ +p) ⇒ (((+q ⇒ +p) ⇒ +p) ⇒ +p).
2.21. CCqpCCCqpCCpqpp. Restated: (+q ⇒ +p) ⇒ ((+q ⇒ +p) ⇒ (((+p ⇒ +q) ⇒ +p)) ⇒ +p).
2.22. CCCqpCCpqpCCqpp. Restated: ((+q ⇒ +p) ⇒ ((+p ⇒ +q) ⇒ +p)) ⇒ ((+q ⇒ +p) ⇒ +p).
2.23. CCCpqqCCqpp. Restated: ((+p ⇒ +q) ⇒ +q) ⇒ ((+q ⇒ +p) ⇒ +p).
2.24. CCqpCCCpqqp. Restated: ((+q ⇒ +p) ⇒ (((+p ⇒ +q) ⇒ +q) ⇒ +p).
K1. CpCqKpq. Restated: p ⇒ (q ⇒ (p & q)).
K2. CKpqp. Restated: (p & q) ⇒ p.
K3. CKpqq. Restated: (p & q) ⇒ q.
2.25. CKqpCKqpKpq. Restated: (+q & +p) ⇒ ((+q & +p) ⇒ (+p & +q)).
2.26. CKqpKpq. Restated: (q & p) ⇒ (p & q).
2.27. CpKpp. Restated: p ⇒ (p & p).
2.28. CCpqCpCrKqr. Restated: (+p ⇒ +q) ⇒ (+p ⇒ (+r ⇒ (+q & +r))).
2.29. CCpqCKprCKprKqr. Restated: (+p ⇒ +q) ⇒ ((+p & +r) ⇒ ((+p & +r) ⇒ (+q & +r))).
2.30. CCpqCKprKqr. Restated: (+p ⇒ +q) ⇒ ((+p & +r) ⇒ (+q & +r)).
2.31. CCpqCKrpKrq. Restated: (+p ⇒ +q) ⇒ ((+r & +p) ⇒ (+r & +q)).
2.32. CCqrCKqqKqr. Restated: (+q ⇒ +r) ⇒ ((+q & +q) ⇒ (+q & +r)).
2.32a. CCqrCqKqr. Restated: (+q ⇒ +r) ⇒ (+q ⇒ (+q & +r)).
2.33. CCqpCCpqCCCqrCqKqrCCprCpKqr. Restated: (+q ⇒ +p) ⇒ (+p ⇒ +q) ⇒ ((+q ⇒ +r) ⇒ ((+q ⇒ (+q & +r))) ⇒ ((+p ⇒ +r) ⇒ (+p ⇒ (+q & +r)))).
2.34. CCCqrCqKqrCCqpCCpqCCprCpKqr. Restated: ((+q ⇒ +r) ⇒ (+q ⇒ (+q & +r))) ⇒ ((+q ⇒ +p) ⇒ ((+p ⇒ +q) ⇒ ((+p ⇒ +r) ⇒ (+p ⇒ (+p & +r))))).
2.35. CCqpCCpqCCprCpKqr. Restated: (+q ⇒ +p) ⇒ ((+p & +q) ⇒ ((+p & +r) (+p ⇒ (+q & +r)))).
2.36. CpCCpqCCprCpKqr. Restated: +p ⇒ ((+p ⇒ +q) ⇒ ((+p ⇒ +r) ⇒ (+p ⇒ (+q & +r)))).
2.37. CCpqCCprCpKqr. Restated: (+p ⇒ +q) ⇒ ((+p ⇒ +r) ⇒ (+p ⇒ (+q & +r))).
2.38. CCpCqrCpCqr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ (+p ⇒ (+q ⇒ +r)).
2.39. CCpCqrCKpqCKpqr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+p & +q) ⇒ ((+p & +q) ⇒ +r)).
2.40. CCpCqrCKpqr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+p & +q) ⇒ +r).
2.41. CCrsCCpCqrCpCqs. Restated: (+r ⇒ +s) ⇒ ((+p ⇒ (+q ⇒ +r)) ⇒ (+p ⇒ (+q ⇒ +s))).
2.42. CCpCqrCCrsCpCqs. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+r ⇒ +s) (+p ⇒ (+q ⇒ +r))).
2.43. CKpqCCKpqrr. Restated: (+p & +q) ⇒ (((+p & +q) ⇒ +r) ⇒ +r).
2.44. CpCqCCKpqrr. Restated: (+p ⇒ (+q ⇒ (((+p & +q) ⇒ +r) ⇒ +r))).
2.45. CCKpqrCpCqr. Restated: ((+p & +q) ⇒ +r) ⇒ (+p ⇒ (+q ⇒ +r)).
2.46. ECpCqrCKpqr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+p & +q) ⇒ +r) and ((+p & +q) ⇒ +r) ⇒ (+p ⇒ (+q ⇒ +r)).
2.47. CKpKqrp. Restated: (p & (q & r)) ⇒ p.
2.48. CKpKqrKqr. Restated: (+p & (+q & +r)) ⇒ (+q ⇒ +r).
2.49. CKpKqrq. Restated: (p & (q & r)) ⇒ q.
2.50. CKpKqrr. Restated: (p & (q & r)) ⇒ r.
2.51. CKpKqrKpq. Restated: (p & (q & r)) ⇒ (p & q).
2.52. CKpKqrKKpqr. Restated: (p & (q & r)) ⇒ ((p & q) & r).
2.53. CKKpqrKpKqr. Restated: ((+p & +q) & +r)) ⇒ (p & (q & r)).
2.54. EKpKqrKKpqr. Restated: (+p & (+q & +r)) ⇒ ((+p & +q) & +r); and ((+p & +q) & +r) ⇒ (+p & (+q & +r)).
2.55. EKpqKqp. Restated: ((+p & +q) = (+q & +p)) is ((p & q) ⇒ (q & p)) and ((q & p) ⇒ (p & q)).
2.56. EpKpp. Restated: (+p = (+p & +p)) is (+p ⇒ (+p & +p)) and ((+p & +p) ⇒ +p).
A1. CpApq. Restated: +p ⇒ (+p | +q).
A2. CqApq. Restated: +q ⇒ (+p | +q).
A3. CCprCCqrCApqr. Restated: (+p ⇒ +r) ⇒ ((+q ⇒ +r) ⇒ ((+p | +q) ⇒ +r)).
2.57. CAppp. Restated: (+p | +p) ⇒ +p.
2.58. CApqAqp. Restated: (+p | +q) ⇒ (+q | +p).
2.59. CApqAApqr. Restated: (+p | +q) ⇒ ((+p | +q) | +r).
2.60. CpAApqr. Restated: +p ⇒(+p | (+q | +r)).
2.61. CqAApqr. Restated: +q ⇒(+p | (+q | +r)).
2.62. CAqrAApqr. Restated: (+q | +r) ⇒ ((+p | +q) | +r).
2.63. CApAqrAApqr. Restated: (+p | (+q | +r)) ⇒ ((+p | +q) | +r).
2.64. CAApqrApAqr. Restated: ((+p | +q) | +r) ⇒ (+p | (+q | +r)).
2.65. CCsqCsAqr. Restated: (+s ⇒ +q) ⇒ (+s ⇒ (+q ⇒ +r)).
2.66. CpCCpqAqr. Restated: +p ⇒ ((+p ⇒ +q) ⇒ (+q | +r)).
2.67. CrCsAqr. Restated: +r ⇒ (+s ⇒ (+q | +r)).
2.68. CAprCCpqAqr. Restated: +p ⇒ (+p | +r) ⇒ ((+p ⇒ +q) ⇒ (+q ⇒ +r)).
2.69. CCpqCAprAqr. Restated: (+p ⇒ +q) ⇒ ((+p | +r) ⇒ (+q | +r)).
2.70. CCpqCArpArq. Restated: (+p ⇒ +q) ⇒ ((+r | +p) ⇒ (+r | +q)).
2.71. CApqCCpqq. Restated: (+p | +q) ⇒ ((+p ⇒ +q) ⇒ +q).
2.72 EAppp. Restated: (+p | +p) = +p. is ((+p | +p) ⇒ +p) and (+p ⇒ (+p | +p)).
2.73. EApqAqp. Restated: ((+p | +q) = (q | p)) is ((+p | +q) ⇒ (+q | +p)) and ((+q | +p) ⇒ (+p | +q)).
2.74. EApAqrAApqr. Restated: (+p | (+q | +r)) ⇒ ((+p | +q) | +r); and ((+p | +q) | +r) ⇒ (+p | (+q | +r)).
2.75. CKqrApq. Restated: (+q & +r) ⇒ (+p | +q).
2.76. CApKqrApq. Restated: (+p | (+q & +r)) ⇒ (+p | +q).
2.77. CKqrApr. Restated: (+q & +r) ⇒ (+p | +q).
2.78. CApKqrApr. Restated: (+p | (+q & +r)) ⇒ (+p | +r).
2.79. CApKqrKApqApr. Restated: (+p | (+q & +r)) ⇒ ((+p | +q) & (+p | +r)).
2.80. CrCArqArKpq. Restated: +r ⇒ ((+r | +q) ⇒ (+r | (+p & +q))).
2.81. CpCqArKpq. Restated: (+p ⇒ (+q ⇒ (+r | (+p & +q)))).
2.82. CpCrArKpq. Restated: (+p ⇒ (+r ⇒ (+r | (+p & +q)))).
2.83. CpCArqArKpq. Restated: +p ⇒ ((+r | +q) ⇒ (+r | (+p & +q))).
2.84. CArpCArqArKpq. Restated: (+r | +p) ⇒ ((+r | +p) ⇒ (+r | (+p & +q))).
2.85. CKApqAprApKqr. Restated: ((+p | +q) & (+p | +r)) ⇒ (+p | (+q & +r)).
2.86. EApKqrKApqApr. Restated: (+p | (+q & +r)) ⇒ ((+p | +q) & (+p | +r)); and ((+p | +q) & (+p | +r)); ⇒ (+p | (+q & +r)).
2.87. EKpAqrAKpqKpr. Restated: (+p & (+q | +r)) ⇒ ((+q & +r)| (+q & +r)); and ((+q & +r)| (+q & +r)) ⇒ (+p & (+q | +r)).
2.88. CCprCCCCrprrCCCpqrr. Restated: (+p ⇒ +r) ⇒ ((((+r ⇒ +p) ⇒ +r) ⇒ +r) ⇒ (((+p ⇒ +q) ⇒ +r) ⇒ +r)).
2.89. CCprCCCpqrr. Restated: (+p ⇒ +r) ⇒ (((+p ⇒ +q) ⇒ +r) ⇒ +r).
2.90. ApCpq. Restated: -p | (+p | +q).
2.91. CCCpqqApq. Restated: ((+p ⇒ +q) ⇒ +q) ⇒ (+p | +q).
2.92. EApqCCpqq. Restated: (+p | +q) ⇒ ((+p ⇒ +q) ⇒ +q); and ((+p ⇒ +q) ⇒ +q) ⇒ (+p | +q).
2.93. CCprCCCqrCCCrqqrCCqrCCCpqqr. Restated: (+p ⇒ +r) ⇒ (((+q ⇒ +r) ⇒ (((+r ⇒ +q) ⇒ +q) ⇒ +r)) ⇒ (((+q ⇒ +r) ⇒ (((+p ⇒ +q) ⇒ +q) ⇒ +r)))).
2.94. CCprCCqrCCCpqqr. Restated: (+p ⇒ +r) ⇒ ((+q ⇒ +r) ⇒ (((+p ⇒ +q) ⇒ +q) ⇒ +r)).
N1. CCpNpNp. Restated: ((p ⇒ -p) ⇒ -p).
N2. CNpCpq. Restated: (-p ⇒ (p ⇒ -q)).
2.95. CCpqCCqNpCpNp. Restated: (+p ⇒ +q) ⇒ ((+q ⇒ -p) ⇒ (+p ⇒ -p)).
2.96. CCpqCNqCpNp. Restated: (-p ⇒ q) ⇒ (-q ⇒ (p ⇒ -p)).
2.97. CCpqCNqNp. Restated: (p ⇒ q) ⇒ (-q ⇒ -p).
2.98. CCpqCCpCqNpCpNp. Restated: (+p ⇒ +q) ⇒ (+p ⇒ ((+q ⇒ -p)) ⇒ (+p ⇒ -p)).
2.99. CCpqCCpNqNp. Restated: (+p ⇒ +q) ⇒ ((+p ⇒ -q) ⇒ -p).
2.100. CqCCpNqNp. Restated: q ⇒ ((p ⇒ -q) ⇒ -p).
2.101. CCpNqCqNp. Restated: (p ⇒ -q) ⇒ (q ⇒ -p).
2.102. CpNNp. Restated: (+p ⇒ --p).
2.103. CNNNpNp. Restated: (---p ⇒ -p).
2.104. ENpNNNp. Restated: (-p = ---p) is (-p ⇒ ---p) and (---p ⇒ -p).
2.105. CNpCNNpq. Restated: -p ⇒ (--p ⇒ q).
2.106. CANpqCNNpq. Restated: (-p | +q) ⇒ (--p ⇒ +q).
2.107. CCNNpqCpq. Restated: (--p ⇒ +q) ⇒ (+p ⇒ +q).
2.108. CpCNqNCpq. Restated: p ⇒ (-q ⇒ -(+p ⇒ +q)).
2.109. CKpNqNCpq. Restated: (p & -q) ⇒ -(+p ⇒ +q).
2.110. CCpqNKpNq. Restated: (p ⇒ -q) ⇒ -(+p & +q).
2.111. CNNCpqNKpNq. Restated: --(+p ⇒ +q) ⇒ -(+p & -q).
2.112. CpCNqKpNq. Restated: +p ⇒ (-q ⇒ (+p & -q)).
2.113. CpCNKpNqNNq. Restated: ((+p ⇒ -(+p & -q)) ⇒ --q).
2.114. CNKpNqCpNNq. Restated: -(+p & -q) ⇒ (+p ⇒ --q).
2.115. CCpCqrCqCNNpNNr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ (+q ⇒ (--p ⇒ --r)).
2.116. CCpCqrCNNpCNNqNNNNr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ (--p ⇒ (--q ⇒ ----r)).
2.117. CCpCqrCNNpCNNqNNr. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ (--p ⇒ (--q ⇒ --r)).
2.118. CNNCpqCNNpNNq. Restated: --(+p ⇒ +q) ⇒ (--p ⇒ --q).
2.119. CCNNpNNqCpNNq. Restated: (--p ⇒ --q) ⇒ (+p ⇒ --q).
2.120. CCpCqrCCpCrsCpCqs. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+p ⇒ (+r ⇒ +s)) ⇒ (+p ⇒ (+q ⇒ +s))).
2.121. CCpCqrCCpNrCpNq. Restated: (+p ⇒ (+q ⇒ +r)) ⇒ ((+p ⇒ -r) ⇒ (+p ⇒ -p)).
2.122. CNCpqNNp. Restated: -(+p ⇒ +q) ⇒ --p.
2.123. CCpNqCCNqNpCpNp. Restated: (+p ⇒ -q) ⇒ ((-q ⇒ -p) ⇒ (+p ⇒ -p)).
2.124. CCpNqCCNqNpNp. Restated: (+p ⇒ -q) ⇒ ((-q ⇒ -p) ⇒ -p).
2.125. CNCpqNq. Restated: -(+p ⇒ +q) ⇒ -q.
2.126. CNCpqCCNqNpNp. Restated: -(+p ⇒ +q) ⇒ ((-q ⇒ -p) ⇒ -p).
2.127. CNCpqNCNqNp. Restated: -(+p ⇒ +q) ⇒ -(-q ⇒ -p).
2.128. CCpNNqNNCpq. Restated: (+p ⇒ --q) ⇒ --(+p ⇒ +q).
2.129. CKpqKNNpq. Restated: (+p & +q) ⇒ (--p & +q).
2.130. CCNNpNqNKNNpNNq. Restated: (--p ⇒ -q) ⇒ -(--p & --q).
2.131. CCpNqNKNNpq. Restated: (+p ⇒ -q) ⇒ -(--p & +q).
2.132. CKNNpqNCpNq. Restated: (--p & +q) ⇒ -(+p ⇒ -q).
2.133. CANpNqCpNq. Restated: (-p | -q) ⇒ (+p ⇒ -q).
2.134. CNCpNqNANpNq. Restated: -(+p ⇒ -q) ⇒ -(-p | -q).
2.135. CCNpNNpNNp. Restated: (-p ⇒ --p) ⇒ --p.
2.136. CCNppNNp. Restated: (-p ⇒ +p) ⇒ --p.
2.137. CCpqCCANpqrCpr. Restated: (+p ⇒ +q) ⇒ (((-p | +q) ⇒ +r) ⇒ (+p ⇒ +r)).
2.138. CCpqCNANpqNp. Restated: (+p ⇒ +q) ⇒ (-(-p | +q) ⇒ +p).
2.139. CCpqCNANpqANpq. Restated: (+p ⇒ +q) ⇒ (-(-p | +q) ⇒ (+p | +q)).
2.140. CCpqNNANpq. Restated: (+p ⇒ +q) ⇒ --(-p | +q).
2.141. CNANpNqNCpNq. Restated: -(-p | -q) ⇒ -(+p ⇒ -q).
2.142. CpCNKpqNq. Restated: +p ⇒ (-(+p & +q) ⇒ -q).
2.143. CNKpqCpNq. Restated: -(+p & +q) ⇒ (+p ⇒ -q).
2.144. CNANpNqNNKpq. Restated: -(-p | -q) ⇒ --(+p & -q).
2.145. CNNKpqNNp. Restated: --(+p & -q) ⇒ --p.
2.146. CNNKpqNNq. Restated: --(+p & -q) ⇒ --q.
2.147. CNNKpqKNNpNNq. Restated: --(+p & -q) ⇒ (--p & --q).
2.148. CCpNqCNNpNq. Restated: (+p ⇒ -q) ⇒ (--p ⇒ -q).
2.149. CNNpCCpNqNq. Restated: --p ⇒ ((+p ⇒ -q) ⇒ -q).
2.150. CNNpCNNqNCpNq. Restated: --p ⇒ (--q ⇒ (--p ⇒ -q)).
2.151. CKNNpNNqNCpNq. Restated: (--p & --q) ⇒ -(+p ⇒ -q).
2.152. ENNEpqKNNCpqNNCqp.................
2.153. CCpNqNKpq. Restated: (+p ⇒ -q) ⇒ -(+p & +q).
2.154. CANpNqNKpq. Restated: (-p | -q) ⇒ -(+p & +q).
2.155. CNApqNp. Restated: -(+p | +q) ⇒ -p.
2.156. CNApqNq. Restated: -(+p | +q) ⇒ -q.
2.157. CNApqKNpNq. Restated: -(+p | +q) ⇒ (-p & -q).
2.158. CNpCApqq. Restated: -p ⇒ ((+p | +q) ⇒ +q).
2.159. CNpCNqNApq. Restated: -p ⇒ (-q ⇒ -(+p | +q)).
2.160. CKNpNqNApq. Restated: ((-p & -q) ⇒ (+p | +q).
2.161. ENApqKNpNq. (DeMorgan's Law.) Restated: -(+p | +q) ⇒ (-p & -q); and (-p & -q) ⇒ -(+p | +q).
2.162. CApqCCpqq. Restated: ((+p | +q) ⇒ ((+p ⇒ +q) ⇒ +q).
2.163. CCCpqqCCpqq. Restated: ((+p ⇒ +q) ⇒ +q) ⇒ ((+p ⇒ +q) ⇒ +q).
2.164. CCCpqqCNpq. Restated: ((+p ⇒ +q) ⇒ +q) ⇒ (-p ⇒ +q).
2.165. CCNpqNKNpNq. Restated: (-p ⇒ +q) ⇒ -(-p & -q).
2.166. CCNppp. Restated: ((-p ⇒ +p) ⇒ +p).
2.167. CNNpp. Restated: (--p ⇒ +p).
2.168. EpNNp. Restated: (+p = --p) is (+p ⇒ --p) and (--p ⇒ p).
2.169. CCNpNqCNNqNNp. Restated: (-p ⇒ -q) ⇒ (--q ⇒ --p).
2.170. CCNpNqCqp. Restated: (-p ⇒ -q) ⇒ (+q ⇒ +p).
2.171. CCNpNNqCNqp. Restated: (-p ⇒ --q) ⇒ (-q ⇒ +p).
2.172. CCNpqCNqp. Restated: (-p ⇒ +q) ⇒ (-q ⇒ +p).
2.173. ApNp. Restated: (+p | -p).
2.174. CCpqANpq. Restated: (+p ⇒ +q) ⇒ (-p | +q).
2.175. CNNCpqANpq. Restated: --(+p ⇒ +q) ⇒ (-p | +q).
2.176. CNNKpqKpq. Restated: --(+p & +q) ⇒ (+p & +q).
2.177. CNKNpNqApq. Restated: -(-p & -q) ⇒ (+p | +q).
2.178. EANpNqNKpq. (DeMorgan's Law.) Restated: (-p | -q) ⇒ -(+p & +q); and -(+p & +q) ⇒ (-p | -q).
CN1. CCpqCCqrCpr. Restated: (+p ⇒ +q) ⇒ ((+q ⇒ +r) ⇒ (+p ⇒ +r)).
CN2. CpCNpq. Restated: (+p ⇒ (-p ⇒ +q)).
CN3. CCNppp. Restated: ((-p ⇒ +p) ⇒ +p).
KN1. CpKpp. Restated: (+p ⇒ (+p & +p)).
KN2. CKpqp. Restated: ((+p & +q) ⇒ +p).
KN3. CCpqCNKqrNKrp. Restated: (+p ⇒ +q) ⇒ (-(+q & +r) ⇒ -(+r & +p)).
5.72. CLKpqLp. Restated: (+□(+p&+q)) ⇒ +□+p.
5.73. CLKpqLp. Restated: (+□(+p&+q)) ⇒ +□+q.
5.74. CLKpqKLpLq. Restated: (+□(+p&+q)) ⇒ (+□+p & +□+q).
5.78. CLpCLqLKpq. Restated: (+□+p) ⇒ ((+□+q) ⇒ (+□(+p&+q)).
5.79. CKLpLqLKpq. Restated: (+□+p &+□+q) ⇒ (+□(+p &+q)).
5.80. ELKpqKLpLq. Restated: +□(+p&+q) ⇔ (+□+p & +□+q).
5.83. CALpLqLApq. Restated: (+□+p|+□+q) ⇒ +□(+p|+q). I CAN'T MAKE THIS PROOF WORK, ALTHOUGH I CAN PROVE THE CONVERSE.

NOTE: CpLp is not necessarily true, but CpMp is always true in GWM modal logic. However (Zeman, p. 89), there are some modal logics where CpMp is not necessarily true.

ADDITIONAL GWMML THEOREMS AND PROOFS.

GWM1. CpMp. +p ⇒ +◇+p.
Restated: Nandset {+p,+$p,-p} is vacuous.

GWM2. CLpLp. +□+p ⇒ +□+p.
Restated: Nandsets {-$p,-p,+$p} and {-$p,-p,+p} are vacuous.

GWM3. CLpMp. +□+p ⇒ +◇+p.
Restated: Nandset {-$p,-p,+$p,+p} is vacuous.

GWM4. CCLpMNpLNp. ((+□+p ⇒ +◇+p) ⇒ +◇+p).
Last updated: 3/7/3008, by G. William Moore, MD, PhD.