It is a theorem or valid rule of replacement in classical logic that P implies Q is logically equivalent to not-P or Q, which means they can be replaced (in proofs) or defined (in axioms) by each other. It is well known that the equivalence is problematic as it is not actually valid. Specifically, from P implies Q, not-P or Q can be inferred (``Implication-to-disjunction'' is indeed valid), while from not-P or Q, P implies Q cannot be inferred (``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 subsystem of CL with Disjunction-to-implication being exactly removed.

翻译：这是经典逻辑中的一个定理或有效的替换规则：P蕴涵Q在逻辑上等价于非P或Q，这意味着它们可以在证明中相互替换，或在公理中相互定义。众所周知，这一等价性存在争议，因为它实际上并不成立。具体而言，从P蕴涵Q可以推出非P或Q（“蕴涵-析取”确实有效），而从非P或Q不能推出P蕴涵Q（“析取-蕴涵”无效），因此两者之间的等价关系不成立。本研究旨在从经典逻辑（CL）中精确移除错误的“析取-蕴涵”规则。本文提出一个逻辑系统（IRL），它具有以下性质：（1）在IRL中添加“析取-蕴涵”规则即可得到完整的CL；（2）“析取-蕴涵”规则独立于IRL，即该规则及其否定均无法在IRL中导出。换句话说，IRL正是精确移除“析取-蕴涵”规则后的CL子系统。