What Does it Mean Exactly to Claim Logical Theorems (Axioms) Independent?

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?

-
Consider writing in standard notation: using non-standard notation distracts from the actual question. –  Zhen Lin Aug 28 '11 at 3:32
Yes, actually. I'm more used to that notation. At the moment I can't figure out what your question is about because I have to expend considerable effort translating your formulae into expressions I can understand. –  Zhen Lin Aug 28 '11 at 5:41
This looks to me like saying a set of vectors $u,v,w$ can't be (linearly) independent, because you can express $u$ as a linear combination, $u=1\cdot u+0\cdot v+0\cdot w$. It's linearly independent if you can't express $u$ as a linear combination of the other vectors. I think that's what Carl is saying in his answer. –  Gerry Myerson Aug 29 '11 at 3:30
Doug, I realize it's probably been a lot of effort to post what you have, but honestly this Polish notation is still fairly alien to me. However, I trust the conclusion q->(p->q) whenever p because it's fairly intuitive. The thing is, given this, you can't derive (x->y) without assuming y in the first place, no? Then it doesn't make sense to set out to show y follows solely from the other set of axioms, and then assume y as a theorem in the very process. Independence means y can follow exclusively from the other axioms - to not understand this is to miss the whole point of the term. –  anon Aug 29 '11 at 6:38

We could say that $A$ is independent of a set of axioms $B$ if $A$ is not an admissible rule over $B$, or if $A$ is not a derivable rule over $B$. For definitions, see the Wikipedia article on rules of inference. In either case, when asking whether a rule is independent of some other rules, you would take the set of other rules for $B$, not the set including $A$ itself.

-
By this definition, then, would you say that since "strict implication" is not truth-functional, that the rule of substitution, and the rule of replacement both qualify as independent of the rules of modal logic, since those rules rely upon truth-functionality? –  Doug Spoonwood Aug 29 '11 at 4:25
I don't know whether they are independent rules. First, you have to decide whether you want to show that one of them is not admissible, or whether you want to show it is not derivable, from the other rules. Then you need to construct an example to show that rule really is not admissible, or really is not derivable, from the others. –  Carl Mummert Aug 29 '11 at 11:06

In classical propositional logic, we say that a formula $\varphi$ is independent from a theory (i.e. a set of formulas) $T$ if $T \nvDash \varphi$ and $T \nvDash \lnot \varphi$. Alternatively, if $T \cup \{\varphi\}$ and $T \cup \{\lnot \varphi\}$ are both satisfiable. Obviously any classical propositional tautology is part of the classical propositional logic and cannot be independent from any theory.

More generally, assume that we have a logic (which gives us some definition for $T \vDash \varphi$). We can similarly define the independence of a formula from a theory w.r.t. that logic.

-

Let's call a theorem or axiom A dependent if given a set Z of axioms and primitive inference rules, then a proof of A can get written from Z. An axiom is independent of Z if given Z, then a proof of A cannot get written. A set of axioms S for system Y comes as independent if each subsystem of Y with just one less axiom under the same rule(s) of inference as Y cannot prove the axiom omitted.

-