典型力迫、NP 搜索问题与 Riis 定理的一个推广

我们定义典型力迫，涵盖有界算术中许多非正式的力迫论证，并给出此类力迫产生相对化 $T^1_2$ 的泛化变体模型的一般条件。我们应用该结果研究对应于有限组合原理的总（2 型）NP 搜索问题的相对复杂性。复杂性理论依据多项式时间多一或图灵归约比较此类问题。从逻辑视角看，此类问题根据证明其实体性的有界算术理论分级。归约的逻辑类比是从一个问题的实体性证明另一个问题的实体性。两种视角之间的联系对于我们称之为相对化有界算术的泛化变体是紧密的。我们加强了 Buss 和 Johnson (2012) 的一个定理，该定理从多项式时间图灵可归约性推断实体性的相对有界深度弗雷格证明。作为我们一般力迫方法的应用，我们导出了 Riis 有限化定理 (1993) 的一种强形式。我们将其推广，给出一个简单的模型论性质，它蕴含相对于相对化 $T^1_2$ 的泛化变体加上弱鸽巢原理的独立性。更一般地，我们证明相对化 $T^1_2$ 的泛化变体不能从弱有限组合原理证明（对应于）强有限组合原理的总 NP 搜索问题的实体性。弱或强是基于原理在仅部分定义的有限结构上的行为所得的简单模型论性质。