Defining implication relation for classical logic
From MaRDI portal
Abstract: 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.
This page was built for publication: Defining implication relation for classical logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6247725)
