無矛盾性証明とは何か、何であるべきか

ウヒくんと名乗るおそらく数学者の方のブログ記事「世界共通の言語」より引用

多くの人にとって自然数の存在というのは明らかであって、
したがってモデルが存在する以上、
自然数論（ＰＡ）の無矛盾性は明らかである。
とすると無矛盾性証明を試みる意図がよく分からないし、
話によれば、ある程度大きい順序数の
超限帰納法を用いることで証明できるそうだが、
帰納法を仮定した時点で、
ほとんど自然数の存在を認めているようなものではないか。
という疑問も生じるのである。

PAの無矛盾性証明の意図については話は簡単です。そもそも、自然数の存在を示すために無矛盾性証明を行っているのではありません。PAが無矛盾であるという結果そのものは、今となってはあまり重要ではありません。重要なのは、証明に必要な順序数が であり、それよりも小さくすることができない事実です。

無矛盾性証明にどの順序数までの超限帰納法を必要とするかは、体系の強さを計る強力な物差しです。PAの無矛盾性証明に 帰納法が必要である事実によって、数ある体系の中でのPAの位置が明確になったのです。

数理論理学(数学基礎論)は、数学的対象としての論理・計算・集合などを研究する数学の一分野です。数学の基礎付けだけを扱っているのではありません。

失礼を承知で書きますが、ウヒくんさんは、数学の基礎付けに興味を持たない数理論理学研究者が、基礎付けを興味の中心とする研究者よりも、人数だけ比べると圧倒的に多いことをご存じないのでしょう。数学基礎論の研究者はみな、数学の基礎付けを研究していると誤解されていて、そのために、PAの無矛盾性証明の位置付けが見えないのでしょう。