The equivalential fragment EQ of classical logic was first axiomatized by Leśniewski, using substitution and E-detachment ("From Eαβ and α, infer β") as rules together with the axioms EEEpqErpEqr / ((pq)(rp))(qr) and EEpEqrEEpqr / (p(qr))((pq)r).  One of the most useful alternate two-bases found since is the pair {EEpqEEqrEpr, EEpqEqp}, that is, {(pq)((qr)(pr)), (pq)(qp)}.
          The first single axioms for EQ were discovered by Wajsberg (EEEpEqrEErssEpq and EEEEpqrsEsEpEqr, each 15 symbols in length).  Łukasiewicz then found three single axioms of length 11, and proved that they were shortest possible using six distinct matrices [there is an alternative proof, using a single matrix, in D. Ulrich, A five-valued model of the E-p-q theses, Notre Dame Journal of Formal Logic, vol. 29 (1988), pp. 137-138].  C. A. Meredith found seven additional axioms of length 11, and J. A. Kalman another (though he presents it as simply correcting a typographical error in an eighth one reported by Meredith).  Winker found two more, and the 14th was found by Wos, Ulrich, and Fitelson as reported in the UPDATE to  Question D on the Twenty-six open questions page.
          I note that the following list of single axioms for EQ of length 11 is complete, all other theorems of EQ of this length having been ruled out earlier, most by J. G. Peterson [The possible shortest single axioms for EC-tautologies, Report No. 105, University of Auckland, Department of Mathematics] and the rest by Wos et. al [Questions concerning possible shortest single axioms for the equivalential calculus: An application of automated theorem proving in infinite domains, Notre Dame Journal of Formal Logic, vol. 24 (1983), pp. 205-223].
          The names used below for EQ theorems of length 11 follow the conventions worked out by J. A. Kalman and have now become standard.  Click here for a detailed account of those conventions.

               EEpqEErqEpr / (pq)[(rq)(pr)]  (YQL)
              
EEpqEEprErq / (pq)[(pr)(rq)]  (YQF)
              
EEpqEErpEqr / (pq)[(rp)(qr)]  (YQJ)
              
EEEpqrEqErp / [(pq)r][q(rp)]  (UM)
              
EpEEqEprErq / p{[q(pr)](rq)}  (XGF)
              
EEpEqrErEpq / [p(qr)][r(pq)]  (WN)
              
EEpqErEEqrp / (pq){r[(qr)p]}  (YRM)
              
EEpqErEErqp / (pq){r[(rq)p]}  (YRO)
              
EEEpEqrrEqp / {[p(qr)]r}(qp)  (PYO)
              
EEEpEqrqErp / {[p(qr)]q}(rp)  (PYM)
              
EpEEqErpErq / p{[q(rp)](rq)}  (XGK)
              
EpEEqrEEprq / p{(qr)[(pr)q]}  (XHK)
              
EpEEqrEErpq / p{(qr)[(rp)q]}  (XHN)
               EpEEEpqErqr / p
{[(pq)(rq)]r}  (XCB)

Meredith also found several single axioms for EQ when the rule of detachment is replaced by reverse detachment ("From E
αβ and β, infer α").  Clearly a formula is a single axiom for EQ when this rule is used just in case it results from one of the fourteen formulas listed above by replacing each subformula in the latter of the form Eαβ with the corresponding formula of the form Eβα.  The list of all single axioms under the reverse detachment rule is then as follows:

               EEEpqrEqErp / [(pq)r][q(rp)]  (UM)
               EEpqErEEqrp / (p
q){r[(qr)p]}  (YRM)
               EEpqErEErqp / (p
q){r[(rq)p]}  (YRO)
               EEEpEqrrEqp / {[p
(qr)]r}(qp)  (PYO)
               EEEpEqrqErp / {[p
(qr)]q}(rp)  (PYM)
               EEEpqErpErq / [(p
q)(rp)](rq)  (QYK)
               EEEpqEqrEpr / [(p
q)(qr)](pr)  (QYH)
               EEEpqErpEqr / [(p
q)(rp)](qr)  (QYJ)
               EEEEpqEqrpr / {[(p
q)(qr)]p}r  (HXH)
               EEEpqrEErpq / [(p
q)r][(rp)q]  (TN)
               EEEpqEErqpr / {(p
q)[(rq)]p]}r  (HXL)
               EEEpEqrEqpr / {[p
(qr)](qp)}r  (GXL)
               EEEpEqrErpr / {[p
(qr)](rp)}q  (GXN)
               EEpEEqpEqrr / {p
[(qp)(qr)]}r  (LXD)

Kahlil Hodgson [Shortest single axioms for the equivalential calculus with CD and RCD, Journal of Automated Reasoning, vol. 20 (1998), pp. 283-316], working with Kalman, has investigated the single axioms for EQ of length 11 when both detachment and reverse detachment are used as rules.  The list of all such axioms is presently incomplete.  It certainly includes the twenty-three distinct formulas appearing on the two lists displayed above, plus the following eleven formulas discovered by Hodgson:

               EEpqEEqEprr / (p
q){[q(pr)]r}  (YPG)
               EEpEEpqrErq / {p
[(pq)r]}(rq)  (RYC)
               EEEEpqErqrp / {[(p
q)(rq)]r}p  (CXM)
               EpEqEErqErp / p
{q[(rq)(rp)]}  (XLM)
               EEEEpqrCqrp / {[(p
q)r](qr)}p  (DXM)
               EpEEqrEqErp / p
{(qr)[q(rp)]}  (XIM)
               EEEEpqrpEqr / {[(p
q)r]p}(qr)  (OYJ)
               EEpqErEpEqr / (p
q){r[p(qr)]}  (YSJ)
               EEEpqrEpEqr / [(p
q)r][p(qr)]  (UJ)
               EEpEqrEEpqr / [p
(qr)][(pq)r]  (VJ)
               EEpEqrEErpq / [p
(qr)][(rp)q]  (VN)

But in addition to XCB and LXD (whose standing was undetermined thenadays), Hodgson left as open questions the status of eight other formulas:

 

     
    OPEN QUESTIONS
Is BXO = EEEEpEqrrqp / [{[p(qr)]r}q]p a single axiom for EQ when both detachment and reverse detachment are rules?
Is XMO
= EpEqErEErqp / p[q{r[(rq)p]}] a single axiom for EQ when both detachment and reverse detachment are rules?
Is AXL
= EEEEEpqrqpr / [{[(pq)r]q}p]r a single axiom for EQ when both detachment and reverse detachment are rules?

UPDATE: Despite Hodgson's remark that any matrix showing that AXL is not a single axiom must contain at least seven values, I showed (at AWARD 2004) that the following six-valued matrix does the job by validating AXL as well as both rules but rejecting the EQ theorem EEpqEEqrEpr / (pq)((qr)(pr)):

                                                    E | 1 2 3 4 5 6 .
                                                  *1  | 1 1 4 4 4 4
                                                  *2 | 1 1  3 6 5 6
                                                    3 | 3 3 2 5 6 5
                                                    4 | 4 4  1 1 1  1
                                                    5 | 5 5 6 3 2 3
                                                    6 | 6 6 5 2 3 2
Is XNK
= EpEqErEpErq / p[q{r[p(rq)]}] a single axiom for EQ when both detachment and reverse detachment are rules?

UPDATE: Similarly, I showed that XNK is not a single axiom via the matrix


                                                    E | 1 2 3 4 5 6 .
                                                  *1  | 1 2 3 4 5 6
                                                  *2 | 1 2 3 4 5 6
                                                    3 | 3 4 1 2 6 5
                                                    4 | 5 4 6 2 1 3
                                                    5 | 5 4 6 2 1 3
                                                    6 | 6 4 5 2 3 1

Is XBC = EpEEEpEqrrq / p[{[p(qr)]r }q] a single axiom for EQ when both detachment and reverse detachment are rules?
Is MXG
= EEpEqEEqprr / [p{q[(qp)r]}]r a single axiom for EQ when both detachment and reverse detachment are rules?
Is XDB
= EpEEEpqrEqr / p{[(pq)r](qr)} a single axiom for EQ when both detachment and reverse detachment are rules?
Is IXD
= EEEpqEpEqrr / {(pq)[p(qr)]}r a single axiom for EQ when both detachment and reverse detachment are rules? 

 © Dolph Ulrich, 2007


 Entrance page | Home page | Twenty-six open questions |

Single axioms for:  | BCI | 4 subsystems of BCI | monothetic BCI | C-pure R | C-pure R-Mingle | C-pure LNo |
   
| BCK | C-pure intuitionism | Classical equivalence | A few more systems |

| D-complete axioms for (classical) equivalence | Exit page |