Como sospechabas, esto se puede demostrar sólo a partir de los tres primeros axiomas. Intenté enumerar por fuerza bruta los teoremas deducibles de los tres axiomas (tomando todos los pares de teoremas ya demostrados y unificando uno con la premisa del otro), pero no encontré tu objetivo en el primer axioma. $80000$ teoremas demostrados.
Entonces encontré algunas orientaciones en el artículo sobre la lógica de la relevancia en el Manual de lógica filosófica . La lógica de la relevancia se centra en el fragmento de la lógica en el que, a grandes rasgos, las premisas son relevantes para las conclusiones. No incluye el axioma $p\to(q\to p)$ que nos permite añadir una premisa irrelevante a un teorema ya demostrado sin esa premisa, y por lo tanto es estrictamente más débil que el sistema que estás utilizando, pero sin embargo podemos hacer uso de los resultados citados en ese artículo.
Primero describiré la estructura de la prueba y cómo la encontré, y luego daré la prueba en detalle. Aquí están los nombres que usaré para los axiomas; la primera columna nombra los axiomas correspondientes de la lógica combinatoria, para comparar con la discusión en los comentarios bajo la pregunta:
$$ \begin{array}{c|l|l} \mathbf I&\text{self-implication}&p\to p\\ \mathbf K&\text{weakening}& p \to (q \to p) \\ \hline \mathbf B&\text{prefixing}& (p \to q) \to ((r \to p) \to (r \to q)) \\ \mathbf A&\text{suffixing}& (p \to q) \to ((q \to r) \to (p \to r)) \\ \hline \mathbf W&\text{contraction}& (p \to (p \to q)) \to (p \to q) \\ \mathbf S&\text{self-distribution}&(p \to (q \to r)) \to ((p \to q) \to (p \to r))\\ \hline \mathbf C&\text{permutation}&(p\to(q\to r))\to(q\to(p\to r))\\ &\text{assertion}&p\to((p\to q)\to q) \end{array} $$
(Los nombres son los utilizados en el artículo, excepto que yo uso "debilitamiento" en lugar de "paradoja positiva", ya que es más corto y tiene más sentido para mí).
Teorema $1$ del artículo afirma que, con modus ponens (e implícitamente la sustitución universal), los conjuntos de axiomas formados por la autoimplicación y uno de los tres pares prefijación/sufijación, contracción/autodistribución y permutación/afirmación conducen a la misma teoría.
Lo que hay es debilitamiento, sufijación y contracción. La autoimplicación puede deducirse del debilitamiento y la contracción en un solo paso (sustituyendo $p$ para $q$ en todas partes). Así, si podemos deducir la aserción en su sistema, el teorema nos dirá que podemos deducir todo lo demás, incluyendo su objetivo, la autodistribución. Encontré una prueba para la aserción mediante la búsqueda por fuerza bruta.
El artículo no da una prueba de su Teorema $1$ y sólo dice que se puede demostrar consultando un libro que no está disponible en Internet y haciendo algunos "chanchullos", por lo que todavía tenemos que mostrar cómo llegar desde la autoimplicación, la sufijación, la contracción y la aserción a la autodistribución.
He encontrado una deducción de la autodistribución en línea que utiliza la prefijación y la permutación. Resulta que la prefijación es deducible en un solo paso a partir de la sufijación y la permutación, por lo que el problema seguía siendo sólo deducir la permutación. Una vez más, encontré una prueba para esto mediante la búsqueda por fuerza bruta.
Así que aquí está toda la prueba reunida, empezando por tus tres axiomas y terminando con tu objetivo. Primero, una descripción de alto nivel similar a las llamadas reales en mi código Java:
assertion = t (t (weakening,suffixing),contraction);
permutation = t (suffixing,m (assertion,suffixing));
prefixing = m (suffixing,permutation);
target = t (m (prefixing,prefixing),t (permutation,m (contraction,prefixing)));
Cada llamada a m es una aplicación de modus ponens en el que el primer argumento es $A$ el segundo argumento es $A\to B$ y el unificador más general que hace el $A$ s coinciden. Cada llamada a t es una invocación a la transitividad (es decir, la deducción de $A\to C$ de $A\to B$ y $B\to C$ ), que puede implementarse como
t (A->B,B->C) = m (B->C,m (A->B,suffixing))
utilizando el sufijo, o como
t (A->B,B->C) = m (A->B,m (B->C,prefixing))
una vez que la prefijación está disponible.
Esta es la prueba que se explica en $14$ pasos. La primera tabla muestra los teoremas utilizados para generar los antecedentes $A$ y las implicaciones $A\to B$ para modus ponens así como los teoremas resultantes $B$ :
$$ \begin{array}{c|c|c|c|c} &&A&A\to B&B\\\hline \text{(a)}&\text{weakening}&&&p \to (q \to p)\\ \text{(b)}&\text{suffixing}&&&(p \to q) \to ((q \to r) \to (p \to r))\\ \text{(c)}&\text{contraction}&&&(p \to (p \to q)) \to (p \to q)\\ \hline \text{(d)}&\text{*}&\text{(a)}&\text{(b)}&((p \to q) \to r) \to (q \to r)\\ \text{(e)}&&\text{(b)}&\text{(d)}&p \to ((p \to q) \to (r \to q))\\ \text{(f)}&\text{*}&\text{(e)}&\text{(b)}&(((p \to q) \to (r \to q)) \to s) \to (p \to s)\\ \text{(g)}&\text{assertion}&\text{(c)}&\text{(f)}&p \to ((p \to q) \to q)\\ \text{(h)}&&\text{(g)}&\text{(b)}&(((p \to q) \to q) \to r) \to (p \to r)\\ \text{(i)}&\text{*}&\text{(b)}&\text{(b)}&(((p \to q) \to (r \to q)) \to s) \to ((r \to p) \to s)\\ \text{(j)}&\text{permutation}&\text{(h)}&\text{(i)}&(p \to (q \to r)) \to (q \to (p \to r))\\ \text{(k)}&\text{prefixing}&\text{(b)}&\text{(j)}&(p \to q) \to ((r \to p) \to (r \to q))\\ \text{(l)}&&\text{(k)}&\text{(k)}&(p \to (q \to r)) \to (p \to ((s \to q) \to (s \to r)))\\ \text{(m)}&&\text{(c)}&\text{(k)}&(p \to (q \to (q \to r))) \to (p \to (q \to r))\\ \text{(n)}&\text{*}&\text{(j)}&\text{(b)}&((p \to (q \to r)) \to s) \to ((q \to (p \to r)) \to s)\\ \text{(o)}&&\text{(m)}&\text{(n)}&(p \to (q \to (p \to r))) \to (q \to (p \to r))\\ \text{(p)}&\text{*}&\text{(l)}&\text{(b)}&((p \to ((q \to r) \to (q \to s))) \to t) \to ((p \to (r \to s)) \to t)\\ \text{(q)}&\text{self-distribution}&\text{(o)}&\text{(p)}&(p \to (q \to r)) \to ((p \to q) \to (p \to r))\\ \end{array} $$
Los asteriscos marcan los pasos intermedios en las invocaciones de transitividad. Obsérvese que la mayoría de los teoremas con más de tres variables sólo aparecen en esos pasos intermedios. Las sustituciones se realizan lo más tarde posible; si se realizaran lo antes posible, la demostración podría escribirse utilizando sólo teoremas con un máximo de tres variables.
La segunda tabla muestra las sustituciones utilizadas; también puede encontrarlas automáticamente mediante unificación . Las variables se nombran de forma que aparezcan en orden alfabético en los teoremas resultantes.
$$ \begin{array}{c|l|l} &A&A\to B\\\hline \text{(d)}& p\mapsto q,q\mapsto p& p\mapsto q,q\mapsto (p \to q),r\mapsto r\\ \text{(e)}& p\mapsto r,q\mapsto p,r\mapsto q& p\mapsto r,q\mapsto p,r\mapsto ((p \to q) \to (r \to q))\\ \text{(f)}& p\mapsto p,q\mapsto q,r\mapsto r& p\mapsto p,q\mapsto ((p \to q) \to (r \to q)),r\mapsto s\\ \text{(g)}& p\mapsto (p \to q),q\mapsto q& p\mapsto p,q\mapsto q,r\mapsto (p \to q),s\mapsto ((p \to q) \to q)\\ \text{(h)}& p\mapsto p,q\mapsto q& p\mapsto p,q\mapsto ((p \to q) \to q),r\mapsto r\\ \text{(i)}& p\mapsto r,q\mapsto p,r\mapsto q& p\mapsto (r \to p),q\mapsto ((p \to q) \to (r \to q)),r\mapsto s\\ \text{(j)}& p\mapsto q,q\mapsto r,r\mapsto (p \to r)& p\mapsto (q \to r),q\mapsto r,r\mapsto p,s\mapsto (q \to (p \to r))\\ \text{(k)}& p\mapsto r,q\mapsto p,r\mapsto q& p\mapsto (r \to p),q\mapsto (p \to q),r\mapsto (r \to q)\\ \text{(l)}& p\mapsto q,q\mapsto r,r\mapsto s& p\mapsto (q \to r),q\mapsto ((s \to q) \to (s \to r)),r\mapsto p\\ \text{(m)}& p\mapsto q,q\mapsto r& p\mapsto (q \to (q \to r)),q\mapsto (q \to r),r\mapsto p\\ \text{(n)}& p\mapsto q,q\mapsto p,r\mapsto r& p\mapsto (q \to (p \to r)),q\mapsto (p \to (q \to r)),r\mapsto s\\ \text{(o)}& p\mapsto q,q\mapsto p,r\mapsto r& p\mapsto q,q\mapsto p,r\mapsto (p \to r),s\mapsto (q \to (p \to r))\\ \text{(p)}& p\mapsto p,q\mapsto r,r\mapsto s,s\mapsto q& p\mapsto (p \to (r \to s)),q\mapsto (p \to ((q \to r) \to (q \to s))),r\mapsto t\\ \text{(q)}& p\mapsto p,q\mapsto (p \to q),r\mapsto r& p\mapsto p,q\mapsto p,r\mapsto q,s\mapsto r,t\mapsto ((p \to q) \to (p \to r))\\ \end{array} $$
