使用Isabelle验证狭义相对论，并应用于超计算理论
Using Isabelle to verify special relativity, with application to hypercomputation theory
摘要：
布达佩斯雷尼数学研究所的逻辑学家花了几年时间发展了完全基于一阶逻辑的相对论（狭义、广义和其他变体），并通过利用宇宙学现象支持物理上的可判定性，以解决形式上不可判定的问题，如停止问题和集合论的一致性。匈牙利的理论非常广泛，它们的相关证明在直觉上非常令人满意，但这也带来了自己的风险，因为直觉有时会产生误导。作为一个联合项目的一部分，谢菲尔德的研究人员最近开始生成匈牙利证明的严格机器验证版本，以证明他们工作的可靠性。在本文中，我们解释了该项目的背景，并证明了定理的伊莎贝尔证明“没有惯性观察者可以比光速更快”。这种物理理论和物理可计算性的方法有几个好处：（a）我们可以肯定我们的直觉没有把我们引入歧途（或者如果有，我们可以确定这发生在哪里）;（b）我们可以确定在每个定理的证明中具体需要哪些公理，以及这些公理可以被削弱到什么程度（我们预先做的假设越少，结果就越强）;（c）我们可以确定在处理物理而不是数学理论时是否需要新的形式证明技术和策略。
英文摘要：
Logicians at the Rényi Mathematical Institute in Budapest have spent several years developing versions of relativity theory (special, general, and other variants) based wholly on first order logic, and have argued in favour of the physical decidability, via exploitation of cosmological phenomena, of formally undecidable questions such as the Halting Problem and the consistency of set theory. The Hungarian theories are very extensive, and their associated proofs are intuitively very satisfying, but this brings its own risks since intuition can sometimes be misleading. As part of a joint project, researchers at Sheffield have recently started generating rigorous machine-verified versions of the Hungarian proofs, so as to demonstrate the soundness of their work. In this paper, we explain the background to the project and demonstrate an Isabelle proof of the theorem "No inertial observer can travel faster than light". This approach to physical theories and physical computability has several pay-offs: (a) we can be certain our intuition hasn't led us astray (or if it has, we can identify where this has happened); (b) we can identify which axioms are specifically required in the proof of each theorem and to what extent those axioms can be weakened (the fewer assumptions we make up-front, the stronger the results); and (c) we can identify whether new formal proof techniques and tactics are needed when tackling physical as opposed to mathematical theories.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
