N-place implicational tautologies

Diving into Mathematical Logic brought me across Peirce’s Law, which uses the logical implication ⇒ operator only and is always True irrespective of what its two inputs (say) P and Q are:

((P ⇒ Q) ⇒ P) ⇒ P

Tower of N-place implicational tautologies

This got me thinking about the possibility of logical formulae that only use the logical implication ⇒ operator and are always True for any number of inputs.

A Hierarchy of Laws

I investigated this with some Python code and it turns out that there is a hierarchy of Laws:

Number of Variables – ArityVariablesNumber of Shortest TautologiesShortest Tautologies
(Unique up to variable renaming)
Comments
01True
1P1P ⇒ P
2P, Q2P ⇒ (Q ⇒ P)
P ⇒ (Q ⇒ Q)
Peirce’s Law is just one of sixteen two-variable tautologies with three ⇒ operators:
P ⇒ ((P ⇒ Q) ⇒ P)
P ⇒ (P ⇒ (Q ⇒ P))
(P ⇒ Q) ⇒ (P ⇒ Q)
P ⇒ (Q ⇒ (P ⇒ Q))
(P ⇒ Q) ⇒ (Q ⇒ Q)
P ⇒ (Q ⇒ (Q ⇒ Q))
((P ⇒ Q) ⇒ P) ⇒ P
P ⇒ ((Q ⇒ P) ⇒ P)
(P ⇒ Q) ⇒ (P ⇒ P)
P ⇒ (Q ⇒ (P ⇒ P))
P ⇒ ((Q ⇒ Q) ⇒ P)
P ⇒ (Q ⇒ (Q ⇒ P))
((P ⇒ P) ⇒ Q) ⇒ Q
P ⇒ ((P ⇒ Q) ⇒ Q)
(P ⇒ P) ⇒ (Q ⇒ Q)
P ⇒ (P ⇒ (Q ⇒ Q))
3P, Q, R5(P ⇒ Q) ⇒ (R ⇒ R)
P ⇒ (Q ⇒ (R ⇒ R))
P ⇒ (Q ⇒ (R ⇒ Q))
P ⇒ ((Q ⇒ R) ⇒ P)
P ⇒ (Q ⇒ (R ⇒ P))
4P, Q, R, S16P ⇒ (((Q ⇒ R) ⇒ S) ⇒ P)
P ⇒ ((Q ⇒ (R ⇒ S)) ⇒ P)
P ⇒ (Q ⇒ ((R ⇒ S) ⇒ P))
P ⇒ ((Q ⇒ R) ⇒ (S ⇒ P))
P ⇒ (Q ⇒ (R ⇒ (S ⇒ P)))
((P ⇒ Q) ⇒ R) ⇒ (S ⇒ S)
(P ⇒ (Q ⇒ R)) ⇒ (S ⇒ S)
P ⇒ ((Q ⇒ R) ⇒ (S ⇒ S))
(P ⇒ Q) ⇒ (R ⇒ (S ⇒ S))
P ⇒ (Q ⇒ (R ⇒ (S ⇒ S)))
(P ⇒ Q) ⇒ (R ⇒ (S ⇒ R))
P ⇒ (Q ⇒ (R ⇒ (S ⇒ R)))
P ⇒ (Q ⇒ ((R ⇒ S) ⇒ Q))
P ⇒ (Q ⇒ (R ⇒ (S ⇒ Q)))
5P, Q, R, S , T42
6P, Q, R, S, T, U132
Table of shortest tautological laws using implication alone, of increasing arity.

Reader’s feedback is welcome!