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.


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


1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.