■

授業第三回目は、自然演繹の論理結合子 ⇒ に関する証明の構造についてです。導入規則・除去規則を復習し、また回り道がない「きれいな証明」について取り上げます。また、同時に、論理結合子 ¬（ただし¬AはA⇒⊥の略記）の証明についても取り上げます。
きれいな証明とは、証明樹の上半部は除去規則のみ、下半部では導入規則のみを使うような証明です。多くの論理式はきれいな証明によって証明可能です。このような「きれいな」証明によってある論理式を証明するとは、まず前提を除去規則を使ってバラバラにし、これ以上分解できないぐらいにバラバラにしたら、今度はバラバラにされた部分論理式を導入規則を使って組み合わせていくという作業です。
ちなみに、今回の話は、後期にする「証明の正規化」という作業と深い関係があります。