论文标题
强迫作为计算过程
Forcing as a computational process
论文作者
论文摘要
我们研究了如何将设置理论强迫视为集合理论模型的计算过程。鉴于有关集合理论模型$ \ langle m，\ in^m \ rangle $的信息，我们可以解释一种感觉，其中一个人可以计算$ m $ generic滤波器$ g \ subseteq \ subseteq \ subseteq \ mathbb {p} \ in m $和相应的强迫扩展扩展$ m [g] $。具体而言，从原子图中可以计算$ g $，从$Δ_0$ -DIAGRAGRAM中，一个人可能会计算$ m [g] $及其$Δ_0$ -DIAGRAGR，并且从基本图中可以计算$ m [g] $的基本图。我们还研究了使过程功能功能所需的信息，并得出结论，在一般情况下，这种计算过程将不起作用。对于任何这样的过程，总是有可能对设置理论$ m $模型的不同异构呈现，从而导致不同的非同构强迫扩展$ m [g] $。实际上，从这种意义上讲，没有鲍尔功能提供通用过滤器。
We investigate how set-theoretic forcing can be seen as a computational process on the models of set theory. Given an oracle for information about a model of set theory $\langle M,\in^M\rangle$, we explain senses in which one may compute $M$-generic filters $G\subseteq\mathbb{P}\in M$ and the corresponding forcing extensions $M[G]$. Specifically, from the atomic diagram one may compute $G$, from the $Δ_0$-diagram one may compute $M[G]$ and its $Δ_0$-diagram, and from the elementary diagram one may compute the elementary diagram of $M[G]$. We also examine the information necessary to make the process functorial, and conclude that in the general case, no such computational process will be functorial. For any such process, it will always be possible to have different isomorphic presentations of a model of set theory $M$ that lead to different non-isomorphic forcing extensions $M[G]$. Indeed, there is no Borel function providing generic filters that is functorial in this sense.
