Skip to main content
2 of 2
Commonmark migration

Completeness of certain formal deduction system

Consider a certain formal system with only axiom Excluded Middle -$EM$

enter image description here

and 18 inference rules:

9 implicative ruules (clearly not independent)

enter image description here

and 9 tautological rules:

enter image description here

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.