发表机构
Charles University, Faculty of Arts; University of Warwick, Department of Computer Science; Charles University, Faculty of Mathematics and Physics（查理大学文学院; 华威大学计算机科学系; 查理大学数学物理学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文概述有界算术中的多种力迫方法，与集合论力迫对比，指出可数框架可统一解释现有方法，并探讨类比能否发现新偏序。
AI 中文摘要
我们提供了有界算术中几种力迫方法的现代概述，并将其与集合论中的力迫进行比较。我们具体讨论了Atserias和Muller的可数力迫框架、Bydzovsky和Muller的受限超幂，以及Krajicek发展的随机变量力迫。我们通过回顾Paris--Wilkie力迫并给出Krajicek构造的浅层PHP模型的自包含构造来说明这些力迫论证。我们观察到，从形式角度看，Krajicek对不可数结构的力迫在通过LS论证进行可数塌缩后，可以在Atserias和Muller的框架中解释。我们进一步观察到，Bydzovsky和Muller的可数受限超幂（用于获得理论$T_{PV}$的模型）也可以在此框架中解释。这部分作为有界算术中现代力迫方法的入门。在下一部分，我们讨论算术与集合论中力迫之间的类比与差异。我们将Krajicek的布尔值模型嵌入集合论模型的泛型扩张中，观察到集合论力迫框架可用于解释算术中的力迫。在我们的解释中，集合论为形式化不可数结构的力迫论证提供了便捷方法。我们以一个疑问结束：与集合论的类比是否能促进发现算术中新的不可数偏序。
英文摘要
We provide a modern overview of several forcing methods in bounded arithmetic and compare them with forcing in set theory. We specifically discuss the countable forcing framework of Atserias and Muller, the restricted ultrapowers of Bydzovsky and Muller, and forcing with random variables developed by Krajicek. We illustrate these forcing arguments by reviewing the Paris--Wilkie forcing and by giving a self-contained construction of the shallow PHP model constructed by Krajicek. We observe that, from a formal point of view, Krajicek's forcing with uncountable structures can be interpreted in the framework of Atserias and Muller after a countable collapse using an LS argument. We further observe that the countable restricted ultrapowers of Bydzovsky and Muller, used to obtain models of the theory $T_{PV}$, can also be interpreted in this framework. This part serves as a primer on modern forcing methods in bounded arithmetic. In the next part, we discuss the analogies and differences between forcing in arithmetic and set theory. We embed Krajicek's Boolean-valued models into generic extensions of models of set theory, observing that the set-theoretic forcing framework can be used to interpret forcing in arithmetics. In our interpretation, set theory offers a convenient method for formalizing forcing arguments with uncountable structures. We end with a question whether analogies with set theory can facilitate the discovery of new uncountable partial orders for arithmetic.
Comments47 pages
