■

授業第三回目、自然演繹の⇒ と¬の証明についてです。導入規則・除去規則を復習し、また回り道がない「きれいな証明」について取り上げます。
きれいな証明とは、証明樹の上半部は除去規則のみ、下半部では導入規則のみを使うような証明です。多くの論理式はきれいな証明によって証明可能です。このような「きれいな」証明によってある論理式を証明するとは、まず前提を除去規則を使ってバラバラにし、これ以上分解できないぐらいにバラバラになったら、今度はバラバラにされた部分論理式を導入規則を使って組み合わせていくという作業です。