No Faster-Than-Light Observers (GenRel)

Mike Stannett 📧, Edward Higgins, Hajnal Andreka 🌐, Judit Madarasz 🌐, István Németi 🌐 and Gergely Szekely 🌐

March 5, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

We have previously verified, in the first order theory SpecRel of Special Relativity, that inertial observers cannot travel faster than light. We now prove the corresponding result for GenRel, the first-order theory of General Relativity. Specifically, we prove that whenever an observer m encounters another observer k (so that m and k are both present at some spacetime location x), k will necessarily be observed by m to be traveling at less than light speed.

License

BSD License

Topics

Related publications

  • https://isa-afp.org/entries/No_FTL_observers.html

Session No_FTL_observers_Gen_Rel

Cite

× 
@article{No_FTL_observers_Gen_Rel-AFP,
  author  = {Mike Stannett and Edward Higgins and Hajnal Andreka and Judit Madarasz and István Németi and Gergely Szekely},
  title   = {No Faster-Than-Light Observers (GenRel)},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/No_FTL_observers_Gen_Rel.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: