結局、巨大数を求めるにあたってどこまで奇妙な性質をもつことを許容できるか
という哲学の問題なのかな。

いったんここでは自然数論のモデルに属しうるものはすべて自然数と呼ぶことに
して、以下の4つに分類しよう。特に断りがない場合、証明可能とは古典論理の
もとで証明可能であることを意味する。

(1)存在を直観主義論理のもとでも証明可能な自然数

例: ふぃっしゅ数ver6など、計算可能な手段で求められるもの

(2)存在を証明可能だが、直観主義論理のもとでは証明不能な自然数

例: ある程度大きな入力に対するビジービーバー関数やラヨ関数、
その他の計算不能関数の出力？

(2)の数は、さっきの※みたいな、任意のn∈{0,1,2,...}についてnより大きい
としても無矛盾、といったやや奇妙な性質をもつようになると思われる。

続く