始代数Kruskalの逆数学
## Trigger
chatgptで「Kruskal型の逆数学に対する統一的手法」という講演構想を読解した.長谷川立やAnton Freundによる,Kruskal theoremをinitial algebra・recursive datatypeへ一般化する研究と,Pakhomov–Walshによるreflection principleの反復を同じ図に置いたことが出発点である.
## Idea
polynomial functor等のinitial algebra
[
mu F
]
に,材料となるwqoから誘導される埋め込み順序を入れる.「(mu F)がwqoである」というKruskal型定理のreverse-mathematical strengthを,(F)に付随するordinal/dilator dataから構成したreflection principleのiterationとして一様に計算できるかを問う.
目標は個々のtree theoremを別々に分析することではなく,
[
Flongmapsto ext{reflection rank of the Kruskal theorem for }mu F
]
という構造的対応を作ることである.List,finite tree,一般のWPO-dilatorを最初の比較対象とする.
## Goal
initial algebraの圏論的構造とproof-theoretic ordinal/reflection rankを結び,Kruskal型reverse mathematicsの統一計算法を与える.既存研究の組合せから生じたprogramであり,新規性と実現可能性は未確認.