|
|
|
|
|
Direction from right to left:
We assume
(Negated Implication.RA) ![[Graphics:indexgr60.gif]](indexgr60.gif)
and show
(Negated Implication.LC) ![[Graphics:indexgr61.gif]](indexgr61.gif)
.
We prove (Negated Implication.LC) by contradiction.
We assume
(Negated Implication.LC.pos) ![[Graphics:indexgr62.gif]](indexgr62.gif)
,
and show ![[Graphics:indexgr63.gif]](indexgr63.gif)
From (Negated Implication.RA.1) and (Negated Implication.LC.pos) we obtain by modus ponens
(Negated Implication.LC.pos.C) ![[Graphics:indexgr64.gif]](indexgr64.gif)
.
Formula (a contradiction) is proved because (Negated Implication.LC.pos.C) and (Negated Implication.RA.2) are contradictory.