# Derivation of implicational propositional axioms

Is there a way to subtract and add properties of axioms to generate new axioms?

For example:

{L} = {P S K} // natural deduction

{P S K} = {P H K I} // natural deduction

{S K} = {?} // constructive logic

{K I} = {?}

Where:

L = ((A -> B) -> C) -> ((C -> A) -> (D -> A)) // Łukasiewicz's axiom system

P = ((A -> B) -> A) -> A // Piece's Law

H = (A -> B) -> ((B -> C) -> (A -> C)) // Weak hypothetical syllogism

S = (A -> (B -> C)) -> ((A -> B) -> (A -> C))

K = A -> (B -> A)

I = A -> A

I want to be able to be able to add and subtract axioms such that P + S + K = P + H + K + I implies S encodes the properties of H + I

I'm probably using unjustified assumptions here. For example, I assume you can derive S from H and I, without using P or K. Ideally, there would be a way to automate the process of constructing and destructing axioms (though it'd probably be NP hard).

A similar definition is $\mathbf{A} + \mathbf{B} = \mathbf{A} \land \mathbf{B}$, but then you need to interpret equality as logical equivalence. The definitions then become completely equivalent.
However, you can't "cancel" axioms. If you know that $\mathbf{A}+\mathbf{B} = \mathbf{A}+\mathbf{C}$ then all you can conclude is that in the presence of $\mathbf{A}$, $\mathbf{B}$ and $\mathbf{C}$ are equivalent. As an example, let $\mathbf{A}$ be $x=0$, let $\mathbf{B}$ be $y=1$, and let $\mathbf{C}$ be $x+y=1$. In the presence of $\mathbf{A}$, the axioms $\mathbf{B}$ and $\mathbf{C}$ are equivalent, but in general they aren't.
If are are really keen on the cancellation law, you can always take formal sums. It is then true that $\mathbf{A}+\mathbf{B} = \mathbf{A}+\mathbf{C}$ implies $\mathbf{B}=\mathbf{C}$, but at the cost of $\mathbf{A}+\mathbf{B}$ having no other meaning than the formal sum of $\mathbf{A}$ and $\mathbf{B}$.