Medvedev逻辑是不可判定的
Medvedev logic is undecidable
浏览论文内容
中文总结 AI 辅助
本文通过将周期性平铺问题归约到非定理性，证明了Medvedev逻辑不可判定，并类似地证明了Skvortsov逻辑的不可判定性及两者的区别，解决了一个长期开放问题。
中文摘要 AI 辅助
我们证明了Medvedev的有限问题逻辑（一种著名的超直觉主义逻辑）是不可判定的。关键方法是将周期性平铺问题归约到Medvedev逻辑中的非定理性。这解决了一个长期悬而未决的问题。使用类似的技术，但改为归约到普通平铺问题，我们同样获得了Skvortsov的无限问题逻辑的不可判定性，以及这两个逻辑是不同的这一事实——实际上，它们被平面的任何非周期平铺所区分。由于Medvedev逻辑出现在许多不同领域，这些结果对多个领域都有影响——例如，对诸如命题依赖逻辑等逻辑的示意片段的研究，或对拓扑斯内部逻辑的研究。不可判定性证明的核心思想和技术工作是通过ChatGPT Sol 5.6获得的，并由Claude Opus 5在Lean中进行了形式化验证。一个详细的方法论部分概述了如何获得这些结果。
英文摘要
We show that Medvedev's logic of finite problems, a well-known superintuitionistic logic, is undecidable. The key method is a reduction from the periodic tiling problem to non-theoremhood in Medvedev's logic. This settles a longstanding open problem. Using similar techniques, but reducing instead to the ordinary tiling problem, we likewise obtain undecidability of Skvortsov's logic of infinite problems, and the fact that the two logics are distinct -- in fact, they are separated by any aperiodic tiling of the plane. Due to the fact that Medvedev's logic figures in so many different areas, these results have implications for several fields -- for example, the study of schematic fragments of logics such as propositional dependence logic, or the study of internal logics of toposes. The core idea and technical work of the undecidability proof were obtained using ChatGPT Sol 5.6, and formally verified in Lean by Claude Opus 5. A detailed methodology section outlines how such results were obtained.
