反推数学、杨图与升链条件

设 $S$ 为可数无限集的有限支撑置换群。设 $K[S]$ 为 $S$ 在特征为 $0$ 的域 $K$ 上的群代数。根据 Formanek 和 Lawrence 的一个定理，$K[S]$ 满足双侧理想的升链条件。我们研究了该定理的反推数学，证明了它在 RCA$_0$（甚至 RCA$_0^*$）之上等价于 $\omega^\omega$ 是良序的命题。我们的等价性证明是通过杨图构成良偏序这一命题进行的。