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 lengthstrictly lessthan 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.