ただの走り書きです。
ZFC + 最小の弱マーロ基数が存在する の下で Jäger ψ は定義されている。
ここから「最小の弱マーロ基数が存在する」という公理を外すという議論はこのような感じなのだろうか。
Jäger ψ の順序数表記 S から順序を保って最小の弱マーロ基数以下の順序数まで写す写像を構成する。これにより順序数の整礎性を利用して順序数表記の整礎性が分かる。
S から再帰的類似を利用した ω _ 1 以下の順序数で写す写像を構成する。この際に上記の写像の構成を参考にできる。この議論は ZFC のみで行える。
ゆえに S の整礎性は ZFC のみで証明できる。
このような議論ではないようだ。
最小の弱マーロ基数が存在するという事実を用いて証明した S の整礎性を利用して ω _ 1 への順序を保つ写像を作る。
ω _ 1 への順序を保つ写像が存在することを利用して S の整礎性を証明する。
うん、絶対これではないな。
T(M) \cap M が表記における正則基数の集合を表す……？
原論文を読むと、どうやら「参考にする」というだけのように見える。
Buchmann’s recasted ψ function が正則非可算基数に関して自由に定義されるように、基数が現れるところを条件を満たす順序数に一般化できれば Coq でも扱いやすそう？
Bachmann’s recasted ψ function においては再帰的な形で何回も操作を適用しても埋め尽くせないことが求められる……？
Coq において関数が全て再帰的なものだとして計算できることは内部で示せないこと。
Coq では正則性公理は排中律を導くため使えない。よって min ... のような構成は使えない。自分で min を求める関数を定義する必要がある。
Coq での証明が思いつくのは広義単調減少する列に辞書式順序をいれたものの整礎性ぐらいかもしれない。
Coq では Homotopy Type Theory を使わないと集合を直接扱いづらいかもしれない。
でも適切な Inductive 型を定義していけば何とかなるかもしれない。
ω の整礎性は証明できた。ω ^ ω の整礎性も証明できるだろう。そして ε _ 0 以下の整礎性は証明できるだろう。
Coq では sup を構成できる。
不動点を数え上げる関数を構成できるかだが、これはおそらく構成できない。
いや、構成できるかもしれない。
a よりも大きい f b = b を満たす b を求める方法がある。
すなわち forall x : A, exists y : A, x <= y /\ f y = y である。
y [ 0 ] = x
y [ n + 1 ] = f ( y [ n ] )
このような列を作る。
y := sup { n < ω } ( y [ n ] )
これが期待する値となる。
この方法がうまくいけば Veblen 関数まで構成できる。
以上の証明は Wikipedia を参考にした。
https://en.wikipedia.org/wiki/Fixed-point_lemma_for_normal_functions
やはり大きな壁は順序数崩壊関数であり、正則性の公理がない以上 ψ ( x ) = min { a | a \notin C ( x ) } のような構成を取れない。
Bachmann’s recasted ψ function では ψ ( x ) = min { a | sup ( C ( x, a ) \cap Ω ) = a } という定義をしているわけだが、順序数の比較を計算することができない。
正則性の公理の他にも、内包による定義をしているのもやばい。非可述性の塊じゃないか？
非可述には非可述をということで forall V, (forall V, V -> Term V) -> Term V みたいな項を追加するのが有効かもしれない。
たとえば Bachmann’s recasted ψ function で ψ_Ω(Ω) を fun v => ψ_Ω(v) に対応づけるとか。
これ自体は Coq の Inductive 定義における制限に引っかかって出来ないけど PHOAS のように回避は出来るはず。