Consider a certain formal system with only axiom Excluded Middle -$EM$
[![enter image description here][1]][1]
and 18 inference rules:
9 implicative ruules (clearly not independent)
[![enter image description here][2]][2]
and 9 tautological rules:
[![enter image description here][3]][3]
If we have substitution at hands as well but we are restricted no to use conditional proof.
Is this particular system complete?
I always believed that the system is complete. But once I decided to prove or disprove completeness I stuck. I neither can find any reference neither nor can proof completeness.
If someone is familiar with this system I would be grateful to have some reference or proof. [1]: https://i.sstatic.net/o5WuK.png [2]: https://i.sstatic.net/6nGnu.png [3]: https://i.sstatic.net/fUZCG.png