There are a number of axiom systems for classical propositional calculus. Here, I focus on those which use negation ($\neg$) and implication ($\to$) as the connectives, with Modus Ponens and Substitution serving as the rules of inference.
Roughly speaking, it seems there is a trade-off between the number of axioms in a given system and the corresponding lengths of the axioms. For instace, there is the well-known single axiom of Meredith [1]:
$$ ((((p\to q)\to(\neg r\to\neg s))\to r)\to t)\to((t\to p)\to(s\to p)) $$
which, counting connectives and propositional variables, has a length of 21. On the other hand, the longest axiom can be made shorter by allowing several axioms in the system. Many common systems [2] include the distributive axiom
$$ (p\to(q\to r))\to((p\to q)\to(p\to r)) $$
having length 13, or the syllogistic axiom
$$ (p\to q)\to((q\to r)\to(p\to r)) $$
of length 11, with the remaining axioms being at most as long. Interestingly, Sobociński gave the following system, called $S_2$ in [2]:
(1) $\enspace (p\to q)\to(\neg q\to(p\to r))$
(2) $\enspace p\to(q\to(r\to p))$
(3) $\enspace (\neg p\to q)\to((p\to q)\to q)$
whose longest axioms, (1) and (3), are only of length 10. Otherwise, I haven't been able to find systems with shorter axioms than these. Therefore, my question is:
Question: For classical propositional calculus, do there exist axiom systems whose axioms are all of length strictly less than 10, counting connectives and variables?
I initially tried to find short axioms for the fragment implicational intuitionistic logic, adding small (< 10) axioms covering negation and excluded middle, but I was unsuccessful in this line of attack. Any help is appreciated.
Sources:
[1]: Meredith, C. A., Single axioms for the systems $(C, N), (C, 0)$ and $(A, N)$ of the two-valued propositional calculus, J. comput. Systems 1, 155-164 (1953). ZBL0053.00204.
[2]: Imai, Y.; Iséki, K., On axiom systems of propositional calculi. I, Proc. Japan Acad. 41, 436-439 (1965). ZBL0223.02007.
