前スレでビジービーバー関数の全域性うんぬん言ってたやつに致命的な間違いを見つけた。
ω矛盾の定義がおかしい。∃n∈(自然数)(Q(n))が証明可能なのに
Q(0),Q(1),Q(2),...がいずれも証明不能であることをω矛盾の定義といってたが、
これだとペアノ算術に例えば定数記号aを加えただけの拡張でも、
a = a から ∃n (a = n)が導出できる一方で、a = 0,a = 1,a = 2,... のいずれも証明不能で、
ω矛盾になる。しかし、これにa = 0という仮定を加えても無矛盾だから、
超準モデルになるとは限らない。

間違いの源はおそらく日本語版wikipediaだ。

"ω矛盾とは、自然数 n によって定まる論理式 Q(n) が存在して、次を満たすことをいう。
Q(0), Q(1), Q(2), …が全て証明可能であるが、「∃n： ¬Q(n) 」も証明可能である"

この記述は正しい。問題があるのはその下の、

"公理系が無矛盾であれば、対偶を取る事により、ω矛盾の概念が次と同値である事を示せる：
「∃n： Q(n) 」が証明可能であるが、Q(0), Q(1), Q(2), … のいずれも証明可能ではない。"

というところだ。最初の記述は「Q(0),Q(1),Q(2),...が証明可能で、かつ∃n(¬Q(n))も証明可能」
と言い換えられる。すると、実はAならばBの形になってないから、そもそも"対偶を取る"のは変だ。
英語版wikipediaには下の記述に該当する文は無い。
同値でないことも簡単に確認できる。ペアノ算術に定数記号aを加えただけの拡張は、
∃n(a = n)が証明可能で、a = 0, a = 1, ...が証明不能なことから下の記述を満たすが、
∃n(¬(a ≠ n))が証明可能な一方、a ≠ 0, a ≠ 1, ...は証明不能だから、上の記述を満たさない。
よって2つの記述は同値でない。
だから、前スレのあの証明では、「ビジービーバー関数の出力が超準的自然数になる」ことは
証明できていない、と言える。

あー、すっきりした