# How short can the axioms of propositional logic be?

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.

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.)