Using Isabelle/HOL to Verify First-Order Relativity Theory

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

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2014-04, Vol.52 (4), p.361-378
Main Authors: Stannett, Mike, Németi, István
Format: Article
Language:English
Subjects:
Algorithmics. Computability. Computer arithmetics
Applied sciences
Artificial Intelligence
Automated reasoning
Computer Science
Computer science
control theory
systems
Consistency
Exact sciences and technology
Exploitation
Logic and foundations
Logical, boolean and switching functions
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Mathematical logic, foundations, set theory
Mathematical models
Mathematics
Observers
Proof theory and constructive mathematics
Proving
Relativity
Sciences and techniques of general use
Set theory
Symbolic and Algebraic Manipulation
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 unsolvable questions such as the Halting Problem and the consistency of set theory. 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 a first-order proof in Isabelle/HOL of the theorem “no inertial observer can travel faster than light”. This approach to physical theories and physical computability has several pay-offs, because the precision with which physical theories need to be formalised within automated proof systems forces us to recognise subtly hidden assumptions.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-013-9292-7