Using Isabelle to verify special relativity, with application to hypercomputation theory

TL;DR

This paper demonstrates the formal verification of special relativity principles using Isabelle, aiming to ensure logical soundness and explore implications for hypercomputation and physical decidability.

Contribution

It introduces a machine-verified proof of a key relativity theorem within a formal logical framework, bridging physics and formal methods.

Findings

Successful Isabelle proof of 'No inertial observer can travel faster than light'

Enhanced confidence in the logical consistency of relativity theories

Insights into the axioms necessary for formal proofs in physics

Abstract

Logicians at the R\'enyi 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.