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?