Attempt a proof by contradiction. It doesn't quite work.
Chris Pressey
4 years ago

112 | 112 | end |

113 | 113 | end |

114 | 114 | Step_6 = or(b, a) by Tautology with Step_5 |

115 | qed | |

116 | ===> ok | |

117 | ||

118 | ### Proof by Contradiction ### | |

119 | ||

120 | If we assume p and show that it leads to a contradiction, | |

121 | we can then infer ¬p. If we can use proof by contradiction, | |

122 | we can derive Modus Tollens. | |

123 | ||

124 | given | |

125 | Modus_Ponens = impl(P, Q) ; P |- Q | |

126 | ||

127 | Double_Negation = not(not(P)) |- P | |

128 | Contradiction = P ; not(P) |- bottom | |

129 | Explosion = bottom |- P | |

130 | ||

131 | block Reductio_ad_Absurdum | |

132 | Supposition = A{term} |- A | |

133 | Conclusion = bottom |- not(A) | |

134 | end | |

135 | ||

136 | Premise_1 = |- impl(p, q) | |

137 | Premise_2 = |- not(q) | |

138 | show | |

139 | not(p) | |

140 | proof | |

141 | Step_1 = impl(p, q) by Premise_1 | |

142 | Step_2 = not(q) by Premise_2 | |

143 | block Reductio_ad_Absurdum | |

144 | Step_3 = p by Supposition with p | |

145 | Step_4 = q by Modus_Ponens with Step_1, Step_3 | |

146 | Step_5 = bottom by Contradiction with Step_4, Step_2 | |

147 | Step_6 = not(p) by Conclusion with Step_5 | |

148 | end | |

149 | Step_7 = not(p) by Tautology with Step_6 | |

115 | 150 | qed |

116 | 151 | ===> ok |

117 | 152 |