Alternate axioms for relevant logic R

Relevant logic system R can be defined -as I read in D. Palladino, C. Palladino, Logiche non classiche- by the following axioms

1. A→A
2. (A→B)→((C→A)→(C→B))
3. (A→(A→B))→(A→B)
4. (A→(B→C))→(B→(A→C))
5. A∧B→A, A∧B→B
6. (A→B)∧(A→C)→(A→B∧C)
7. A→A∨B, B→A∨B
8. (A→C)∧(B→C)→(A∨B→C)
9. A∧(B∧C)→(A∧B)∧C
10. (A→¬B)→(B→¬A)
11. ¬¬A→A

together with the rules of modus ponens A,A→B⊢B and adjunction A,B⊢A∧B.

I read that axioms (2), (3) and (4) can be substituted by

2'. (A→B)→((B→C)→(A→C))

3'. (A→(B→C))→((A→B)→(A→C))

4'. A→((A→B)→B)

and axioms (1) and (4) also by

1''. ((A→A)→B)→B

4''. A→((A→A)→A)

(from which I see that the equivalence between A and (A→A)→A follows, as the authors say).

I am inclined to think that can be substituted means that the systems obtained by substituting the respective axioms are equivalent*, but I have not been able to prove the equivalence of the systems obtained by substituting the respective axioms. How can it be proved? I heartily thank you for any answer!

*By equivalence of the systems I mean:

(1),(2),(3),(4),(5),(6),(7),(8),(9),(10)⊢(1)∧(2')∧(3')∧(4')∧(5)∧(6)∧(7)∧(8)∧(9)∧(10)

and (1),(2'),(3'),(4'),(5),(6),(7),(8),(9),(10)⊢(1)∧(2)∧(3)∧(4)∧(5)∧(6)∧(7)∧(8)∧(9)∧(10)

and

(1),(2),(3),(4),(5),(6),(7),(8),(9),(10)⊢(1'')∧(2')∧(3')∧(4'')∧(5)∧(6)∧(7)∧(8)∧(9)∧(10)

and (1''),(2'),(3'),(4''),(5),(6),(7),(8),(9),(10)⊢(1)∧(2)∧(3)∧(4)∧(5)∧(6)∧(7)∧(8)∧(9)∧(10)

where I have used the number of the axioms as propositional symbols and where ⊢ represents deduction by using the two rules.

I take it that when you say "equivalent" you do not mean simply that the original axioms and their substitutes ought to each imply each-other (since that is true of any two axioms at all), but that they can effectively serve the same role in the system. That is, given the substituted axiom and the rest of the original axioms, you can get back to the original axiom for which the substitution was made. Then it seems to me that you are asking whether you can prove (1'') → (1) and (4'') → (4) given only the other original axioms and your two additional rules. Well, I can try...

This first proof strikes me as cheating just a little bit, since it does not convince me that there is really any sort of logical relationship between 1'' and 1, but I'll show you what I came up with anyway and let you decide:

1. ((A → A) → B) → B; assume (premise)
2. | A; assume (open conditional proof)
3. | A; by 2
4. A → A; close conditional proof
5. (((A → A) → B) → B) → (A → A); conclusion

So we have that (1'') → (1). I'll see whether I can come up with something more satisfying for the second dilemma:

1. A → ((A → A) → A); assume (premise)
2. | A → (B → C); assume (open conditional proof)
3. | | B; assume (open conditional proof)
4. | | | A; assume (open conditional proof)
5. | | | B → C; by 2, 4, modus ponens
6. | | | C; by 3, 5, modus ponens
7. | | A → C; close conditional proof
8. | B → (A → C); close conditional proof
9. (A → (B → C)) → (B → (A → C)); close conditional proof
10. [A → ((A → A) → A)] → [(A → (B → C)) → (B → (A → C))]; conclusion

Then (4'') → (4). So, nope - it seems that I can't. Well, I don't feel that I have helped you (and, now that I notice it, I am not even sure that the R allows for the conditional proof structure I've used), but on the off chance that you might appreciate my reply to some small degree, I think I will post it anyway.

Best of luck with any future answers!

• Thank you very much for your answer, which has been useful and is making me believe that the systems are indeed equivalent! By equivalence of the systems I mean that, if we substitute the corresponding axioms, we get sets of axioms implying each other, cfr. added note in the original post. It remains to prove that from (2') and (3') (together with (1''),(4''),(5),(6),(7),(8),(9),(10)) the "original" axioms (1),...,(10) follow to complete the (1''),(2'),(3'),(4''),(5),(6),(7),(8),(9),(10)⊢(1)∧(2)∧(3)∧(4)∧(5)∧(6)∧(7)∧(8)∧(9)∧(10) part... – Self-teaching worker Mar 15 '15 at 10:56