4.5 now の使い方

 さらに証明のスケルトンですが,not pを証明するのに,nowを使うことがあります.now は次のように使います.

     now assume p;
     ······
     ······
     thus contradiction;
    end;



 now は now 〜 end で1つの文(論理式)とみなします.この now 〜 end は,not p と同じものです.あるいは,assume p で, p implies contradiction という論理式です.