Medvedev逻辑不可判定：它是π₀¹完全的。谁能猜到？
Medvedev Logic is Not Decidable. It is π01 -complete. Who Would Have Guessed?
浏览论文内容
中文总结 AI 辅助
本研究证明Medvedev逻辑ML在可计算多一归约下是π₀¹完全的，从而不可判定且非递归可枚举；通过构造Wang-Medvedev对，将周期性平铺与直觉主义公式反模型联系起来，给出证明。
中文摘要 AI 辅助
本项目始于一个尝试：借助生成式人工智能系统证明Medvedev逻辑是可判定的。作者（以及生成式人工智能系统——至少在我询问它们时它们如此声称）对其最终结论感到惊讶。我们证明了Medvedev逻辑ML，即有限问题的中间逻辑，在可计算多一归约下是π₀¹完全的。因此，ML不是递归可枚举的，更不用说不可判定了，并且不存在递归可枚举的可靠且完备的证明演算。该证明通过一个我们称之为Wang-Medvedev对的共享中间结构，将周期性多米诺问题与直觉主义公式联系起来。这样的对由一个有限偏序的角色集合连同需求组成。需求定义了角色之间的交互。一个实现用这些角色标记有限集的非空子集，尊重序并满足需求。我们将一个对与每个有限Wang系统相关联，并证明该对有一个实现当且仅当该系统平铺一个有限环面。然后我们构造一个直觉主义公式，该公式在某些有限Medvedev框架上失败当且仅当同一对是可实现的。因此，可实现性提供了周期性平铺与反模型之间的联系。
英文摘要
This project began as an attempt to prove that Medvedev logic is decidable with the help of generative AI systems. The author (as well as the generative AI systems, or at least they claim to be since I have asked them) was surprised by its eventual conclusion. We prove that Medvedev logic ML, the intermediate logic of finite problems, is Pi-01-complete under computable many-one reductions. Consequently, ML is not recursively enumerable, a fortiori undecidable, and admits no recursively enumerable sound and complete proof calculus. The proof connects the periodic domino problem with intuitionistic formulas through a shared intermediate structure that we call a Wang-Medvedev pair. Such a pair consists of a finite partially ordered set of roles together with demands. Demands define the interaction between roles. A realization labels nonempty subsets of a finite set with these roles, respecting the order and satisfying the demands. We associate a pair with each finite Wang system and show that it has a realization iff the system tiles a finite torus. We then construct an intuitionistic formula that fails on some finite Medvedev frame iff the same pair is realizable. Realizability thus provides the link between periodic tilings and the countermodels.
