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 valid), so the equivalence between them is invalid. This work aims to remove exactly the incorrect Disjunction-to-implication from classical logic (CL). The paper proposes a logical system (IRL), which has the properties (1) adding Disjunction-to-implication to IRL is simply CL, and (2) Disjunction-to-implication is independent of IRL, i.e. either Disjunction-to-implication or its negation cannot be derived in IRL. In other words, IRL is just the sub-system of CL with Disjunction-to-implication being exactly removed.

翻译：在经典逻辑中，“P蕴含Q”等价于“非P或Q”。众所周知，这一等价性存在问题。实际上，从“P蕴含Q”可以推出“非P或Q”（蕴含析取规则有效），而从“非P或Q”通常无法推出“P蕴含Q”（析取蕴含规则不成立），因此二者之间的等价性无效。本研究旨在从经典逻辑中精确移除错误的析取蕴含规则。本文提出一个逻辑系统（IRL），它具有以下性质：（1）向IRL添加析取蕴含规则后即得经典逻辑；（2）析取蕴含规则与IRL独立，即析取蕴含规则及其否定均不能在IRL中推导得出。换言之，IRL正是精确移除析取蕴含规则后的经典逻辑子系统。