  In classical logic, "P implies Q" is equivalent to "not-P or Q". It is well
known that the equivalence is problematic. Actually, from "P implies Q", "not-P
or Q" can be inferred ("Implication-to-disjunction" is valid), while from
"not-P or Q", "P implies Q" cannot be inferred in general
("Disjunction-to-implication" is not generally valid), so the equivalence
between them is invalid in general. This work aims to remove exactly the
incorrect Disjunction-to-implication from classical logic (CL). The paper
proposes a logical system (IRL) with the expected properties: (1) CL is simply
obtained by adding Disjunction-to-implication to IRL, and (2)
Disjunction-to-implication is independent of IRL (either
Disjunction-to-implication or its negation cannot be derived in IRL) in the
general case. In other words, IRL is just the system obtained by exactly
removing Disjunction-to-implication from CL.
