Let $\mathcal{S}$ be a complete set of axioms for classical propositional logic (for example, say the Hilbert axioms), and let $\pi\in\mathcal{S}$ be an axiom in it. Is it decidable (in a Turing machine sense) if $\pi$ is redundant, i.e.:- if $\pi$ can be derived from axioms in $\mathcal{S}\setminus\pi$?
My work
I was working through Hedman's 'A First Course in logic,' where he proves that $\lor$-symm is a redundant rule in his deductive system. Similarly, I've seen two or three other redundancy proofs, including one in a multi-valued propositional logic. However, I found no general 'thread' unifying those proofs since all of them seemed to be based on some very specific properties of $\mathcal{S}, \pi$, which leads me to suspect that this problem may be undecidable after all. Still, I need help to show this.