4.4 同値の証明


次に,p iff q (p ⇔ q) の証明の仕方ですが,これは p implies q を証明し,それから q implies p を証明します.p iff q は,p implies q & q implies p とシステムは自動的に解釈します.ですから,p implies q をいいますと,前半は証明したことになります.あとは後半の証明だけです.そうして assume q で,thus p となったので,これで p iff q がいえたと判断するわけです.


p iff q

proof

assume p;

...

thus q; p ⇒ q がいえた

assume q;

...

thus p; q ⇒ p がいえて p ⇔ q

end;