Single Axioms and Axiom-Pairs for the Implicational Fragments of $\mathbf {R}$, R-Mingle, and Some Related Systems

Abstract

Various axiom sets for the implicational fragments $\mathbf {R}_\rightarrow$ and $\mathbf {RM}_\rightarrow$ of $\mathbf {R}$ and of R-Mingle have appeared in the literature over the last six-and-a-half decades, some of them in other guises well before the full systems with $\sim$, &, and $\vee$ were even introduced. Most such sets are comprised of three or four axioms. For other logics of pure implication, the historical progression has typically been from longer axiom sets to the discovery of deductively equivalent two- and one-axiom bases. This paper continues in that pattern, presenting such bases for $\mathbf {R}_\rightarrow$ and $\mathbf {RM}_\rightarrow$. Along the way, new axiom pairs and new single axioms are given for a number of other implicational logics as well, some in the paper itself and many in the Appendix attached to it. Prominent among these is C.A. Meredith’s system $\mathbf {BCI}$. Though single axioms for $\mathbf {BCI}$ are of independent interest, one of them in particular also plays an invaluable role in the construction of those provided here for implicational $\mathbf {R}$ and R-Mingle.

Appendix: Axiom Sets for Some Implicational Logics

Modus ponens (i.e., detachment) and uniform substitution of formulas for sentence letters are the rules of inference throughout all sections. Names for axioms are handled as follows. When an axiom involved in any of the systems below first appears, what the author takes to be the most commonly used name for it (if such exists) is listed first, with alternate names appended thereafter. When such an axiom is also used in axiom sets farther down the list, he is occasionally inconsistent: usually only the name taken to be most common is used, but sometimes, when a reminder seems to be in order, the formula it names is repeated.

Axiom sets discovered before 1961 for several of the logics appearing here are given in the Appendix to Prior’s Formal Logic (Prior 1962). There is some overlap, but the author has tried to minimize the duplication whence readers interested in seeing more axiomatizations are encouraged to consult Prior. Several of the early results, especially those from Tarski, Łukasiewicz, Wajsberg, and C.A. Meredith, were obtained considerably earlier than the date of the reference cited below in which they first appeared in the literature. Prior’s Appendix gives approximate years in several such cases.

Results not attributed below to others are, barring accidental omissions, believed by the author to be new.

A.1 IF: The implicational fragment of the classical sentential calculus

Four-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!/\mathbf {Syll}/\mathbf {Syl}\,=(p\rightarrow q)\rightarrow ((q\rightarrow r)\rightarrow (p\rightarrow r))$,  $\mathbf {C}/\mathbf {Com}=(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow (p\rightarrow r))$,  $\mathbf {I}/\mathbf {Id}=p\rightarrow p$,  $\mathbf {Peirce}=((p\rightarrow q)\rightarrow p)\rightarrow p$    [in Peirce (1885)]

Three-bases:   $\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {K}/\mathbf {Simp}=p\,{\rightarrow }\,(q\,{\rightarrow }\, p)$,  $\mathbf {Tarski}=((p\,{\rightarrow }\, q)\rightarrow r)\rightarrow ((p\rightarrow r)\rightarrow r)$   [Tarski, Bernays circa 1921; cf. Łukasiewicz and Tarski (1930)]

$\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {K},{\,\,}\mathbf {Peirce}$   [circa 1926; ibid.]

Two-bases:  $p\,{\rightarrow }\,(q\,{\rightarrow }\,(r\rightarrow p))$,  $((p{\rightarrow } q){\rightarrow } r)\rightarrow ((s\rightarrow r)\rightarrow ((p\rightarrow r){\rightarrow } r))$    [Wajsberg (1932) but circa 1925–1926; cf. Prior (1962, p. 302)]

$\mathbf {Peirce},{\,\,}(((p\rightarrow q)\rightarrow r)\rightarrow s)\rightarrow ((q\rightarrow r)\rightarrow (p\rightarrow s))$   [Wajsberg circa 1925–1926; ibid.]

$\mathbf {K},{\,\,}(((p\rightarrow q)\rightarrow r)\rightarrow s)\rightarrow ((q\rightarrow s)\rightarrow (p\rightarrow s))$      [Łukasiewicz circa 1926; cf. Łukasiewicz and Tarski (1930)]

$\mathbf {Peirce},{\,\,}(p\rightarrow q)\rightarrow (s\rightarrow ((q\rightarrow r)\rightarrow (p\rightarrow r)))$   [Wajsberg (1939)]

$((p\rightarrow q)\rightarrow p)\rightarrow (r\rightarrow p),{\,\,}\mathbf {B}^{_{\textstyle \texttt {'}}}$   [Wajsberg (1939)]

$\mathbf {K},{\,\,}((p\,{\rightarrow }\, q)\,{\rightarrow }\, r)\,{\rightarrow }\,((r\rightarrow p)\rightarrow (s\rightarrow (t\rightarrow p)))$   [Meredith circa 1956, in Lemmon et al. (1969)]

$\mathbf {K},{\,\,}\mathbf {M2}=(((p\rightarrow q)\rightarrow r)\rightarrow q)\rightarrow ((q\rightarrow s)\rightarrow (p\rightarrow s))$   [Prior circa 1960; cf. Prior (1961)]

$\mathbf {I},{\,\,}((p\rightarrow q)\rightarrow r)\rightarrow (((q\rightarrow s)\rightarrow t)\rightarrow ((t\rightarrow q)\rightarrow r))$

$\mathbf {I}$ with any one of $(p\rightarrow q)\rightarrow (((p\rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow q)\rightarrow (t\rightarrow q)))$,  $(p\rightarrow q)\,{\rightarrow }\,(((q \rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow p)\rightarrow (t\rightarrow q)))$,  $(p\rightarrow q)\rightarrow (((r\rightarrow s)\rightarrow p)\rightarrow ((r\rightarrow p)\rightarrow (t\rightarrow q)))$, or $(p\rightarrow q)\rightarrow (((r\rightarrow s)\rightarrow q)\rightarrow ((r\rightarrow p)\,{\rightarrow }\,(t\rightarrow q)))$,  and probably others, will also do.

$\mathbf {I},{\,\,}((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow p)\rightarrow (s\rightarrow (t\rightarrow p)))$   [Meredith; see Prior (1961).]

One-bases:  $((p\rightarrow q)\rightarrow ((r\rightarrow s)\rightarrow t))\rightarrow ((u\rightarrow ((r\rightarrow s)\rightarrow t))\rightarrow ((p\rightarrow u)\rightarrow (s\rightarrow t)))$   [Wajsberg circa 1926; cf. Łukasiewicz and Tarski (1930).]

$((p\,{\rightarrow }\,(q\,{\rightarrow }\, p))\,{\rightarrow }\,(((((r\rightarrow s)\rightarrow t)\rightarrow u)\rightarrow ((s\rightarrow u)\rightarrow (r\rightarrow u)))\rightarrow v))\rightarrow v$   [Łukasiewicz; ibid.]

$((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow (t\rightarrow ((s\rightarrow p)\rightarrow (r\rightarrow p)))$   [in Łukasiewicz (1948), but discovered earlier.]

$((p\,{\rightarrow }\, q)\,{\rightarrow }\,(r\,{\rightarrow }\, s))\,{\rightarrow }\,((s\,{\rightarrow }\, p)\,{\rightarrow }\,(t\rightarrow (r\rightarrow p)))$   [also in Łukasiewicz (1948), and also discovered earlier.]

$(p\rightarrow (q\rightarrow r))\rightarrow ((r\rightarrow p)\rightarrow (s\rightarrow p))$      [Łukasiewicz (1948), but discovered in 1936.]

$\mathbf {A.2{\,\,}BCI}$

Three-bases:  $\mathbf {B}=(p\rightarrow q)\rightarrow ((r\rightarrow p)\rightarrow (r\rightarrow q))$,  $\mathbf {C}=(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow (p\rightarrow r))$,  $\mathbf {I}$   [Meredith; cf. Prior (1962, p. 302). $\mathbf {BCI}$ turns out to be the implicational fragment of linear logic from Girard (1987).]

$\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {C},{\,\,}\mathbf {I}$   [An obvious variant of the preceding base.]

$\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {Pon}/\mathbf {Assertion}/\mathbf {T}=p\rightarrow ((p\rightarrow q)\rightarrow q),{\,\,}\mathbf {I}$   [Another variant.]

Two-bases:  $\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-1 $=(((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow s)\rightarrow (p\rightarrow s)),{\,\,}\mathbf {I}$

$\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-2 $=(p\rightarrow q)\rightarrow ((((r\rightarrow s)\rightarrow s)\rightarrow p)\rightarrow (r\rightarrow q)),{\,\,}\mathbf {I}$

$(p\rightarrow q)\rightarrow ((((q\rightarrow r)\rightarrow r)\rightarrow s)\rightarrow (p\rightarrow s)),{\,\,}\mathbf {I}$

$(p\rightarrow (q\rightarrow r))\rightarrow ((t\rightarrow q)\rightarrow (t\rightarrow (p\rightarrow r))),{\,\,}\mathbf {I}$

$\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-1 and $\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-2 are the only theorems of $\mathbf {BCI}$ (or even of $\mathbf {IF}$) of length 15 or less that give all of $\mathbf {B}$, $\mathbf {B}^{_{\textstyle \texttt {'}}}\!$, and $\mathbf {C}$. Each is a single axiom for the system (also new) whose axioms are $\mathbf {B}$ and either $(((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow s)\rightarrow (p\rightarrow s))$ or $(((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow (p\rightarrow ((r\rightarrow s)\rightarrow s))$ (equivalently, $\mathbf {B}^{_{\textstyle \texttt {'}}}$ and either; $\mathbf {C}$ and either).

One-bases:  BCI-1 $= (p\,{\rightarrow }\,(q\,{\rightarrow }\, r))\,{\rightarrow }\,(((s\rightarrow s)\rightarrow (t\rightarrow q))\rightarrow (t\rightarrow (p\rightarrow r)))$

BCI-2 $=((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow ((s\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow (s\rightarrow t)))$

BCI-1 is Meredith’s circa 1956, and BCI-2 is Prior’s; see Meredith and Prior (1963). The 78 additional single axioms for $\mathbf {BCI}$ below are new.

BCI-3.  $(p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (((q\rightarrow s)\rightarrow s)\rightarrow t))\rightarrow (p\rightarrow t))$

BCI-4.  $(p\rightarrow q)\rightarrow ((q\rightarrow ((r\rightarrow r)\rightarrow (s\rightarrow t)))\rightarrow (s\rightarrow (p\rightarrow t)))$

BCI-5.  $((((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow t)\rightarrow (q\rightarrow t))$

BCI-6.  $(((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow (((s\rightarrow s)\rightarrow (r\rightarrow t))\rightarrow (p\rightarrow t))$

BCI-7.  $(p\rightarrow (q\rightarrow r))\rightarrow (((((s\rightarrow s)\rightarrow p)\rightarrow r)\rightarrow t)\rightarrow (q\rightarrow t))$

BCI-8.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow s)\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow (p\rightarrow t)))$

BCI-9.  $((p\rightarrow p)\rightarrow (((q\rightarrow r)\rightarrow r)\rightarrow s))\rightarrow ((s\rightarrow t)\rightarrow (q\rightarrow t))$

BCI-10.  $((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow ((r\rightarrow (s\rightarrow t))\rightarrow (q\rightarrow t)))$

BCI-11.  $((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow ((((r\rightarrow s)\rightarrow s)\rightarrow t)\rightarrow (q\rightarrow t))$

BCI-12.  $((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow ((r\rightarrow (s\rightarrow t))\rightarrow (s\rightarrow (q\rightarrow t)))$

BCI-13.  $(p\rightarrow ((q\rightarrow q)\rightarrow (r\rightarrow s)))\rightarrow ((s\rightarrow t)\rightarrow (r \rightarrow (p\rightarrow t)))$

BCI-14.  $(p\rightarrow ((q\rightarrow q)\rightarrow r))\rightarrow (s\rightarrow ((r\rightarrow (s\rightarrow t)) \rightarrow (p\rightarrow t)))$

BCI-15.  $(p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (q\rightarrow (s\rightarrow t)))\rightarrow (s\rightarrow (p\rightarrow t)))$

BCI-16.  $(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow (((s\rightarrow s)\rightarrow (r\rightarrow t)) \rightarrow (p\rightarrow t)))$

BCI-17.  $p\rightarrow (((q\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow ((s\rightarrow (p\rightarrow t)) \rightarrow (r\rightarrow t)))$

BCI-18.  $p\rightarrow ((q\rightarrow (p\rightarrow r))\rightarrow (((s\rightarrow s)\rightarrow (r\rightarrow t)) \rightarrow (q\rightarrow t)))$

BCI-19.  $(p\rightarrow q)\rightarrow (r\rightarrow (((s\rightarrow s)\rightarrow (q\rightarrow (r\rightarrow t))) \rightarrow (p\rightarrow t)))$

BCI-20.  $((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow ((((s\rightarrow t)\rightarrow t)\rightarrow q)\rightarrow (s\rightarrow r))$

BCI-21.  $p\rightarrow (((q\rightarrow q)\rightarrow (r\rightarrow (p\rightarrow s)))\rightarrow ((t\rightarrow r) \rightarrow (t\rightarrow s)))$

BCI-22.  $((p\rightarrow p)\rightarrow (q\rightarrow (r\rightarrow s)))\rightarrow ((t\rightarrow q)\rightarrow (r\rightarrow (t\rightarrow s)))$

BCI-23.  $(p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (((s\rightarrow p)\rightarrow q)\rightarrow t))\rightarrow (s\rightarrow t))$

BCI-24.  $(p\rightarrow ((q\rightarrow q)\rightarrow (r\rightarrow s)))\rightarrow ((t\rightarrow p)\rightarrow (r\rightarrow (t\rightarrow s)))$

BCI-25.  $((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow ((((s\rightarrow q)\rightarrow r)\rightarrow t)\rightarrow (s\rightarrow t))$

BCI-26.  $((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow ((s\rightarrow (t\rightarrow q))\rightarrow (t\rightarrow (s\rightarrow r)))$

BCI-27.  $(p\rightarrow ((q\rightarrow q)\rightarrow r))\rightarrow ((r\rightarrow (s\rightarrow t))\rightarrow (s\rightarrow (p\rightarrow t)))$

BCI-28.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow s)\rightarrow (t\rightarrow p))\rightarrow (q\rightarrow (t\rightarrow r)))$

BCI-29.  $((p\rightarrow p)\rightarrow (q\rightarrow (r\rightarrow s)))\rightarrow ((s\rightarrow t)\rightarrow (r\rightarrow (q\rightarrow t)))$

BCI-30.  $((p\rightarrow p)\rightarrow (q\rightarrow (r\rightarrow s)))\rightarrow ((t\rightarrow r)\rightarrow (t\rightarrow (q\rightarrow s)))$

BCI-31.  $((p\rightarrow p)\rightarrow (q\rightarrow (r\rightarrow s)))\rightarrow (r\rightarrow ((s\rightarrow t) \rightarrow (q\rightarrow t)))$

BCI-32.  $((p\rightarrow p)\rightarrow (q\rightarrow (r\rightarrow s)))\rightarrow (r\rightarrow ((t\rightarrow q) \rightarrow (t\rightarrow s)))$

BCI-33.  $((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow ((s\rightarrow (r\rightarrow t)) \rightarrow (s\rightarrow t)))$

BCI-34.  $(p\rightarrow ((q\rightarrow q)\rightarrow (r\rightarrow s)))\rightarrow ((t\rightarrow r)\rightarrow (t\rightarrow (p\rightarrow s)))$

BCI-35.  $(p\rightarrow (q\rightarrow r))\rightarrow ((s\rightarrow ((t\rightarrow t)\rightarrow p))\rightarrow (q\rightarrow (s\rightarrow r)))$

BCI-36.  $(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow (((s\rightarrow s)\rightarrow (t\rightarrow p)) \rightarrow (t\rightarrow r)))$

BCI-37.  $(p\rightarrow q)\rightarrow (((((r\rightarrow r)\rightarrow (s\rightarrow t))\rightarrow t)\rightarrow p)\rightarrow (s\rightarrow q))$

BCI-38.  $(p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (s\rightarrow (q\rightarrow t)))\rightarrow (p\rightarrow (s\rightarrow t)))$

BCI-39.  $(p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (s\rightarrow (t\rightarrow p)))\rightarrow (t\rightarrow (s\rightarrow q)))$

BCI-40.  $(p\rightarrow q)\rightarrow ((r\rightarrow ((s\rightarrow s)\rightarrow (q\rightarrow t)))\rightarrow (p\rightarrow (r\rightarrow t)))$

BCI-41.  $(p\rightarrow q)\rightarrow (r\rightarrow (((s\rightarrow s)\rightarrow (t\rightarrow (r\rightarrow p))) \rightarrow (t\rightarrow q)))$

BCI-42.  $p\rightarrow ((q\rightarrow ((r\rightarrow r)\rightarrow (p\rightarrow s)))\rightarrow ((s\rightarrow t) \rightarrow (q\rightarrow t)))$

BCI-43.  $p\rightarrow (((q\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow ((t\rightarrow (p\rightarrow r)) \rightarrow (t\rightarrow s)))$

BCI-44.  $p\rightarrow ((q\rightarrow ((r\rightarrow r)\rightarrow (p\rightarrow s)))\rightarrow ((t\rightarrow q) \rightarrow (t\rightarrow s)))$

BCI-45.  $p\rightarrow ((q\rightarrow ((r\rightarrow r)\rightarrow s))\rightarrow ((s\rightarrow (p\rightarrow t)) \rightarrow (q\rightarrow t)))$

BCI-46.  $(p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow (((t\rightarrow t)\rightarrow (s\rightarrow q)) \rightarrow (p\rightarrow r)))$

BCI-47.  $(p\rightarrow q)\rightarrow ((r\rightarrow ((s\rightarrow s)\rightarrow (t\rightarrow p)))\rightarrow (t \rightarrow (r\rightarrow q)))$

BCI-48.  $p\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (((t\rightarrow t)\rightarrow (p\rightarrow r)) \rightarrow (q\rightarrow s)))$

BCI-49.  $p\rightarrow ((q\rightarrow r)\rightarrow (((s\rightarrow s)\rightarrow (r\rightarrow (p\rightarrow t))) \rightarrow (q\rightarrow t)))$

BCI-50.  $((((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow s)\rightarrow ((q\rightarrow (t\rightarrow r))\rightarrow (t\rightarrow s))$

BCI-51.  $(((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow (((s\rightarrow s)\rightarrow (t\rightarrow p))\rightarrow (t\rightarrow r))$

BCI-52.  $(((p\rightarrow q)\rightarrow r)\rightarrow s)\rightarrow (((t\rightarrow t)\rightarrow (q\rightarrow r))\rightarrow (p\rightarrow s))$

BCI-53.  $((p\rightarrow p)\rightarrow (((q\rightarrow r)\rightarrow r)\rightarrow s))\rightarrow ((t\rightarrow q)\rightarrow (t\rightarrow s))$

BCI-54.  $((p\rightarrow p)\rightarrow (((q\rightarrow r)\rightarrow s)\rightarrow t))\rightarrow ((r\rightarrow s)\rightarrow (q\rightarrow t))$

BCI-55.  $(p\rightarrow q)\rightarrow (p\rightarrow (((r\rightarrow r)\rightarrow (s\rightarrow (q\rightarrow t)))\rightarrow (s\rightarrow t)))$

BCI-56.  $p\rightarrow ((q\rightarrow (p\rightarrow r))\rightarrow (((s\rightarrow s)\rightarrow (t\rightarrow q))\rightarrow (t\rightarrow r)))$

BCI-57.  $p\rightarrow ((p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (s\rightarrow (q\rightarrow t)))\rightarrow (s\rightarrow t)))$

BCI-58.  $p\rightarrow ((q\rightarrow r)\rightarrow ((r\rightarrow ((s\rightarrow s)\rightarrow (p\rightarrow t))) \rightarrow (q\rightarrow t)))$

BCI-59.  $((((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow r)\rightarrow s)\rightarrow ((t\rightarrow q)\rightarrow (t\rightarrow s))$

BCI-60.  $(((p\rightarrow (q\rightarrow r))\rightarrow r)\rightarrow s)\rightarrow (((t\rightarrow t)\rightarrow p)\rightarrow (q\rightarrow s))$

BCI-61.  $((p\rightarrow p)\rightarrow q)\rightarrow ((((q\rightarrow (r\rightarrow s))\rightarrow s)\rightarrow t)\rightarrow (r\rightarrow t))$

BCI-62.  $(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow ((s\rightarrow ((t\rightarrow t)\rightarrow p))\rightarrow (s\rightarrow r)))$

BCI-63.  $((p\rightarrow p)\rightarrow (q\rightarrow (r\rightarrow s)))\rightarrow (t\rightarrow ((t\rightarrow r)\rightarrow (q\rightarrow s)))$

BCI-64.  $((p\rightarrow p)\rightarrow (((q\rightarrow r)\rightarrow ((s\rightarrow q)\rightarrow r))\rightarrow t))\rightarrow (s\rightarrow t)$

BCI-65.  $(p\rightarrow q)\rightarrow ((((q\rightarrow r)\rightarrow r)\rightarrow ((s\rightarrow s)\rightarrow t))\rightarrow (p\rightarrow t))$

BCI-66.  $(p\rightarrow q)\rightarrow ((((r\rightarrow p)\rightarrow q)\rightarrow ((s\rightarrow s)\rightarrow t))\rightarrow (r\rightarrow t))$

BCI-67.  $p\rightarrow (((q\rightarrow q)\rightarrow (r\rightarrow (p\rightarrow s)))\rightarrow ((s\rightarrow t)\rightarrow (r\rightarrow t)))$

BCI-68.  $p\rightarrow (((q\rightarrow q)\rightarrow (r\rightarrow (s\rightarrow t)))\rightarrow ((p\rightarrow s)\rightarrow (r\rightarrow t)))$

BCI-69.  $p\rightarrow ((q\rightarrow ((r\rightarrow r)\rightarrow (s\rightarrow t)))\rightarrow ((p\rightarrow s)\rightarrow (q\rightarrow t)))$

BCI-70.  $p\rightarrow ((q\rightarrow (p\rightarrow r))\rightarrow ((s\rightarrow ((t\rightarrow t)\rightarrow q))\rightarrow (s\rightarrow r)))$

BCI-71.  $p\rightarrow ((q\rightarrow r)\rightarrow ((s\rightarrow ((t\rightarrow t)\rightarrow (p\rightarrow q))) \rightarrow (s\rightarrow r)))$

BCI-72.  $p\rightarrow ((p\rightarrow q)\rightarrow ((r\rightarrow ((s\rightarrow s)\rightarrow (q\rightarrow t))) \rightarrow (r\rightarrow t)))$

BCI-73.  $((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow ((t\rightarrow (s\rightarrow q)) \rightarrow (t\rightarrow r)))$

BCI-74.  $(p\rightarrow q)\rightarrow (((((r\rightarrow r)\rightarrow (q\rightarrow s))\rightarrow s)\rightarrow t)\rightarrow (p\rightarrow t))$

BCI-75.  $(p\rightarrow q)\rightarrow ((((r\rightarrow s)\rightarrow s)\rightarrow ((t\rightarrow t)\rightarrow p))\rightarrow (r\rightarrow q))$

BCI-76.  $(((p\rightarrow q)\rightarrow ((r\rightarrow p)\rightarrow q))\rightarrow ((s\rightarrow s)\rightarrow t))\rightarrow (r\rightarrow t)$

BCI-77.  $((((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow ((s\rightarrow q)\rightarrow r))\rightarrow t)\rightarrow (s\rightarrow t)$

BCI-78.  $p\rightarrow ((q\rightarrow r)\rightarrow (((s\rightarrow s)\rightarrow (t\rightarrow (p\rightarrow q))) \rightarrow (t\rightarrow r)))$

BCI-79.  $((((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow s)\rightarrow t)\rightarrow ((r\rightarrow s)\rightarrow (q\rightarrow t))$

BCI-80.  $(p\rightarrow q)\rightarrow (((((r\rightarrow r)\rightarrow (s\rightarrow p))\rightarrow q)\rightarrow t)\rightarrow (s\rightarrow t))$

Working from a list of $\mathbf {BCI}$ candidates circulated by the author starting in 2007, John Halleck and Larry Wos found the first proof for BCI-29. Halleck also provided the first proofs for BCI-73 and BCI-74, Wos gave proofs for BCI-75, BCI-76, and BCI-77, and Mark Stickel discovered proofs for BCI-78 through BCI-80.

It is well known that every theorem of any substitution-detachment system is a substitution instance of at least one formula derivable from the axioms by condensed detachment. Axiom sets from which every theorem can be derived by that method are said to be $\text {D}$-complete. None of the bases for $\mathbf {BCI}$ shown above is $\text {D}$-complete. Each of them has Belnap’s two-property (Belnap 1976), that is, each axiom appearing in any of them contains each sentence letter occurring in it exactly twice, and Hindley (1993) shows that, consequently, each theorem derivable from any such set of axioms by condensed detachment alone will have the two-property as well. So, for example, though $p\rightarrow p$ is obtainable in all of the systems above when condensed detachment is used, instances of it such as $(p\rightarrow p)\rightarrow (p\rightarrow p)$ that lack the two-property cannot be so derived.

An example of a $\text {D}$-complete axiom set for $\mathbf {BCI}$—in fact, a single axiom—is given in Ulrich (2005a): $((((((p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow s)\rightarrow (t\rightarrow q))\rightarrow (t\rightarrow (p\rightarrow r))))\rightarrow s)\rightarrow s)\rightarrow s)\rightarrow s)$.

There are fifteen length-19 theorems of $\mathbf {BCI}$ whose status remains an open question, having been neither ruled out nor confirmed as being single axioms:

BCI-Q1.  $(p\rightarrow ((q\rightarrow q)\rightarrow r))\rightarrow ((((s\rightarrow t)\rightarrow t)\rightarrow p)\rightarrow (s\rightarrow r))$

BCI-Q2.  $(((p\rightarrow q)\rightarrow q)\rightarrow ((r\rightarrow r)\rightarrow s))\rightarrow ((s\rightarrow t)\rightarrow (p\rightarrow t))$

BCI-Q3.  $(((p\rightarrow q)\rightarrow q)\rightarrow ((r\rightarrow r)\rightarrow s))\rightarrow ((t\rightarrow p)\rightarrow (t\rightarrow s))$

BCI-Q4.  $(((p\rightarrow q)\rightarrow r)\rightarrow ((s\rightarrow s)\rightarrow t))\rightarrow ((q\rightarrow r)\rightarrow (p\rightarrow t))$

BCI-Q5.  $(((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow ((s\rightarrow s)\rightarrow t))\rightarrow (p\rightarrow t))$

BCI-Q6.  $(((p\rightarrow q)\rightarrow q))\rightarrow r)\rightarrow ((r\rightarrow ((s\rightarrow s)\rightarrow s))\rightarrow (p\rightarrow s)$

BCI-Q7.  $(p\rightarrow ((q\rightarrow q)\rightarrow (q\rightarrow r)))\rightarrow ((s\rightarrow p)\rightarrow (q\rightarrow (s\rightarrow r)))$

BCI-Q9.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow s)\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow (p\rightarrow s)))$

BCI-Q10.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow s)\rightarrow (s\rightarrow p))\rightarrow (q\rightarrow (s\rightarrow r)))$

BCI-Q11.  $(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow (((s\rightarrow s)\rightarrow (r\rightarrow s)) \rightarrow (p\rightarrow s)))$

BCI-Q13.  $(p\rightarrow q)\rightarrow ((((r\rightarrow p)\rightarrow q)\rightarrow ((s\rightarrow s)\rightarrow s))\rightarrow (r\rightarrow s))$

BCI-Q16.  $p\rightarrow (((q\rightarrow q)\rightarrow (q\rightarrow r))\rightarrow ((r\rightarrow (p\rightarrow s)) \rightarrow (q\rightarrow s)))$

BCI-Q17.  $p\rightarrow (((q\rightarrow q)\rightarrow (r\rightarrow q))\rightarrow ((s\rightarrow (p\rightarrow r)) \rightarrow (s\rightarrow q)))$

BCI-Q18.  $p\rightarrow ((q\rightarrow ((p\rightarrow p)\rightarrow (p\rightarrow r)))\rightarrow ((s\rightarrow q) \rightarrow (s\rightarrow r)))$

BCI-Q20.  $p\rightarrow ((q\rightarrow r)\rightarrow ((r\rightarrow ((p\rightarrow p)\rightarrow (p\rightarrow s))) \rightarrow (q\rightarrow s)))$

The formula which appeared as BCI-Q14 when the author originally sent out the list was ruled out by John Halleck. Those formerly appearing as BCI-Q8, BCI-Q12, BCI-Q15, and BCI-Q19 were ruled out by Petr Pudlak.

A.3  Some relatives of BCI

Restricted versions of $\mathbf {C}$ can be gotten by replacing one or more of its variables with distinct elementary implications.

$\mathbf {C}^{\mathbf {000}}.{\,\,}(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow (p\rightarrow r))$

$\mathbf {C}^{\mathbf {100}}.{\,\,}((p\rightarrow s)\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow ((p\rightarrow s)\rightarrow r))$

$\mathbf {C}^{\mathbf {010}}.{\,\,}(p\rightarrow ((q\rightarrow t)\rightarrow r))\rightarrow ((q\rightarrow t)\rightarrow (p\rightarrow r))$

$\mathbf {C}^{\mathbf {001}}.{\,\,}(p\rightarrow (q\rightarrow (r\rightarrow u)))\rightarrow (q\rightarrow (p\rightarrow (r\rightarrow u)))$

$\mathbf {C}^{\mathbf {110}}.{\,\,}((p\rightarrow s)\rightarrow ((q\rightarrow t)\rightarrow r))\rightarrow ((q\rightarrow t)\rightarrow ((p\rightarrow s)\rightarrow r))$

$\mathbf {C}^{\mathbf {101}}.{\,\,}((p\rightarrow s)\rightarrow (q\rightarrow (r\rightarrow u)))\rightarrow (q\rightarrow ((p\rightarrow s)\rightarrow (r\rightarrow u)))$

$\mathbf {C}^{\mathbf {011}}.{\,\,}(p\rightarrow ((q\rightarrow t)\rightarrow (r\rightarrow u)))\rightarrow ((q\rightarrow t)\rightarrow (p\rightarrow (r\rightarrow u)))$

$\mathbf {C}^{\mathbf {111}}.{\,\,}((p\rightarrow s)\rightarrow ((q\rightarrow t)\rightarrow (r\rightarrow u)))\,{\rightarrow }\, ((q\rightarrow t)\rightarrow ((p\rightarrow s)\rightarrow (r\rightarrow u)))$

Kashima and Kamide (1999), using Gentzen-type sequent calculi, initiated investigation of the variants of $\mathbf {BCI}$ that can be obtained by adding to $\mathbf {B}$ and $\mathbf {I}$ varying combinations of those eight formulas. Exactly five nonequivalent logics result: $\mathbf {BC}^{\mathbf {011}}\mathbf {I}$, it’s two proper extensions, $\mathbf {BC}^{\mathbf {010}}\mathbf {I}$ and $\mathbf {BC}^{\mathbf {001}} \mathbf {I}$, their common proper extension $\mathbf {BC}^{\mathbf {010}}\mathbf {C} ^{\mathbf {001}}\mathbf {I}$, and its proper extension $\mathbf {BC}^{\mathbf {000}}\mathbf {I}$, which is of course $\mathbf {BCI}$ itself. These four proper subsystems of $\mathbf {BCI}$ can be axiomatized with single axioms as well.

BC $^{\mathbf {011}}{} \mathbf I$.

Three-base:  $\mathbf {B},{\,\,}\mathbf {C}^{\mathbf {011}}=(p\rightarrow ((q\rightarrow t)\rightarrow (r\rightarrow u)))\rightarrow ((q\rightarrow t)\rightarrow (p\rightarrow (r\rightarrow u))),{\,\,}\mathbf {I}$   [Kashima and Kamide (1999)]

Two-base:  $\mathbf {B},{\,\,}((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow r)$

One-base:  $(p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (q\rightarrow s))\rightarrow (p\rightarrow s))$   [Ulrich (2006)]

This axiom, which results from the insertion of a copy of $\mathbf {I}$ into $\mathbf {B}^{_{\textstyle \texttt {'}}}\!$ at a critical point, is the shortest possible, and no others of its length will suffice [(Ulrich 2011).]

$\mathbf {BC^{\mathbf {010}}}$ I.

Three-base:  $\mathbf {B},{\,\,}\mathbf {C}^{\mathbf {010}}=(p\rightarrow ((q\rightarrow t)\rightarrow r))\rightarrow ((q\rightarrow t)\rightarrow (p\rightarrow r)),{\,\,}\mathbf {I}{\,\,}$ [Kashima and Kamide (1999)]

Two-base:  $\mathbf {B},{\,\,}\mathbf {Specialized\ Assertion}=((p\rightarrow p)\rightarrow q)\rightarrow q,{\,\,}\mathbf {I}$   [Meredith]

One-bases:  $(p\rightarrow q)\rightarrow (((((r\rightarrow r)\rightarrow s)\rightarrow s)\rightarrow (q\rightarrow t))\rightarrow (p\rightarrow t))$    [Meredith]

$((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow ((r\rightarrow s)\rightarrow (((q\rightarrow s)\rightarrow t)\rightarrow t))$

$(((p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (q\rightarrow s))\rightarrow (p\rightarrow s)))\rightarrow t)\rightarrow t$

$(p\rightarrow q)\rightarrow (((r\rightarrow r)\rightarrow (q\rightarrow s))\rightarrow (((p\rightarrow s)\rightarrow t)\rightarrow t))$

$(p\rightarrow q)\rightarrow (((((r\rightarrow r)\rightarrow (q\rightarrow s))\rightarrow (p\rightarrow s))\rightarrow t)\rightarrow t)$

Anderson and Belnap (1975) report that the first of these single axioms, which results from the insertion of a copy of $\mathbf {Specialized\ Assertion}$ into $\mathbf {B} ^{_{\textstyle \texttt {'}}}$, was given by Meredith as a single axiom uniting the two. The others are in Ulrich (2011); the list is exhaustive, and these one-bases are shortest possible.

$\mathbf {BC^{\mathbf {001}}}$ I.

Three-base:  $\mathbf {B},{\,\,}\mathbf {C}^{\mathbf {001}}=(p\rightarrow (q\rightarrow (r\rightarrow u)))\rightarrow (q\rightarrow (p\rightarrow (r\rightarrow u))),{\,\,}\mathbf {I}{\,\,}$ [Kashima and Kamide (1999)]

Two-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}},{\,\,}p\rightarrow ((q\rightarrow r)\rightarrow ((p\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t)))$

One-bases:  $p\rightarrow ((q\rightarrow r)\rightarrow ((p \rightarrow ((s\rightarrow s)\rightarrow (r\rightarrow t)))\rightarrow (q\rightarrow t)))$

$p\rightarrow ((p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow s)\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t)))$

$((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow ((s\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t)))$

Ulrich (2011); no shorter theorems of $\mathbf {BC}^{\mathbf {001}}\mathbf {I}$ are single axioms for it, nor are any others of equal length.

$\mathbf {BC^{\mathbf {010}}C^{\mathbf {001}}}$ I.

Four-base:  $\mathbf {B},{\,\,}\mathbf {C}^{\mathbf {010}}=(p\rightarrow ((q\rightarrow t)\rightarrow r))\rightarrow ((q\rightarrow t)\rightarrow (p\rightarrow r)),{\,\,}\mathbf {C}^{\mathbf {001}}=(p\,{\rightarrow }\,(q\,{\rightarrow }\,(r\,{\rightarrow }\, u)))\rightarrow (q\rightarrow (p\rightarrow (r\rightarrow u))), {\,\,}\mathbf {I}$   [Kashima and Kamide (1999)]

Two-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}p\rightarrow ((p\rightarrow ((q\rightarrow q)\rightarrow r))\rightarrow r)$

One-bases:  $(((p\rightarrow q)\rightarrow ((r\rightarrow (q\rightarrow s))\rightarrow (p\rightarrow s)))\rightarrow ((t\rightarrow t)\rightarrow u))\rightarrow (r\rightarrow u)$

$((p\rightarrow ((p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow r)))\rightarrow ((t\rightarrow t)\rightarrow u)))\rightarrow ((s\rightarrow q)\rightarrow u)$

$(((p\rightarrow (q\rightarrow r))\rightarrow ((s\rightarrow q)\rightarrow (s\rightarrow r)))\rightarrow ((t\rightarrow t)\rightarrow u))\rightarrow (p \rightarrow u)$

$(((p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow r))\rightarrow ((t\rightarrow t)\rightarrow u))\rightarrow ((s\rightarrow q)\rightarrow (p \rightarrow u))$

$((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow ((((s\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t))\rightarrow u)\rightarrow u))$

$(p\rightarrow q)\rightarrow ((((r\rightarrow (q\rightarrow s))\rightarrow (p\rightarrow s))\rightarrow ((t\rightarrow t)\rightarrow u))\rightarrow (r\rightarrow u))$

$p\rightarrow ((((p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow r))\rightarrow ((t\rightarrow t)\rightarrow u))\rightarrow ((s\rightarrow q)\rightarrow u))$   

Ulrich (2011); no shorter single axioms for $\mathbf {BC}^{\mathbf {001}} \mathbf {C}^{\mathbf {010}}\mathbf {I}$ can be found, but the author assumes that there exist additional hitherto undiscovered single axioms of this same length.

$\mathbf {BCI}^{_{\textstyle \texttt {'}}}\!$.

Three-base:  $\mathbf {B},{\,\,}\mathbf {C},{\,\,}\mathbf {I}^{_{\textstyle \texttt {'}}}=(p\rightarrow q)\rightarrow (p\rightarrow q)$

Two-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}},{\,\,}\mathbf {Pon}=p\rightarrow ((p\rightarrow q)\rightarrow q)$

One-base:  $(p\rightarrow q)\rightarrow (((r\rightarrow ((r\rightarrow s)\rightarrow s)\rightarrow (q\rightarrow t))\rightarrow (p\rightarrow t))$    [Ulrich (2005b)]

The author has been unable to locate references to this system in the literature.

$\mathbf {BCI}^{{\textstyle \mathbf {*}\!}}\!/\mathbf {Monothetic\ BCI}$.

Three-base:  $\mathbf {B},{\,\,}\mathbf {C},{\,\,}\mathbf {I}^{{\textstyle \mathbf {*}}}=(p\rightarrow p)\rightarrow (q\rightarrow q)$   [Bunder (1983)]

Two-bases:  $\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-1 $=(((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow s)\rightarrow (p\rightarrow s)),{\,\,}\mathbf {I}^{_{\textstyle \mathbf {*}}}=(p\rightarrow p)\rightarrow (q\rightarrow q)$

$\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-2 $= (p\rightarrow q)\rightarrow ((((r\rightarrow s)\rightarrow s)\rightarrow p)\rightarrow (r\rightarrow q)),{\,\,}\mathbf {I}^{_{\textstyle \mathbf {*}}}$

One-bases:  $(((p\rightarrow p)\rightarrow q)\rightarrow r)\rightarrow ((s\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow (s\rightarrow t)))$    [Ulrich (2007)]

$(p\rightarrow (q\rightarrow r))\rightarrow ((((s\rightarrow s)\rightarrow t)\rightarrow q)\rightarrow (t\rightarrow (p\rightarrow r)))$   [ibid.]

$(p\rightarrow q)\rightarrow ((((r\rightarrow r)\rightarrow (s\rightarrow s))\rightarrow (q\rightarrow t))\rightarrow (p\rightarrow t))$ is a single axiom for $\mathbf {BC}^{\mathbf {011}}\mathbf {I}^{_{\textstyle \mathbf {*}}}\!$, where, as above, $\mathbf {C}^{\mathbf {011}}=(p\rightarrow ((q\rightarrow t)\rightarrow (r\rightarrow u)))\rightarrow ((q\rightarrow t)\rightarrow (p\rightarrow (r\rightarrow u)))$.

A.4  Entailment: $\mathbf {E}_\rightarrow ,$ the implicational fragment of E

Three-base:  $\mathbf {B},{\,\,}\mathbf {Specialized\ Assertion}=((p\rightarrow p)\rightarrow q)\rightarrow q,{\,\,}\mathbf {W}$    [Anderson et al. (1960)]

Two-base:  $\mathbf {BC}^{\mathbf {010}}$ I-1,  $\mathbf {W}= (p\rightarrow (p\rightarrow q))\rightarrow (p\rightarrow q)\quad$ [Meredith; cf. Anderson and Belnap (1975). Of course, adding $\mathbf {W}$ to any of the other single axioms for $\mathbf {BC} ^{\mathbf {010}}\mathbf {I}$ would do as well.]

One-base:  Rezus (1982) gives instructions for constructing one, but it would be quite long. Perhaps the most outstanding current open problem involving constructing single axioms for implicational logics is that of finding one of reasonable length for $\mathbf {E}_\rightarrow$.

A.5  Relevant implication: $\mathbf {R}_\rightarrow ,$ the implicational fragment of R

Four-bases:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {Pon},{\,\,}\mathbf {I}, {\,\,}\mathbf {W}=(p\rightarrow (p\rightarrow q))\rightarrow (p\rightarrow q)$   [Moh (1950); called $\mathbf {R}_{\rightarrow 2}$ in Anderson and Belnap (1975).]

$\mathbf {B},{\,\,}\mathbf {C},{\,\,}\mathbf {I},{\,\,}\mathbf {W}$   [Church (1951); axiom set $\mathbf {R}_{\rightarrow 1}$ in Anderson and Belnap (1975, p. 88).]

$\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {C},{\,\,}\mathbf {I},{\,\,}\mathbf {S}/ \mathbf {Frege}=(p\rightarrow (q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow (p\rightarrow r))$   [Anderson and Belnap (1975, p. 20)]

$\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {C},{\,\,}\mathbf {I},{\,\,}\mathbf {W}$   [Anderson and Belnap’s set $\mathbf {R}_{\rightarrow 3}$.]

$\mathbf {B},{\,\,}\mathbf {Pon},{\,\,}\mathbf {I},{\,\,}\mathbf {W}$   [Anderson and Belnap’s set $\mathbf {R}_{\rightarrow 4}$.]

$\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {C},{\,\,}\mathbf {I}, ((p\rightarrow q)\rightarrow (r\rightarrow p)) \rightarrow ((p\rightarrow q)\rightarrow (r\rightarrow q))$

Three-bases:  $(p\rightarrow (q\rightarrow r))\rightarrow ((s\rightarrow p)\rightarrow (q\rightarrow (s\rightarrow r))), \ \mathbf {I},\ \mathbf {W}{\,\,}$ [Rezus (1982)]

$\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-1 $=(((p\rightarrow q)\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow s)\rightarrow (p\rightarrow s)),{\,\,}\mathbf {I},{\,\,}\mathbf {W}$

$\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-2 $=(p\rightarrow q)\rightarrow ((((r\rightarrow s)\rightarrow s)\rightarrow p)\rightarrow (r\rightarrow q)),{\,\,}\mathbf {I},{\,\,}\mathbf {W}$

These are the shortest bases for $\mathbf {R}_\rightarrow$ of any kind that are known to the author.

Two-bases:  $\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-1,  $(p\rightarrow (p\rightarrow q))\rightarrow (((r\rightarrow r)\rightarrow p)\rightarrow q)$

$\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-2,  $(p\rightarrow (p\rightarrow q))\rightarrow (((r\rightarrow r)\rightarrow p)\rightarrow q$

The commuted version of the shorter axiom, $((r\rightarrow r)\rightarrow p)\rightarrow ((p\rightarrow (p\rightarrow q))\rightarrow q)$, can be used instead. And of course pairing $\mathbf {W}$ with any of the single axioms above for $\mathbf {BCI}$ will also provide a length-28 two-base.

One-bases:  $((p\rightarrow (((q\rightarrow q)\rightarrow (p\rightarrow r))\rightarrow r))\rightarrow (((((s\rightarrow t)\rightarrow ((t\rightarrow u)\rightarrow (s\rightarrow u)))\rightarrow (((((v\rightarrow (v\rightarrow u))\rightarrow (v\rightarrow u))\rightarrow ((y\rightarrow z)\rightarrow (x\rightarrow z)))\rightarrow a))\rightarrow a)\rightarrow b))\rightarrow b)\rightarrow ((z\rightarrow (((c\rightarrow c)\rightarrow (z\rightarrow d))\rightarrow d))\rightarrow e)))\rightarrow e$    [Rezus (1982)]

$((((p\rightarrow q)\rightarrow (r\rightarrow p))\rightarrow ((p\rightarrow q)\rightarrow (r\rightarrow q)))\rightarrow ((s\rightarrow s)\rightarrow (t \rightarrow (u\rightarrow v))))\rightarrow ((w\rightarrow t)\rightarrow (u\rightarrow (w\rightarrow v)))$   [Ulrich (2012)]

$(((p\rightarrow q)\rightarrow (r\rightarrow p))\rightarrow ((p\rightarrow q)\rightarrow (r\rightarrow q)))\rightarrow ((s\rightarrow s)\rightarrow (t\rightarrow u)))\rightarrow (t\rightarrow ((v\rightarrow (u\rightarrow w))\rightarrow (v\rightarrow w)))$

The author conjectures that there exists a single axiom of length at most 29.

$\mathbf {A.6{\,\,}RM}_\rightarrow$: The implicational fragment of R-Mingle

Four-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {Pon},{\,\,}\mathbf {W},{\,\,}((((p\rightarrow q)\rightarrow q)\rightarrow p)\rightarrow r)\rightarrow (((((q\rightarrow p)\rightarrow p)\rightarrow q)\rightarrow r)\rightarrow r)$   [Meyer and Parks (1972)]

Three-bases:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!, {\,\,}\mathbf {Pon},{\,\,}\mathbf {RM1}=((p\rightarrow (((q\rightarrow p)\rightarrow r)\rightarrow q))\rightarrow r)\rightarrow r{\,\,}$ [Ernst et al. (2001)]

$\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {Pon},{\,\,}\mathbf {RM2}=((((p\rightarrow q)\rightarrow r) \rightarrow (q\rightarrow p))\rightarrow r)\rightarrow r$   [Ernst et al. (2001)]

$\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {Pon},{\,\,}\mathbf {RM3}=((((p\rightarrow q)\rightarrow r) \rightarrow (q\rightarrow p))\rightarrow (s\rightarrow r))\rightarrow (s\rightarrow r)$

Two-bases:  Either $\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-1 or $\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-2 together with one of $\mathbf {RM1}$, $\mathbf {RM2}$, or $\mathbf {RM3}$.

Either $\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-1 or $\mathbf {BB}^{_{\textstyle \texttt {'}}}$ C-2 with $(p\rightarrow (p\rightarrow q))\rightarrow (((r\rightarrow r)\rightarrow p)\rightarrow q)$.

One-bases:  $((((((p\rightarrow q)\rightarrow r)\rightarrow (q\rightarrow p))\rightarrow (s\rightarrow r))\rightarrow (s{\rightarrow } r))\rightarrow ((t{\rightarrow } t)\rightarrow (u\rightarrow (v\rightarrow w))))\rightarrow ((x\rightarrow u)\rightarrow (v\rightarrow (x\rightarrow w)))$   [Ulrich (2009)]

$((((((p\rightarrow q)\rightarrow r)\rightarrow (q\rightarrow p))\rightarrow (s\rightarrow r))\rightarrow (s\rightarrow r))\rightarrow ((t\rightarrow t)\rightarrow (u\rightarrow v)))\rightarrow (u\rightarrow ((w\rightarrow (v\rightarrow x))\rightarrow (w\rightarrow x)))$

Again, the author conjectures there exists a single axiom of length at most 29.

The very first base offered in the literature as a set of axioms for a three-valued logic in Sobociński (1952), which much later proved to be (Parks 1972) characteristic for $\mathbf {RM}_\rightarrow$, was that of Rose (1956). Not shown here, it consists of twenty-one axioms, some of them quite long .

$\mathbf {A.7{\,\,}BCK}$

Three-base:  $\mathbf {B},{\,\,}\mathbf {C},{\,\,}\mathbf {K}/\mathbf {Simp}=p\rightarrow (q\rightarrow p)$   [Meredith and Prior (1963)]

Two-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}((p\rightarrow (q\rightarrow p))\rightarrow r)\rightarrow r$

One-bases:  BCK-1.  $((p\rightarrow q)\rightarrow r)\rightarrow ((s\rightarrow (r \rightarrow t))\rightarrow (q\rightarrow (s\rightarrow t)))$

BCK-2.  $(p\rightarrow (q\rightarrow r))\rightarrow (((p\rightarrow t)\rightarrow q)\rightarrow (t\rightarrow (s\rightarrow r)))$

BCK-3.  $p\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (((t\rightarrow p)\rightarrow r)\rightarrow (q\rightarrow s)))$

BCK-4.  $((p\rightarrow q)\rightarrow r)\rightarrow (q\rightarrow ((s\rightarrow (r\rightarrow t))\rightarrow (s\rightarrow t)))$

BCK-5.  $p\rightarrow (((q\rightarrow p)\rightarrow r)\rightarrow ((s\rightarrow (r\rightarrow t))\rightarrow (s\rightarrow t)))$

BCK-6.  $p\rightarrow (((q\rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow (p\rightarrow t))\rightarrow (r\rightarrow t)))$

BCK-7.  $((p\rightarrow q)\rightarrow r)\rightarrow (s\rightarrow ((r\rightarrow (s\rightarrow t))\rightarrow (q\rightarrow t)))$

BCK-8.  $(p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow (((t\rightarrow s)\rightarrow q)\rightarrow (p\rightarrow r)))$

BCK-9.  $(p\rightarrow q)\rightarrow ((q\rightarrow ((r\rightarrow s)\rightarrow t))\rightarrow ((s\rightarrow (p\rightarrow t)))$

BCK-10.  $(p\rightarrow ((q\rightarrow r)\rightarrow s))\rightarrow (r\rightarrow ((t\rightarrow p)\rightarrow (t\rightarrow s)))$

BCK-11.  $p\rightarrow ((q\rightarrow ((r\rightarrow p)\rightarrow s))\rightarrow ((t\rightarrow q)\rightarrow (t\rightarrow s)))$

BCK-12.  $(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow (((s\rightarrow t)\rightarrow p)\rightarrow (t\rightarrow r)))$

BCK-13.  $p\rightarrow ((q\rightarrow (p\rightarrow r))\rightarrow (((s\rightarrow t)\rightarrow q)\rightarrow (t\rightarrow r)))$

BCK-1 is Meredith’s (Meredith and Prior 1963). The others are new. John Halleck provided a proof for BCK-9. Proofs for BCK-10 through BCK-13 were supplied by Mark Stickel.

None of these axiom sets or single axioms for $\mathbf {BCK}$ are $\text {D}$-complete: in none of them is there a letter occurring more than twice, and by a result of Hindley (1993), each theorem derivable in any of them will have this feature as well. A $\text {D}$-complete single axiom for $\mathbf {BCK}$ is $(((((((p\rightarrow q)\rightarrow r)\rightarrow ((s\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow (s\rightarrow t))))\rightarrow s)\rightarrow s)\rightarrow s)\rightarrow s)$ from Ulrich (2005a).

The author has completed a proof that no shorter single axioms for $\mathbf {BCK}$ exist, but there are twenty-seven 17-symbol theorems of $\mathbf {BCK}$ whose status remains unknown. Numbering below is taken from a list of open questions for single $\mathbf {BCK}$ axioms that he has been circulating for several years.

BCK-Q1.  $((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow ((t\rightarrow r)\rightarrow (t\rightarrow (q \rightarrow s)))$

BCK-Q2.  $(p\rightarrow q)\rightarrow r)\rightarrow ((((r\rightarrow s)\rightarrow s)\rightarrow t)\rightarrow (q\rightarrow t))$

BCK-Q4.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow t)\rightarrow p)\rightarrow (q\rightarrow (t \rightarrow r)))$

BCK-Q5.  $(p\rightarrow q)\rightarrow (((r\rightarrow s)\rightarrow (q\rightarrow t))\rightarrow (p\rightarrow (s \rightarrow t)))$

BCK-Q6.  $((((p\rightarrow q)\rightarrow r)\rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow t)\rightarrow (q\rightarrow t))$

BCK-Q9.  $((p\rightarrow q)\rightarrow r)\rightarrow ((((r\rightarrow s)\rightarrow (q\rightarrow s))\rightarrow t)\rightarrow t)$

BCK-Q10.  $((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow (s\rightarrow t))\rightarrow (s\rightarrow (q\rightarrow t)))$

BCK-Q11.  $((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow s)\rightarrow (((q\rightarrow s)\rightarrow t)\rightarrow t))$

BCK-Q14.  $(p\rightarrow q)\rightarrow (p\rightarrow (((r\rightarrow s)\rightarrow (q\rightarrow t))\rightarrow (s\rightarrow t)))$

BCK-Q15.  $((((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow s)\rightarrow (q\rightarrow s))) \rightarrow t)\rightarrow t$

BCK-Q16.  $p\rightarrow ((p\rightarrow q)\rightarrow (((r\rightarrow s)\rightarrow (q\rightarrow t))\rightarrow (s\rightarrow t)))$

BCK-Q17.  $((p\rightarrow q)\rightarrow r)\rightarrow ((p\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow (p\rightarrow s)))$

BCK-Q18.  $((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow (p\rightarrow s))\rightarrow (p\rightarrow (q\rightarrow s)))$

BCK-Q19.  $((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow ((p\rightarrow r)\rightarrow (p\rightarrow (q\rightarrow s)))$

BCK-Q20.  $((p\rightarrow q)\rightarrow r)\rightarrow (p\rightarrow ((r\rightarrow (p\rightarrow s))\rightarrow (q\rightarrow s)))$

BCK-Q21.  $((p\rightarrow q)\rightarrow r)\rightarrow (q\rightarrow ((p\rightarrow (r\rightarrow s))\rightarrow (p\rightarrow s)))$

BCK-Q22.  $(p\rightarrow ((q\rightarrow r)\rightarrow s))\rightarrow (r\rightarrow ((q\rightarrow p)\rightarrow (q\rightarrow s)))$

BCK-Q23.  $(p\rightarrow (q\rightarrow r))\rightarrow (((p\rightarrow s)\rightarrow q)\rightarrow (s\rightarrow (p\rightarrow r)))$

BCK-Q24.  $(p\rightarrow (q\rightarrow r))\rightarrow (q\rightarrow (((q\rightarrow s)\rightarrow p)\rightarrow (s\rightarrow r)))$

BCK-Q25.  $(p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow (((p\rightarrow s)\rightarrow q)\rightarrow (p\rightarrow r)))$

BCK-Q26.  $(p\rightarrow q)\rightarrow (((p\rightarrow r)\rightarrow (q\rightarrow s))\rightarrow (p\rightarrow (r\rightarrow s)))$

BCK-Q27.  $(p\rightarrow q)\rightarrow (((q\rightarrow r)\rightarrow (p\rightarrow s))\rightarrow (p\rightarrow (r\rightarrow s)))$

BCK-Q28.  $(p\rightarrow q)\rightarrow ((q\rightarrow ((p\rightarrow r)\rightarrow s))\rightarrow (r\rightarrow (p\rightarrow s)))$

BCK-Q30.  $(p\rightarrow q)\rightarrow (p\rightarrow (((p\rightarrow r)\rightarrow (q\rightarrow s))\rightarrow (r\rightarrow s)))$

BCK-Q31.  $p\rightarrow (((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow (p\rightarrow s))\rightarrow (q\rightarrow s)))$

BCK-Q32.  $p\rightarrow (((q\rightarrow p)\rightarrow r)\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow s)))$

BCK-Q33.  $p\rightarrow ((p\rightarrow q)\rightarrow (((p\rightarrow r)\rightarrow (q\rightarrow s))\rightarrow (r\rightarrow s)))$

Candidates 3, 7, 8, 12, and 13 formerly on this list were the ones Halleck and Stickel showed to be single axioms. The formula that originally appeared on the list as BCK-Q29 was shown by Halleck not to be a single axiom for $\mathbf {BCK}$.

$\mathbf {A.8{\,\,}H}_\rightarrow$ : The implicational fragment of Heyting’s intuitionistic calculus

Three-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {K},{\,\,}\mathbf {W}$   [Hilbert’s 1930 set, according to Prior (1962, p. 316).]

Two-bases:  $((p\rightarrow q)\rightarrow r)\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow s)),{\,\,}\mathbf {I}$

$(p\rightarrow q)\rightarrow ((q\rightarrow (q\rightarrow r))\rightarrow (p\rightarrow r)),{\,\,}\mathbf {K}$

One-bases:

HI-1.  $((p\rightarrow q)\rightarrow r)\rightarrow (s\rightarrow ((q\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t)))$    [Meredith (1953)]

HI-2.  $p\rightarrow ((q\rightarrow r)\rightarrow (((s\rightarrow q)\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t)))$    [Meredith and Prior (1963)]

HI-3.  $(p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow (((t\rightarrow p)\rightarrow q)\rightarrow (p\rightarrow r)))$

HI-4.  $p\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (((t\rightarrow q)\rightarrow r)\rightarrow (q\rightarrow s)))$

HI-5.  $((p\rightarrow q)\rightarrow r)\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (t\rightarrow (q\rightarrow s)))$

HI-6.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow p)\rightarrow q)\rightarrow (t\rightarrow (p\rightarrow r)))$

HI-7.  $p\rightarrow (((q\rightarrow r)\rightarrow s)\rightarrow ((r\rightarrow (s\rightarrow t))\rightarrow (r\rightarrow t)))$

HI-8.  $(p\rightarrow q)\rightarrow (((r\rightarrow (s\rightarrow p))\rightarrow (q\rightarrow t))\rightarrow (p\rightarrow t))$

HI-9.  $(p\rightarrow q)\rightarrow ((q\rightarrow ((r\rightarrow p)\rightarrow s))\rightarrow (t\rightarrow (p\rightarrow s)))$

HI-10.  $(p\rightarrow q)\rightarrow (r\rightarrow (((s\rightarrow p)\rightarrow (q\rightarrow t))\rightarrow (p\rightarrow t)))$

HI-11.  $p\rightarrow (((q\rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow (s\rightarrow t))\rightarrow (r\rightarrow t)))$

HI-12.  $((p\rightarrow q)\rightarrow r)\rightarrow (s\rightarrow ((r\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t)))$

HI-3 through HI-7 are from Ulrich (1999). As noted there, they come from Meredith’s HI-1 by permuting its first three antecedents, that is, $(p\rightarrow q)\rightarrow r$, s and $q\rightarrow (r\rightarrow t)$, in all possible ways. HI-8 through HI-12 are new.

These are almost certainly shortest possible single axioms for $\mathbf {H}_\rightarrow$, but (cf. Ulrich (2001)) there are four shorter theorems of $\mathbf {H}_\rightarrow$ whose status is unknown, namely, $\mathbf {C1}=((p\rightarrow q)\rightarrow r)\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow s))$, $\mathbf {C2}=((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow s))$, $\mathbf {C3}=(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow p)\rightarrow q)\rightarrow (p\rightarrow r))$, and $\mathbf {C4}=(p\rightarrow q)\rightarrow (((r\rightarrow p)\rightarrow (q \rightarrow s))\rightarrow (p\rightarrow s))$.

Among the 17-symbol theorems of $\mathbf {H}_\rightarrow$, there remain thirty-one whose status is unknown. Notice that only the first nine have (as do all of the single axioms listed above) five distinct sentence letters occurring in them. The rest contain occurrences of just four distinct letters, and the author conjectures that none of them can serve as a single axiom for $\mathbf {H} _\rightarrow$. Once more, the numbers for the remaining candidates are from a list of such circulated by the author.

HI-Q1.  $((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow (((t\rightarrow q)\rightarrow r)\rightarrow (q\rightarrow s))$

HI-Q2.  $((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow ((q\rightarrow r)\rightarrow (t\rightarrow (q\rightarrow s)))$

HI-Q3.  $((p\rightarrow q)\rightarrow r)\rightarrow (((s\rightarrow q)\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t))$

HI-Q4.  $((p\rightarrow q)\rightarrow r)\rightarrow (((s\rightarrow r)\rightarrow (r\rightarrow t))\rightarrow (q\rightarrow t))$

HI-Q5.  $((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow (r\rightarrow s))\rightarrow (t\rightarrow (q\rightarrow s)))$

HI-Q6.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow (t\rightarrow p))\rightarrow q)\rightarrow (p\rightarrow r))$

HI-Q7.  $(((p\rightarrow q)\rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow (s\rightarrow t))\rightarrow (r\rightarrow t))$

HI-Q8.  $((p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow t))\rightarrow ((r\rightarrow s)\rightarrow (r\rightarrow t))$

HI-Q9.  $((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow (t\rightarrow ((q\rightarrow r)\rightarrow (q\rightarrow s)))$

HI-Q10.  $((p\rightarrow q)\rightarrow r)\rightarrow (((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow s))$

HI-Q11.  $((p\rightarrow q)\rightarrow r)\rightarrow (((p\rightarrow r)\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow s))$

HI-Q12.  $((p\rightarrow q)\rightarrow r)\rightarrow ((q\rightarrow (r\rightarrow (r\rightarrow s)))\rightarrow (q\rightarrow s))$

HI-Q15.  $((p\rightarrow q)\rightarrow r)\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (p\rightarrow (q\rightarrow s)))$

HI-Q16.  $((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow (r\rightarrow s))\rightarrow (p\rightarrow (p\rightarrow s)))$

HI-Q17.  $(((p\rightarrow q)\rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow (s\rightarrow p))\rightarrow (r\rightarrow p))$

HI-Q18.  $(((p\rightarrow q)\rightarrow r)\rightarrow s)\rightarrow ((s\rightarrow (s\rightarrow q))\rightarrow (r\rightarrow q))$

HI-Q19.  $((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow ((q\rightarrow r)\rightarrow (p\rightarrow (q \rightarrow s)))$

HI-Q20.  $((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow (p\rightarrow ((q\rightarrow r)\rightarrow (p \rightarrow s)))$

HI-Q21.  $((p\rightarrow q)\rightarrow (r\rightarrow s))\rightarrow (((p\rightarrow q)\rightarrow r)\rightarrow (q\rightarrow s))$

HI-Q22.  $((p\rightarrow q)\rightarrow r)\rightarrow (p\rightarrow ((q\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow s)))$

HI-Q23.  $((p\rightarrow q)\rightarrow r)\rightarrow (p\rightarrow ((r\rightarrow (r\rightarrow s))\rightarrow (q\rightarrow s)))$

HI-Q24.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow (s\rightarrow p))\rightarrow q)\rightarrow (p \rightarrow r))$

HI-Q25.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow p)\rightarrow (p\rightarrow q))\rightarrow (p \rightarrow r))$

HI-Q26.  $(p\rightarrow (q\rightarrow r))\rightarrow (((s\rightarrow p)\rightarrow q)\rightarrow (s\rightarrow (p \rightarrow r)))$

HI-Q27.  $(p\rightarrow (q\rightarrow r))\rightarrow (s\rightarrow (((s\rightarrow p)\rightarrow q)\rightarrow (p \rightarrow r)))$

HI-Q28.  $(p\rightarrow q)\rightarrow (((r\rightarrow (r\rightarrow p))\rightarrow (q\rightarrow s))\rightarrow (p \rightarrow s))$

HI-Q30.  $(p\rightarrow q)\rightarrow (((r\rightarrow p)\rightarrow (q\rightarrow (p\rightarrow s)))\rightarrow (p \rightarrow s))$

HI-Q31.  $(p\rightarrow q)\rightarrow (((r\rightarrow p)\rightarrow (q\rightarrow (q\rightarrow s)))\rightarrow (p \rightarrow s))$

HI-Q33.  $(p\rightarrow q)\rightarrow ((q\rightarrow ((r\rightarrow p)\rightarrow s))\rightarrow (r\rightarrow (p \rightarrow s)))$

HI-Q34.  $(p\rightarrow q)\rightarrow (r\rightarrow (((r\rightarrow p)\rightarrow (q\rightarrow s))\rightarrow (p \rightarrow s)))$

HI-Q35.  $p\rightarrow (((p\rightarrow q)\rightarrow r)\rightarrow ((r\rightarrow (r\rightarrow s))\rightarrow (q \rightarrow s)))$

Candidates HI-Q13, HI-Q14, HI-Q29, and HI-Q32 from the list as originally circulated were shown by John Halleck to be incapable of being single axioms for $\mathbf {H}_\rightarrow$.

$\mathbf {A.9{\,\,}The\ implicational\ fragment\ of\ Dummett}$’$\mathbf {s\ LC}$

Four-bases:  Add $\mathbf {Dummett} =((p\rightarrow q)\rightarrow r)\rightarrow (((q\rightarrow p)\rightarrow r)\rightarrow r)$ to any three-base for $\mathbf {H}_\rightarrow$ [(Bull 1962)].

Of course three- and two-bases result if $\mathbf {Dummett}$ is added to a smaller base for $\mathbf {H}_\rightarrow$.

One-base:  $(((p\rightarrow (q\rightarrow p))\rightarrow ((((((r\rightarrow s)\rightarrow t)\rightarrow (((s\rightarrow r)\rightarrow t)\rightarrow r))\rightarrow (u\rightarrow (u\rightarrow v)))\rightarrow (w\rightarrow v))\rightarrow x))\rightarrow ((w\rightarrow u)\rightarrow x))$

Shorter single axioms no doubt exist. The author has not, for example, experimented with inserting $\mathbf {Dummett}$ into various spots in any of the single axioms for $\mathbf {H}_\rightarrow$.

$\mathbf {A.10{\,\,}The\ implicational\ fragment\ of\ {\L }ukasiewicz}$’$\mathbf {s\ infinite}$-$\mathbf {valued\, sentential}$ $\mathbf {calculus\ L}_{\aleph _0}, \mathbf {et\ relata}$

Implicational $\mathbf {L}_{\aleph _0}$.

Four-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!,{\,\,}\mathbf {K},{\,\,}\mathbf {Inversion}=((p\rightarrow q)\rightarrow q)\rightarrow ((q\rightarrow p)\rightarrow p),{\,\,}\mathbf {Linearity} =((p\rightarrow q)\rightarrow (q\rightarrow p))\rightarrow (q \rightarrow p)$   [Meyer (1966)]

One-bases:  The methods of Rezus (1982) ensure the existence of single axioms for all logics whose theorems include the first two of these axioms, albeit typically those methods produce long axioms.

In the presence of $\mathbf {B}$ and $\mathbf {K}$, $\mathbf {Inversion}$ and $\mathbf {Linearity}$ can be replaced with the single formula $((p\rightarrow q)\rightarrow q)\rightarrow (((p\rightarrow q)\rightarrow (q\rightarrow p))\rightarrow p)$. As a result, we have (Ulrich 2008) the following 37-symbol single axiom for $\mathbf {L}_{\aleph _0\rightarrow }$.

$((p\rightarrow (q\rightarrow p))\rightarrow ((((((r\rightarrow s)\rightarrow s)\rightarrow (((r\rightarrow s)\rightarrow (s\rightarrow r))\rightarrow r))\rightarrow (t\rightarrow u)))\rightarrow (v\rightarrow u))\rightarrow w)\rightarrow ((v\rightarrow t)\rightarrow w)$

Again, shorter single axioms surely exist .

$\mathbf {BCK} + \mathbf {Inversion}$.

Four-base:  $\mathbf {B},{\,\,}\mathbf {C},{\,\,}\mathbf {K}/\mathbf {Simp},{\,\,}\mathbf {Inversion}$

One-base:  $((p\rightarrow (q\rightarrow p))\rightarrow ((((r\rightarrow s)\rightarrow s)\rightarrow ((s\rightarrow r)\rightarrow r))\rightarrow (t\rightarrow u))) \rightarrow ((u\rightarrow v)\rightarrow (t\rightarrow v))$   [Of length 29, the author doubts that it is shortest possible.]

$\mathbf {BCK} + \mathbf {Linearity}$.

Four-base:  $\mathbf {B},{\,\,}\mathbf {C},{\,\,}\mathbf {K}/\mathbf {Simp},{\,\,}\mathbf {Linearity}$

One-base:  $((((p\rightarrow (q\rightarrow p))\rightarrow r)\rightarrow r)\rightarrow (((s\rightarrow t)\rightarrow (((u\rightarrow t)\rightarrow (t\rightarrow u)\rightarrow (s\rightarrow u)))\rightarrow v))\rightarrow (w\rightarrow v)$   

37 symbols long, one would think shorter axioms surely exist.

A.11  Some systems of strict implication

$\mathbf {C3,}$ the strict-implicational fragment of $\mathbf {S3.}$

Three-base:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!, {\,\,}\mathbf {W},{\,\,}\mathbf {Weak\ Irrelevance}=(p\rightarrow q)\rightarrow (r\rightarrow r)$ [Anderson and Belnap (1962)]

An equivalent base can be obtained by adding the axiom $\mathbf {I}^{{\textstyle \mathbf {*}}}=(p\rightarrow p)\rightarrow (q\rightarrow q)$, used for Monothetic $\mathbf {BCI}$ above, to any base for $\mathbf {E}_\rightarrow$; $\mathbf {C3}$ is thus “Monothetic $\mathbf {E}_\rightarrow$.”

One-base:  $(((p\rightarrow (p\rightarrow q))\rightarrow ((r\rightarrow s)\rightarrow (p\rightarrow q)))\rightarrow (((t{\rightarrow } u)\rightarrow ((v{\rightarrow } w)\rightarrow (((x\rightarrow x)\rightarrow (w\rightarrow y)))\rightarrow (v\rightarrow y)))\rightarrow z))\rightarrow z$   [Ulrich (2005a), where it is also shown that every finitely axiomatizable extension of $\mathbf {C3}$ can be axiomatized by a single axiom. Shorter axioms no doubt await discovery.]

$\mathbf {C4}$, the strict-implicational fragment of $\mathbf {S4}$.

Three-base:  $\mathbf {Frege},{\,\,}\mathbf {Weak\ Irrelevance} =(p\rightarrow q)\rightarrow (r\rightarrow (p\rightarrow q)), {\,\,}\mathbf {I}$ [Anderson and Belnap (1962)]

The strict-implicational fragments of all extensions of $\mathbf {S4}$ between it and $\mathbf {S4.3}$ are identical (Ulrich 1981).

Two-base:  $(p\rightarrow (q\rightarrow r))\rightarrow ((p\rightarrow q)\rightarrow (s\rightarrow (p\rightarrow r))),{\,\,}\mathbf {Irrelevance}=p\rightarrow (q\rightarrow q)$   [Ernst et al. (2002)]

The authors show that this 20-symbol two-base is a shortest such base for $\mathbf {C4}$; they also found five additional two-bases of that same length, and have shown that no others exist.

One-base:  $(p\rightarrow ((q\rightarrow (r\rightarrow r))\rightarrow (p\rightarrow q))\rightarrow ((s\rightarrow t)\rightarrow (u\rightarrow (p\rightarrow t)))$ [Ernst et al. (2002)]

The authors show that this 21-symbol axiom is not only a shortest possible axiom for $\mathbf {C4}$, but that it is the shortest possible axiom for that system: no shorter formula nor even another of the same length will do. Note that $\mathbf {C4}$ is thus one more example (cf. $\mathbf {BCI}$ etc., above) of a system whose shortest possible two-bases are one symbol shorter than their shortest possible single axioms.

$\mathbf {C5}$, the strict-implicational fragment of $\mathbf {S5}$.

Three-bases:  $\mathbf {B}^{_{\textstyle \texttt {'}}}\!, {\,\,}(((p\rightarrow q)\rightarrow r)\rightarrow (p\rightarrow q))\rightarrow (p\rightarrow q),{\,\,}\mathbf {Irrelevance}=p \rightarrow (q\rightarrow q)$   [Meredith, in Lemmon et al. (1969).]

Two-bases:  $\mathbf {Irrelevance}, {\,\,}\mathbf {M2}=(((p\rightarrow q)\rightarrow r)\rightarrow q)\rightarrow ((q\rightarrow s)\rightarrow (p\rightarrow s))$   [Meredith circa 1956; ibid.]

$\mathbf {Irrelevance},{\,\,}(((p\rightarrow q)\rightarrow r)\rightarrow s)\rightarrow ((q\rightarrow s)\rightarrow (p\rightarrow s))$   [Prior (1961)]

$(p\rightarrow q)\rightarrow (((q\rightarrow r)\rightarrow s)\rightarrow r)\rightarrow (p\rightarrow r),{\,\,}\mathbf {I}$   [Ernst et al. (2002)]

One-bases:  $(((p\rightarrow p)\rightarrow q)\rightarrow r))\rightarrow (s\rightarrow t))\rightarrow ((t\rightarrow q)\rightarrow (u\rightarrow (s\rightarrow q)))$

$(((p\rightarrow q)\rightarrow r)\rightarrow ((s\rightarrow s)\rightarrow q))\rightarrow ((q\rightarrow t)\rightarrow (u\rightarrow (p\rightarrow t)))$

$(((p\rightarrow q)\rightarrow r)\rightarrow ((s\rightarrow s)\rightarrow q))\rightarrow (t\rightarrow ((q\rightarrow u)\rightarrow (p\rightarrow u))$

$(((p\rightarrow q)\rightarrow r)\rightarrow ((s\rightarrow s)\rightarrow t))\rightarrow (u\rightarrow ((q\rightarrow t)\rightarrow (p\rightarrow t)))$

$(((p\rightarrow p)\rightarrow q)\rightarrow r)\rightarrow (s\rightarrow q))\rightarrow ((q\rightarrow t)\rightarrow ((u\rightarrow (s\rightarrow t)))$

$(((p\rightarrow p)\rightarrow q)\rightarrow r)\rightarrow (s\rightarrow q))\rightarrow ((t\rightarrow s)\rightarrow (u\rightarrow (t\rightarrow q)))$

$((((p\rightarrow p)\rightarrow (q\rightarrow r))\rightarrow s)\rightarrow r)\rightarrow ((r\rightarrow t)\rightarrow (u\rightarrow (q\rightarrow t)))$

The first single axiom above is Meredith’s circa 1956 in Lemmon et al. (1969). The others are from Ernst et al. (2002). The authors of the latter show that these 21-symbol single axioms for $\mathbf {C5}$ are shortest possible, and that the list above is exhaustive.

Their two-base, however, is just 18 symbols in length and is the most severe example known to the author of a system being axiomatizable by a two-base shorter than its shortest possible single axioms. They also show it is the shortest possible base for $\mathbf {C5}$: no other base of any kind can match its length.