The minimization principle MIN($\prec$) studied in bounded arithmetic in [Chiari, M. and Kraj\'i\v{c}ek, J. Witnessing Functions in Bounded Arithmetic and Search Problems, Journal of Symbolic Logic, 63(3):1095-1115, 1998] says that a strict linear ordering $\prec$ on any finite interval $[0,\dots,n)$ has the minimal element. We shall prove that bounded arithmetic theory $T^1_2(\prec)$ augmented by instances of the pigeonhole principle for all $\Delta^b_1(\prec)$ formulas does not prove MIN($\prec$).
翻译:[Chiari, M. 与 Kraj\'i\v{c}ek, J. 在《有界算术中的见证函数与搜索问题》(《符号逻辑杂志》,63(3):1095-1115, 1998)中研究的有界算术最小化原理MIN($\prec$)断言:任何有限区间$[0,\dots,n)$上的严格线性序$\prec$均存在最小元。本文将证明:对于所有$\Delta^b_1(\prec)$公式的鸽笼原理实例所扩充的有界算术理论$T^1_2(\prec)$,无法推导出MIN($\prec$)。