Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory
Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory
复制标题
直觉 Zermelo-Fraenkel 集合论的 Lifschitz 可实现性
DOI：
10.1007/s00153-012-0299-2
复制
发表时间：
2012
影响因子：
0.3
通讯作者：
Chen R
中科院分区：
文献类型：
--
作者：
Chen R
Lifschitz（Proc Am Math Soc 73：101-106，1979）介绍了一种海廷算法的可实现性的变体，它用唯一性条件验证了丘奇的论文，但不是丘奇论文的一般形式。与Kleene的函数可实现性（在Baire空间中）相对应的Lifschitz由货车Oosten（J SymbLog 55：805-821，1990）开发。在该文件中，他还延长Lifschitz' realizability二阶算术。这里的目标是将其扩展到完全直觉主义的Zermelo-Fraenkel集合理论，IZF。机器也将工作扩展的IZF与大集合公理。除了将Church的唯一性条件命题与直觉主义集合论中的一般形式区分开来外，我们还得到了几个有趣的推论。该解释否定了可数选择的弱形式ACω，ω，断言自然数的可居集合的可数族具有选择函数，ACω，ω由普通Kleene可实现性验证，并且当然在ZF中是可证明的。另一方面，AC ω，ω的一个关键结论，即柯西实数集和戴德金实数集是同构的，在这种解释中仍然有效。这种可实现性的另一个有趣的方面是，它验证了无所不知的有限原则。
A variant of realizability for Heyting arithmetic which validates Church’s thesis with uniqueness condition, but not the general form of Church’s thesis, was introduced by Lifschitz (Proc Am Math Soc 73:101–106, 1979). A Lifschitz counterpart to Kleene’s realizability for functions (in Baire space) was developed by van Oosten (J Symb Log 55:805–821, 1990). In that paper he also extended Lifschitz’ realizability to second order arithmetic. The objective here is to extend it to full intuitionistic Zermelo–Fraenkel set theory,IZF. The machinery would also work for extensions ofIZFwith large set axioms. In addition to separating Church’s thesis with uniqueness condition from its general form in intuitionistic set theory, we also obtain several interesting corollaries. The interpretation repudiates a weak form of countable choice,ACω,ω, asserting that a countable family of inhabited sets of natural numbers has a choice function.ACω,ωis validated by ordinary Kleene realizability and is of course provable inZF. On the other hand, a pivotal consequence ofACω,ω, namely that the sets of Cauchy reals and Dedekind reals are isomorphic, remains valid in this interpretation. Another interesting aspect of this realizability is that it validates thelesser limited principle of omniscience.