论文标题
典型的强迫，NP搜索问题和RII定理的扩展
Typical forcings, NP search problems and an extension of a theorem of Riis
论文作者
论文摘要
我们定义了典型的强迫，其中包含许多非正式的强迫参数，并为这种强迫提供了一般条件，以产生相关化的$ t^1_2 $的通用变体的模型。我们将此结果应用于研究总（2型）NP搜索问题的相对复杂性与有限组合原理相关。 复杂性理论比较了多项式时间的此类问题多一部分或图灵的减少。从逻辑的角度来看，这些问题是根据证明其整体的有限算术理论进行评分的。减少的逻辑类似物是从另一个问题中证明一个问题的总体。对于我们称之为相对界定算术的通用变体的两个观点之间的联系很紧密。我们加强了公共汽车和约翰逊（2012）的定理，该定理从多项式时间缩减可降低了相对有限的深度证明。 作为我们一般强迫方法的应用，我们得出了RIIS的有限定理的强烈形式（1993）。我们通过展示一个简单的模型理论属性来扩展它，该特性暗示着脱离相对化的$ t^1_2 $的通用变体加上弱鸽洞原理的独立性。更普遍地，我们表明，相对化的$ t^1_2 $的通用变体并未证明（与弱者相关的总NP搜索问题的总数）。基于原理在有限结构方面的行为基于仅部分定义的有限结构的行为。
We define typical forcings encompassing many informal forcing arguments in bounded arithmetic and give general conditions for such forcings to produce models of the universal variant of relativized $T^1_2$. We apply this result to study the relative complexity of total (type 2) NP search problems associated to finitary combinatorial principles. Complexity theory compares such problems with respect to polynomial time many-one or Turing reductions. From a logical perspective such problems are graded according to the bounded arithmetic theories that prove their totality. The logical analogue of a reduction is to prove the totality of one problem from the totality of another. The link between the two perspectives is tight for what we call universal variants of relativized bounded arithmetics. We strengthen a theorem of Buss and Johnson (2012) that infers relative bounded depth Frege proofs of totality from polynomial time Turing reducibility. As an application of our general forcing method we derive a strong form of Riis' finitization theorem (1993). We extend it by exhibiting a simple model-theoretic property that implies independence from the universal variant of relativized $T^1_2$ plus the weak pigeonhole principle. More generally, we show that the universal variant of relativized $T^1_2$ does not prove (the totality of the total NP search problem associated to) a strong finitary combinatorial principle from a weak one. Being weak or strong are simple model-theoretic properties based on the behaviour of the principles with respect to finite structures that are only partially defined.
