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.
Best Answer
No. Take the set of truth values to be $\{\top, \bot, P, \neg P, Q, \neg Q\}$, with $\neg$ defined in the obvious way and $\to$ defined by cases: $p \to \top$ and $\bot \to p$ are both $\top$, $\top \to p$ is $p$, $p \to \bot$ is $\neg p$, $\neg p \to p$ is $p$, anything else is $\top$. By brute force all 1056 propositional tautologies of length strictly less than 10 have value $\top$, and modus ponens and substitution are valid (if $p \to q = \top$ and $p = \top$ then $q = \top$), but for example the instance $(P \to Q) \to ((Q \to \neg P) \to (P \to \neg P))$ of the syllogism axiom has value $\neg P \neq \top$.
(The intuition behind trying this particular definition of $\to$ was mostly just that it's a minimal counterexample to "if $p \to q$ and $p \to \neg q$ then $\neg p$", while satisfying $\neg\neg p = p$ and $\neg p \to p = p$. Beyond that I don't really have any idea why it actually works; it would be interesting to see a non-brute-force argument.)
For implicational logic, even axioms of length 10 aren't enough: the model above satisfies all 235 (classical) implicational tautologies of length < 11, so the minimum length is 11, which is the length of Hilbert's first axiom system in the Wikipedia page you linked.