Using Isabelle/HOL to Verify First-Order Relativity Theory

Stannett, M and Németi, István (2014) Using Isabelle/HOL to Verify First-Order Relativity Theory. JOURNAL OF AUTOMATED REASONING, 52 (4). pp. 361-378. ISSN 0168-7433

Preview

Text 1211.6468.pdf Available under License Creative Commons Attribution. Download (199kB) | Preview

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 machineverified 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.

Actions (login required)

Edit Item