本文改造了匈牙利学者H. Andéka, J. X. Madarász, I. Nemeti等人构建的狭义相对论一阶公理系统Specrel，在语言中加入惯性观者iob作为常量，以此构建了明确的坐标系，在此基础上得到的Specrel_iob公理系统无论在公理上还是在性质上都比更加清晰。
在Specrel_iob公理系统中，我们将惯性观者、光子、测地线等物理概念用可定义集的方式表示出来，减少了语言中使用的谓词个数；同时，我们研究了观者iob的坐标系与其他惯性观者坐标系之间的关系，并得出了四维时空中洛伦兹变换的一般形式。
此外，狭义相对性原理作为Einstein提出的狭义相对论的两大原理之一，由于无法用一阶语言表述，因此没有出现在任何一个狭义相对论的一阶公理系统之中。本文在明确地用逻辑语言描述出坐标系建构的基础上，通过模型论中超积、超滤等方法，利用系统中实闭域的初等等价模型给出狭义相对性原理的证明。

The first-order logic axiomatic system Specrel_iob is an improvement system of Specrel which puts forward the first-order logical axioms of special relativity constructed by the Hungarian scholars H. Andéka, J. X. Madarász and I. Nemeti. The language has a new constant iob to represent an inertial observer through which a coordinate system could be constructed. And the axioms and properties of Specrel_iob are clearer than Specrel.
In this paper, the concepts of inertial observers, photons and geodesic lines etc. are put forward by definable sets such that the unnecessary predicates can be deleted. The connection of the coordinate systems between iob and other inertial observers is studied, as well as the general form of coordinate transformation of inertial coordinate systems, that is, the Lorentz transformation of four-dimensional space-time. 
Moreover, the principle of special relativity is one of the basic principles in Einstein’s theory of Relativity. But it is not in any of logic axiomatic systems because it cannot be expressed by first-order language. On the basis of clearly describing the construction of the coordinate system in logical language, the principle of special relativity is proved through constructing the elementary equivalence model of real closed field with ultraproduct and ultrafilter.