Rigorous formulation of special relativity. I want to understand the theory of special relativity and I am reading from Resnick's Introduction to Special Relativity.
But I want to prove everything rigorously.
$\newcommand{\R}{\mathbf R}$
$\newcommand{\mc}{\mathcal}$
$\newcommand{\vp}{\varphi}$
Of course, this requires the definitions to be rigorous.
So here is an attempt, which is really lame right now.
I am hoping those who already understand the theory can add to the formalism which I describe below.
I am trying to understand the theory for the simplest case where there is one spatial dimension and one temporal dimension.
Definition.
Spacetime is a $2$-dimensional smooth manifold homeomorphic to $\R^2$ whose elements are called events.
We will denote spacetime as $E$.
Definition.
A frame of reference is a global smooth chart $\vp:E\to \R^2$.
(The above definition of a frame of reference allows for all sorts of crazy things to be called frames of reference. So it needs more work.)
We postulate that spacetime comes equipped with certain spacial kind of subsets called photons, and the collection of all photons will be denoted by $\mc P$.
Definition.
A frame of reference $\vp:E\to \R^2$ will be called inertial if for each $P\in \mc P$, the set $\vp(P)$ is a straight line with slope $1$.
(What we are tying to say is that light travels with unit speed in an inertial frame).
Now I want to formalize Einstein's postulate that light travels with the same speed in all inertial frames.
For this first I need to defined what is meant by the velocity of a frame with respect to another.
Let $\vp$ and $\psi$ be two frames.
We want to track the origin of $\psi$ as seen by $\vp$.
If $s(t)$ is the spatial location of the origin of $\psi$ when $\vp$'s clock reads $t$ (that is amongst the events which have their second coordinate equal to $t$ under $\vp$, $s(t)$ is the first coordinate under $\vp$ of that event whose first coordinate is zero under $\psi$) the velocity of $\psi$ with respect to $\vp$ is $s'(t)$.
(Of course, this quantity may not even exist. or may not be well-defined because there could be multiple candidates for $s(t)$).
So we need to say some more words, which I am not sure about.
At any rate. Running with it, we have:

Any two inertial frames move at a constant speed with respect to each other.

Okay. So can somebody see as to how to develop this. Or perhaps there is a text where this approach has already been taken.
Just one more thing. I think one needs to insist that is $\vp:E\to \mathbf R^2$ is an inertial frame, and $\ell$ is a line with slope $1$, then $\vp^{-1}(\ell)$ is a photon. This is ugly I know. Perhaps there could be given a more intrinsic axiom to the set of all the photons.
What are your thoughts? Thanks.
 A: Since you seem unfamiliar with the nature of special relativity as the geometry of index 1 symmetric bilinear forms, aka "Lorentz forms", I think the best I can do is to give you a little bit of intuition about how these forms are connected to the reality of physical space time. This might allow you to realize the direction that one must go in order to formalize special relativity.
Beyond that, the best I can suggest is to suggest that you read on. I started with Resnick too, when I was a freshman, oh so many years ago, and it took me a long time until I properly appreciated the linear algebra basis of special relativity.
The starting point for special relativity in 2-dimensional space time is a 2-dimensional vector space $V$ equipped with a symmetric bilinear form $\langle v,w \rangle$ defined for all $v,w \in V$ such that the signature of this form is $(1,1)$. By definition, this means that $V$ has a basis in which the matrix of the form is $\begin{pmatrix}1 & 0 \\ 0 & -1\end{pmatrix}$.
Using these coordinates, we can identify $V$ with $\mathbb R^2$, and we can write the two coordinate functions as $x$, $t$. The first coordinate $x$ is usually called something like the "space-like" coordinate, and $t$ is called the "time-like coordinate". 
Given $p,q \in V$ representing two space-time events, it is useful to ponder the meaning of the quantity 
$$|q-p|^2 = -\langle q-p, q-p \rangle
$$
This quantity can be zero, positive, or negative, and I'll discuss the physical meaning of these possibilities.
Understanding a space time interval $|q-p|^2=0$ is a good start. Mathematically, this just means that the straight line through $p$ and $q$ has slope $\pm 1$. What $|q-p|^2=0$ means physically is that in order for a particle to move under inertia between the events $p$ and $q$, that particle must essentially be a photon: it must move at the speed of light (the coordinates have been normalized so that the speed of light equals $1$). 
In general, the world line of a photon, or any particle moving in a straight line at the speed of light, is a path of the form
$$f(s) = p_0 + s \cdot v
$$
where the vector $v$ satisfies $\langle v,v \rangle = 0$. The appearance of this world line in the space-time $V$ is that it is a line of slope $\pm 1$. 
The physical meaning of $|q-p|^2 > 0$ is that it is possible to move between the events $p,q$ by "real", inertial motion. Furthermore, if you move in that manner, and if your clock is ticking along, then the amount of time that your clock ticks off between $p$ and $q$ is equal to
$$|q-p| = \sqrt{|q-p|^2}
$$
Inertial motion from $p$ to $q$ is modelled by the parameterized path
$$f(s) = p + s u
$$
where $u = \frac{q-p}{|q-p|}$ (in order to be moving "forward" in time, the $t$ coordinate of the vector $u$ should be positive; in other words, $p$ is in the "past" of $q$ and $q$ is in the "future" of $p$). For example, if an object starts at $p_0=(x_0,t_0)$ and does not "move" in this coordinate system, then $u = (0,1)$ and the world line is 
$$f(s) = (x_0,t_0+s)
$$
The specific example of an unmoving particle sitting at the origin $x_0=0$ is $p(s)=(0,s)$. 
The physical meaning assigned to $|q-p|^2 < 0$ is that communication between the space time events $q$ and $p$ is impossible, because moving between them would require faster than light motion. So, for example, it is impossible to see what is happening at this exact moment one inch in front of your face.
A: 
Any two inertial frames move at a constant speed with respect to each other.

There's an important subtlety you're in danger of overlooking. The composition of two Lorentz boosts is in general not a Lorentz boost, but rather a composition of one with a rotation. If you want to flesh out the details properly, you'll need the theory of gyrovector spaces or something equivalent.

Perhaps there could be given a more intrinsic axiom to the set of all the photons.

I assume you mean luxons, since in theory photons aren't the only speed-$c$ particle. An alternative approach is to define speed-$c$ trajectories by $ds^2=\eta_{\mu\nu}dx^\mu dx^\nu=0$.
