GNU Aris Manual: im

Next: dm, Up: Equivalence Rules [Contents]

6.2.1 Implication

P → Q <=> ~P v Q

Implication uses the definition of the conditional. It is also valid to claim something such as ~(~P v Q) v (~R v S) <=> (P → Q) → (R → S), because implication is recursive.