BB(x)をビジービーバー関数として、
「十分大きな自然数Mについて、0 < BB(M), 1 < BB(M), 2 < BB(M), ...が証明可能」
は証明できてないけど、もっと弱い主張である※ならば簡単に証明できる。
(∀n(n < BB(M))と、0 < BB(M), 1 < BB(M), ...は異なる。∀n (n < BB(M))からは、
例えばBB(M) + 1 < BB(M) を導出できるので明らかに矛盾)
※: 任意の無矛盾かつ帰納的公理化可能な公理について、ある自然数Mが存在して、
任意のn ∈ {0,1,2,...}について公理に n < BB(M) という式を加えてもなお無矛盾
やや分かりにくいけど、公理に0 < BB(M)とか1 < BB(M)とか 2 < BB(M)をいくら加えても
そこから矛盾が導出できない、ということ。ビジービーバー関数を扱える公理じゃないと
いけないので、多分自然数論を含むだろう。
