The independence of theorems in some propositional calculus systems seems well studied. For example, if we just have the rules of detachment, substitution, and replacement, and every theorem of this axiom set {((p->q)->((q->r)->(p->r))), ((~p->p)->p), (p->(~p->q))}=X as our system X', every theorem of X, as I've read, can get proved independent of any other theorem of the set (except itself). But, this "independence" simply has to happen outside of the system, since within the system, all the theorems of X imply each other. This works out this way, since (p->(q->(p->q))) happens in the system and via the rule of substitution (or equivalently (q->(p->q)), we can get every instance of (x->y) as a theorem, where x, y belong to X. In turn, this yields short proofs of every axiom from any other axiom of the axiom set.
1 x since x is a theorem by hypothesis
2 (x->y) which can get formally demonstrated by the above
3 y 1, 2 detachment
So, "independence" of logical axioms simply can't mean that we can't prove a logical axiom from another axiom within a system like this, since all axioms can get derived from each other within X'. What then does "independence" of logical axioms mean precisely?
Edit: So it can get checked that (x->y) holds in the sense above, I've reproduced the necessary parts of Jan Lukasiewicz's Elements of Mathematical Logic to prove the "law of simplification" (q->(p->q)). Symbols of the type Lz refers to a thesis given by Lukasiewicz, while Sz refers to intermediate expressions (which also qualify as theorems of his system) which he indicates as intermediate expressions via his shorthand for proofs. I've included spaces where substitutions have gotten made. A string followed by "L1, p/Cpq" for example means that in thesis L1 all instances of "p" occuring in that thesis have gotten uniformly substituted by "Cpq".
L1 CCpqCCqrCpr axiom
L2 CCNppp axiom
L3 CpCNpq axiom
S1 CC Cpq CCqrCpr CC CCqrCpr s C Cpq s L1, p/Cpq, q/CCqrCpr, r/s
L4 CCCCqrCprsCCpqs L1, S1 detachment
S2 CCCC Cqr Csr C p Csr CCsqCpCsr CC p Cqr CCsqCpCsr L4, q/Cqr, r/Csr, s/CCsqCpCsr
S3 CCCC q r C s r CpCsr CC s q CpCsr L4, p/s, s/CpCsr
L5 CCpCqrCCsqCpCsr S2, S3 detachment
S4 CCCC q r C p r CCCprsCCqrs CC p q CCCprsCCqrs L4, s/CCCprsCCqrs
S5 CC Cqr Cpr CC Cpr s C Cqr s L1, p/Cqr, q/Cpr, r/s
L6 CCpqCCCprsCCqrs S4, S5 detachment
S6 CC Cpq C CCprs CCqrs CC t CCprs C Cpq C t CCqrs L5, p/Cpq, q/CCprs, r/CCqrs, s/t
L7 CCtCCprsCCpqCtCCqrs L6, S6 detachment
S7 CC p CNpq CC CNpq r C p r L1, q/CNpq
L9 CCCNpqrCpr L3, S7 detachment
S8 CCCN p q CCCNpppCCqpp C p CCCNpppCCqpp L9, r/CCCNpppCCqpp
S9 CC Np q CCC Np p p CC q p p L6, p/Np, r/p, s/p
L10 CpCCCNpppCCqpp S8, S9 detachment
S10 C CCNppp CCCN CCNppp CCNppp CCNppp CC q CCNppp CCNppp L10, p/CCNppp
S11 CCCNCCNpppCCNpppCCNpppCCqCCNpppCCNppp L2, S10 detachment
S12 CCN CCNppp CCNppp CCNppp L2, p/CCNppp
L11 CCqCCNpppCCNppp S11, S12 detachment
S13 CCCN t CCNppp CCNppp C t CCNppp L9, p/t, q/CCNppp, r/CCNppp
S14 CC Nt CCNppp CCNppp L11 q/Nt
L12 CtCCNppp S14, S13 detachment
S15 CC t CC Np p p CC Np q C t CC q p p L7, p/Np, r/p, s/p
L13 CCNpqCtCCqpp L12, S15 detachment
S16 CC CNpq CtCCqpp CC CtCCqpp r C CNpq r L1 p/CNpq, q/CtCCqpp
L14 CCCtCCqpprCCNpqr L13, S16 detachment
S17 CCC NCCqpp CC q p p CCqpp CCN p q CCqpp L14, t/NCCqpp, r/CCqpp
S18 CCN CCqpp CCqpp CCqpp L2, p/CCqpp
L15 CCNpqCCqpp S18, S17 detachment
S19 CCCN p q CCqpp C p CCqpp L9, r/CCqpp
L17 CpCCqpp L15, S19 detachment
S20 CC q C CNpq q CC p CNpq C q C p q L5, p/q, q/CNpq, r/q, s/p
S21 C q CC Np q q L17, p/q, q/Np
S22 CCpCNpqCqCpq S20, S21 detachment
L18 CqCpq L3, S22 detachment
Now, since we have (q->(p->q)) as a theorem, by uniformly substituting thesis L1 for q, and L2 for p, since L1 holds as a thesis, we can obtain that (L1->L2) as a thesis, or equivalently, a theorem. So, consequently, one completely prove any thesis by any other thesis within the system using just detachment via a proof of the type "x, (x->y), y". What then does "independence" of logical axioms mean precisely?