「数理論理学」の概要

数学ではよく証明を行います。しかし、ある理由付けの文章が証明として認められるか否かは、どのようなしくみによって定められているのでしょうか。高校までの数学では、このことがきちんとは扱われていません。もちろん、個々の問題に対する証明の例、背理法などの証明方法の例は与えられていますが、それらがなぜ証明として、あるいは証明方法として認められているのかについてはふれていません。実際にある理由付けの文章が証明として認められるか否かを判断するには、今まで経験した証明の例などにたよるしかないことになります。高校までにおこなった証明が本当に認められるべきものであることを確認するには、証明というものを規定するしくみを知る必要があります。この講義では、G. Gentzenの方法に従って、証明のしくみを整理していきます。

授業の例

G. Gentzen によって与えられた自然演繹法は、証明すべき文の形などによってその証明の形を規定する方法です。ここでは、「Pでない」という形の文の証明の形を紹介しましょう。まずは、「Pでない」を導く証明を２つあげてみます。

どちらの例も、「Pであると仮定して矛盾を導く」という形で「Pでない」という形の文の証明をしている、ということに気がついたでしょうか。 Gentzenの規定した証明の形もこれと同じです。すなわち、「Pでない」の証明の形は「Pであると仮定して矛盾を導く」ことによって与えることができる、と規定されているのです。

授業では、Gentzenの方法によって証明のしくみを解説します。そして、上のような証明の例をいくつかあげ、それらが本質的にはGentzenの方法で与えられていることを確かめていきます。