Axioms for Equivalential Calculus

=========================================================

Rules:
(S) The substitution rule is defined in a standard way.
(D) $E\alpha\beta, \alpha\vdash \beta$
(RD) $E\alpha\beta, \beta\vdash \alpha$

=========================================================
Rules: S+D 

---------------
Sets of axioms:

A1. Epp
A2. EEpqEqp
A3. EEEpqEqrEpr

(wajsberg1932)  (cf. Yoshinari1966)
W1a. EEEpqrEpEqr
W2a. EEpqEqp

(wajsberg1932)(cf. Yoshinari1966)
W1b. EEpEqrErEqp 
W2b. EEEpppp 

(wajsberg1937)
W1a'. EEpEqrEEpqr (lesniewski1929)
W2a. EEpqEqp

--------------
Single axiom:

(wajsberg1932)
EEEpEqrEErssEpq

(wajsberg1932)
EEEEpqrsEsEpEqr 

Bryman
EEpEqrEEqEsrEsp

(sobocinski1932)
EEpEqrEEpErsEsq

(sobocinski1932)
EEpEqrEEpEsrEsq

(sobocinski1932)
EEpEqrEEpErsEqs

(lukasiewicz1939)
EEpEqrEEqErsEsp

(lukasiewicz1939)
EEsEpEqrEEpqErs
    

--------------
Single 11 characters long axiom:

(lukasiewicz1939) 
YQL. EEpqEErqEpr
YQF. EEpqEEprErq
YQJ. EEpqEErpEqr

(meredith1963)
UM. EEEpqrEqErp
XGF. EpEEqEprErq
WN. EEpEqrErEpq
YRM. EEpqErEEqrp
YRO. EEpqErEErqp
PYO. EEEpEqrrEqp
PYM. EEEpEqrqErp

(kalman1978)
XGK. EpEEqErpErq

(wos1983) 
XHK. EpEEqrEEprq
XHN. EpEEqrEErpq

(wos2003) 
XCB. EpEEEpqErqr


=========================================================
Rules: S+RD 

---------------
Sets of axioms:

Theorem: A set A is a set of axioms for Equivalential Calculus with rules S and RD if and only if a set A^D (consisted of dual formulas of the set A) ia a set of axioms for Equivalential Calculus with rules S and D. 

Wajsberg dual axioms:
W1b^D. EEEpqrEErqp
W2b'. EpEpEpp

---------------
Single 11 characters long axiom:
QYK. EEEpqErpErq
QYH. EEEpqEqrEpr
QYJ. EEEpqErpEqr
UM. EEEpqrEqErp
HXH. EEEpqEEqrpr
TN. EEEpqrEErpq
PYM. EEEpEqrqErp
PYO. EEEpEqrrEqp
YRO. EEpqErEErqp
YRM. EEpqErEEqrp
HXL. EEEpqEErqpr
GXL. EEEpEqrEqpr
GXN. EEEpEqrErpq
MXD. EEpEqEEpqrr

=========================================================
Rules: S+D+RD 

---------------
Single 11 characters long axiom:
{Hodgson1998}
YPG. EEpqEEqEprr
RYC. EEpEEpqrErq
CXM. EEEEpqErqrp
XLM. EpEqEErqErp
DXM. EEEEpqrEqrp 
XIM. EpEEqrEqErp
OYJ. EEEEpqrpEqr
YSJ. EEpqErEpEqr
UJ. EEEpqrEpEqr
VJ. EEpEqrEEpqr
VN. EEpEqrEErpq


Open problems:
{czakon2025}
BXO. EEEEpEqrrqp
XMO. EpEqErEErqp
XBC. EpEEEpEqrrq
MXG. EEpEqEEqprr
XDB. EpEEEpqrEqr
IXD. EEEpqEpEqrr