contradiction

否定が論理式に含まれているとき使えるタクティクを勉強しました。 introタクティク：ゴールがある命題の否定¬ Aである場合、intro hとすると仮定h: Aが導入されて、ゴールがFalse (矛盾)に変わります。仮定の集まりの中で適当な命題Bについてhb:Bとhbn:¬ Bを両方含むようにできれば最後にapply hb hbnで矛盾を導いて証明が終わります。 by_contraタクティク：ゴールが特に否定の形ではない場合でも、by_contra hとすることでゴールの否定を仮定hとして導入するとともに、ゴールをFlase(矛盾)にすることができます。仮定の中で矛盾を導くことで証明を終了させ…