Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems

TL;DR

This paper formalizes an axiomatic system for Minkowski spacetime inspired by Hilbert's approach, emphasizing symmetry and generality, with proofs implemented in Isabelle/Isar to support studies in Special Relativity.

Contribution

It introduces a Hilbert-style axiomatic formalization of Minkowski spacetime, focusing on linear order and symmetry, with proof scripts demonstrating the approach.

Findings

Axiomatic system for Minkowski spacetime formalized in Isabelle/Isar

Theorems related to linear order formalized and proved

Use of symmetry and 'without loss of generality' reasoning emphasized

Abstract

This contribution reports on the continued formalisation of an axiomatic system for Minkowski spacetime (as used in the study of Special Relativity) which is closer in spirit to Hilbert's axiomatic approach to Euclidean geometry than to the vector space approach employed by Minkowski. We present a brief overview of the axioms as well as of a formalisation of theorems relating to linear order. Proofs and excerpts of Isabelle/Isar scripts are discussed, with a focus on the use of symmetry and reasoning "without loss of generality".