# The fragment of elementary plane Euclidean geometry based on
perpendicularity alone with complexity PSPACE-complete

Tatyana Ivanova  Institute of Mathematics and Informatics
Bulgarian Academy of Sciences
e-mail<EMAIL_ADDRESS>Tinko Tinchev  Faculty of Mathematics and
Informatics
Sofia University ”St. Kliment Ohridski”
e-mail<EMAIL_ADDRESS>
###### Abstract

A. Tarski uses in his system for the elementary geometry only the primitive
concept of point, and the two primitive relations betweenness and
equidistance. Another approach is the relations to be on lines instead of
points. W. Schwabhäuser and L. Szczerba showed that perpendicularity together
with the ternary relation of co-punctuality are sufficient for dimension two,
i.e. they may be used as a system of primitive relations for elementary plane
Euclidean geometry. In this paper we give a complete axiomatization for the
fragment of elementary plane Euclidean geometry based on perpendicularity
alone. We show that this theory is not finitely axiomatizable, it is decidable
and the complexity is PSPACE-complete. In contrast the complexity of
elementary plane Euclidean geometry is exponential.

##  1 Introduction

At the end of the 19th and the beginning of the 20th century investigations of
axiomatic approach to geometry were done by Hilbert, Pieri, Veblen and Pasch
(see [8, 11, 23, 24, 10]).

The first-order theory of Euclidean geometry was called elementary Euclidean
geometry.

Pieri introduced the relation $\mathbf{\Delta}$ with the following definition:
$\Delta(abc):=||ab||=||ac||$. The meaning of this relation is that the points
$a$, $b$ and $c$ form an isosceles triangle with base $|bc|$ (in the
degenerated cases either $b=c$ or $a$ is the midpoint of $|bc|$). Pieri proved
that $\Delta$ is sufficient as only primitive relation in terms of which the
whole elementary $n$-dimensional Euclidean geometry for $n\geq 2$ can be
developed.

Veblen ([23]) considered two primitive relations - the ternary relation of
betweenness $\mathbf{B}$ and the quaternary relation of equidistance
$\bm{\equiv}$. If $a$, $b$, $c$ and $d$ are points, then $B(a,b,c)$ means that
$b$ lies on the line segment joining $a$ and $c$; $ab\equiv cd$ means that the
distance from $a$ to $b$ is the same as the distance from $c$ to $d$. Veblen
proved that these primitive relations are sufficient for the elementary
geometry. He showed that $\equiv$ is undefinable in terms of $B$, although he
believed that he had proved the contrary ([24]). This mistake was noticed by
Tarski ([19]).

On the other hand, Pieri ([11]) showed that $B$ is first-order definable in
terms of $\equiv$ for every dimension $n\geq 2$. Thus $\equiv$ can be taken as
the only primitive for the elementary geometry.

In the 1920-70’s Tarski created an axiomatic system for the elementary
$n$-dimensional Euclidean geometry for $n\geq 2$ and this axiomatic system was
improved by Tarski and his students. The obtained theory is complete and
decidable, which was proved by means of quantifier elimination. In connection
with these results see [18, 20, 21, 6, 14, 22]. Tarski’s decision procedure
had nonelementary complexity. Later decision procedures, having elementary
complexity, were given by Monk, Solovay, Collins, Heintz, Roy, Solerno,
Renegar, Basu, Pollack and others ([5, 9, 7, 12, 2, 3]). The complexity of
these decision procedures is exponential.

If in Tarski’s system of geometry we replace the only axiom schema with a
second-order axiom we obtain an axiomatic system for full (non-elementary)
$n$-dimensional Euclidean geometry for $n\geq 2$ (see [20, 21]). If we remove
the dimension axiom, then we get a complete axiomatization of the dimension-
free Euclidean geometry ([15]).

Beth and Tarski ([4]) proved that no binary relation can be sufficient for the
elementary $n$-dimensional geometry for every $n\geq 2$. Still, Beth and
Tarski showed in [4] that the ternary relation $\mathbf{E}$, where $E(abc)$
means that the points $a$, $b$ and $c$ form an equilateral triangle (or $a$,
$b$ and $c$ coincide), can be taken as the only primitive for every dimension
$n\geq 3$ but it is not sufficient for dimension $1$ or $2$.

Szczerba and Tarski ([16, 17]) gave an axiomatization of the affine fragment
of the elementary plane Euclidean geometry - the fragment based on betweenness
relation alone.

Tarski used in his system for the elementary geometry only the primitive
concept of point, and the two primitive relations betweenness and equidistance
- the same primitive relations as Veblen. Another approach is the relations to
be on lines instead of points. Schwabhäuser and Szczerba ([13]) studied
relations on lines which can be taken as primitives for the elementary
Euclidean geometry. They proved that the binary relation of perpendicularity
$\mathbf{O}$ is sufficient for all dimensions higher than three; for dimension
three perpendicularity together with the binary relation of intersection of
lines suffice. Schwabhäuser and Szczerba considered also the ternary relation
of co-punctuality $\bm{\rho}$, meaning that three lines intersect at one
point. They showed that $O$ together with $\rho$ may be used as a system of
primitive relations for elementary plane Euclidean geometry. The paper [1]
studies the first-order theory of the fragment of elementary plane Euclidean
geometry based on the binary relations parallelism ($\mathbf{P}$) and
convergence ($\mathbf{C}$) of lines. The predicates $P$ and $C$ are definable
by $O$ and the converse is not true.

In this paper we give a complete axiomatization for the fragment of elementary
plane Euclidean geometry based on perpendicularity alone. We show that this
theory is not finitely axiomatizable, it is decidable and the complexity is
PSPACE-complete. Moreover the theory is $\omega$-categorical and not
categorical in every uncountable cardinality.

##  2 A complete axiomatization based on perpendicularity alone

We consider first-order language $\bm{\mathcal{L}}$ with predicate symbols $O$
(meaning perpendicularity) and $=$, without constants and functional symbols.
We consider the theory $\mathbf{SAPP}$, containing the following formulas:

$\mathbf{\lambda_{1n}}:\ \forall y_{1}\ldots\forall y_{n}\forall
s(O(s,y_{1})\wedge\ldots\wedge O(s,y_{n})\rightarrow\exists t(t\neq
y_{1}\wedge\ldots\wedge t\neq y_{n}\wedge O(s,t))),\ n\geq 1$

$\mathbf{\lambda_{2n}}:\ \forall y_{1}\ldots\forall y_{n}\exists s(\neg
O(s,y_{1})\wedge\ldots\wedge\neg O(s,y_{n})),\ n\geq 2$

$\mathbf{\lambda_{3}}:\ \forall x\neg O(x,x)$

$\mathbf{\lambda_{4}}:\ \forall x\forall y(O(x,y)\rightarrow O(y,x))$

$\mathbf{\lambda_{5}}:\ \forall x\exists yO(x,y)$

$\mathbf{\lambda_{6}}:\ \forall x\forall y\forall z\forall t(O(x,z)\wedge
O(y,z)\wedge O(x,t)\rightarrow O(y,t))$

###### Remark 2.1

We denote by $\mathcal{F}^{2}_{\mathbb{R}}$ the structure for the language
$\mathcal{L}$, having universe the set of all lines in Euclidean plane.
Clearly $\mathcal{F}^{2}_{\mathbb{R}}\models SAPP$.

###### Remark 2.2

We consider the binary predicate symbols $P$ (meaning that two lines are
parallel), $C$ (meaning that two lines intersect) and the ternary predicate
symbol $\rho$ (three lines intersect at one point). We denote by
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}$ the structure for the language
$\langle\ ;\ ;P,C,O,\rho,=\rangle$, having universe the set of all lines in
Euclidean plane. Clearly $\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models SAPP$.

###### Remark 2.3

We will denote by $A$, $B$, $C\ldots$ the universes of the structures
$\mathcal{A}$, $\mathcal{B}$, $\mathcal{C}\ldots$

###### Remark 2.4

Let $\varphi$ be a first-order formula with free variables
$x_{1},\ldots,x_{n}$, $\mathcal{A}$ be a structure for the language of
$\varphi$ and $a_{1},\ldots,a_{n}\in A$. By
$\mathcal{A}\models\varphi[a_{1},\ldots,a_{n}]$ we denote that $\varphi$ is
true in $\mathcal{A}$ under valuation, assigning $a_{1},\ldots,a_{n}$ to
$x_{1},\ldots,x_{n}$.

###### Remark 2.5

We will denote $a_{1},\ldots,a_{n}$ by $\overline{a}$ and
$f(a_{1}),\ldots,f(a_{n})$ by $\overline{f(a)}$.

###### Proposition 2.6

Let $\mathcal{A}$ be a model of $SAPP$. We consider the relation
$\mathbf{R_{1}}$, defined in the following way:

$xR_{1}y\stackrel{{\scriptstyle def}}{{\Longleftrightarrow}}\textmd{for every
}z,\ \neg O(x,z)\textmd{ or }O(y,z)$

(Intuitively $xR_{1}y$ means ”$x$ does not intersect $y$”.)

$R_{1}$ is an equivalence relation which divides $A$ into infinitely many
infinite equivalence classes.

Proof. Obviously $R_{1}$ is reflexive.

Let $x,y\in A$ and $xR_{1}y$. We will prove $yR_{1}x$. Let $z\in A$. We must
prove that $\neg O(y,z)$ or $O(x,z)$. Let $O(y,z)$. We will show that
$O(x,z)$. We have $\mathcal{A}\models\lambda_{5}$ and hence - there is $t\in
A$ such that $O(x,t)$. From here and $xR_{1}y$ we get that $O(y,t)$. From
$O(y,t)$, $O(x,t)$, $O(y,z)$ and $\mathcal{A}\models\lambda_{6}$ we obtain
that $O(x,z)$. Consequently $R_{1}$ is symmetric.

It can be easily verified that $R_{1}$ is transitive.

Suppose for the sake of contradiction that there are finitely many equivalence
classes - $[x_{1}],\ldots,[x_{n}]$. Using that
$\mathcal{A}\models\lambda_{2n}$ and $\mathcal{A}\models\lambda_{5}$, we get
that there are $s,z\in A$ such that $\neg O(s,x_{1}),\ldots,\neg O(s,x_{n})$,
$O(s,z)$. Clearly $z\overline{R_{1}}x_{1}$,
$z\overline{R_{1}}x_{2},\ldots,z\overline{R_{1}}x_{n}$ and hence
$[z]\neq[x_{1}],\ldots,[x_{n}]$ \- a contradiction. Consequently there are
infinitely many equivalence classes.

Let $[x]$ be an arbitrary equivalence class. Suppose for the sake of
contradiction that $[x]$ is finite, i.e. $[x]=\\{y_{1},\ldots,y_{n}\\}$ for
some $y_{1},\ldots,y_{n}\in A$. From $\mathcal{A}\models\lambda_{5}$ we obtain
that there is $y$ such that $O(y_{1},y)$. Let $i\in\\{2,\ldots,n\\}$. From
$y_{1}R_{1}y_{i}$ and $O(y_{1},y)$ we conclude that $O(y_{i},y)$. Using
$\mathcal{A}\models\lambda_{1n}$, we get that there is $t\in A$ such that
$t\neq y_{1},\ldots,t\neq y_{n}$, $O(y,t)$. We will prove that $y_{1}R_{1}t$.
Let $z\in A$. It suffices to prove that $O(y_{1},z)$ implies $O(t,z)$. From
$O(y_{1},y)$, $O(t,y)$ and $\mathcal{A}\models\lambda_{6}$ we conclude that
$O(t,z)$. Consequently $y_{1}R_{1}t$, i.e. $t\in[x]$, but we proved that
$t\neq y_{1},\ldots,y_{n}$ \- a contradiction. Consequently $[x]$ is infinite.
$\Box$

###### Definition 2.7

Let $\mathcal{A}$ be a model of $SAPP$, $R_{1}$ be the relation from the
previous proposition. We consider the equivalence classes modulo $R_{1}$ and
the following relation:

$[x]\mathbf{R_{2}}[y]\stackrel{{\scriptstyle
def}}{{\Longleftrightarrow}}O(x,y)$

It can be easily verified that this definition is correct and the following
proposition holds:

###### Proposition 2.8

Let $\mathcal{A}$ be a model of $SAPP$. Then for every equivalence class
modulo $R_{1}$ $[x]$ there is exactly one equivalence class $[y]$ such that
$[x]R_{2}[y]$. Moreover $[x]\neq[y]$.

###### Proposition 2.9

Let $\mathcal{A}$ be a countable model of $SAPP$, $\mathcal{B}$ be a model of
$SAPP$. Then $\mathcal{A}$ is elementary embedded in $\mathcal{B}$.

Proof. Since $\mathcal{A}$ is a countable model of $SAPP$, $A$ has countably
many equivalence classes. Let these equivalence classes be $[a_{1}]$,
$[a_{2}],\ldots,[a_{n}],\ldots,[a_{1}^{\prime}]$,
$[a_{2}^{\prime}],\ldots,[a_{n}^{\prime}],\ldots$, all they being different
and $[a_{1}]R_{2}[a_{1}^{\prime}]$,
$[a_{2}]R_{2}[a_{2}^{\prime}],\ldots,[a_{n}]R_{2}[a_{n}^{\prime}],\\\ \ldots$.
There exist countably many equivalence classes of $B$ $[b_{1}]$,
$[b_{2}],\ldots,[b_{n}],\ldots;\ [b_{1}^{\prime}]$,
$[b_{2}^{\prime}],\ldots,[b_{n}^{\prime}],\ldots$ such that all they are
different and $[b_{1}]R_{2}[b_{1}^{\prime}]$,
$[b_{2}]R_{2}[b_{2}^{\prime}],\ldots,[b_{n}]R_{2}$
$[b_{n}^{\prime}],\ldots$. For every $n$, $[a_{n}]$ and $[a_{n}^{\prime}]$ are
countable; $[b_{n}]$ and $[b_{n}^{\prime}]$ are infinite. Consequently for
every $n$, there are injections $h_{n}:\ [a_{n}]\rightarrow[b_{n}]$ and
$h_{n}^{\prime}:\ [a_{n}^{\prime}]\rightarrow[b_{n}^{\prime}]$.

We define the mapping $f$:

$f(a)=\left\\{\begin{array}[]{lll}h_{n}(a)&&\textmd{if }a\in[a_{n}]\textmd{
for some }n\\\ h_{n}^{\prime}(a)&&\textmd{if }a\in[a_{n}^{\prime}]\textmd{ for
some }n\end{array}\right.$

We will prove that $f$ is an elementary embedding of $\mathcal{A}$ in
$\mathcal{B}$. By induction on $\varphi$ we will prove that for every formula
$\varphi$, if $\varphi$ has free variables among $x_{1},\ldots,x_{n}$ and
$c_{1},\ldots,c_{n}\in A$, then
$\mathcal{A}\models\varphi[\overline{c}]\Leftrightarrow\mathcal{B}\models\varphi[\overline{f(c)}]$.
1) The base of induction is trivial.
2) $\varphi$ is $\neg\varphi_{1}$
The proof is obvious.
3) $\varphi$ is $\varphi_{1}\wedge\varphi_{2}$
The proof is obvious.
4) $\varphi$ is $\exists x\varphi_{1}$
Let the free variables of $\varphi$ be among $x_{1},\ldots,x_{n}$ and
$c_{1},\ldots,c_{n}\in A$. It can be easily verified that
$\mathcal{A}\models\exists x\varphi_{1}[\overline{c}]$ implies
$\mathcal{B}\models\exists x\varphi_{1}[\overline{f(c)}]$.

Let $\mathcal{B}\models\exists x\varphi_{1}[\overline{f(c)}]$. We will prove
$\mathcal{A}\models\exists x\varphi_{1}[\overline{c}]$. There exists $b\in B$
such that $\mathcal{B}\models\varphi_{1}[b,f(c_{1}),\ldots,f(c_{n})]$
Case 1: $b=f(a)$ for some $a\in A$
From the induction hypothesis and
$\mathcal{B}\models\varphi_{1}[f(a),f(c_{1}),\ldots,f(c_{n})]$ we get that
$\mathcal{A}\models\varphi_{1}[a,c_{1},\ldots,c_{n}]$ and hence
$\mathcal{A}\models\exists x\varphi_{1}[c_{1},\ldots,c_{n}]$.
Case 2: $b\neq f(a)$ for every $a\in A$
Case 2.1: $b\in[b_{i}]$ or $b\in[b_{i}^{\prime}]$ for some $i$
Without loss of generality $b\in[b_{i}]$ for some $i$. There is
$b^{\prime}\in[b_{i}]$ such that $b^{\prime}=f(a)$ for some $a\neq
c_{1},\ldots,c_{n}$. Since $b$, $b^{\prime}\in[b_{i}]$, $\neg O(b,b^{\prime})$
(we use the definition of $R_{2}$ and Proposition 2.8). We define a function
$g:\ B\rightarrow B$ in the following way:

$g(x)=\left\\{\begin{array}[]{lll}b^{\prime}&&\textmd{if }x=b\\\ b&&\textmd{if
}x=b^{\prime}\\\ x&&\textmd{otherwise}\end{array}\right.$

Obviously $g$ is a bijection. We will prove that $g$ is an automorphism. Let
$d_{1}$, $d_{2}\in B$. It suffices to prove that
$O(d_{1},d_{2})\Leftrightarrow O(g(d_{1}),g(d_{2}))$. We will consider only
the case when $d_{1}\notin\\{b,b^{\prime}\\}$, $d_{2}\in\\{b,b^{\prime}\\}$.
Without loss of generality $d_{2}=b$. It suffices to prove
$O(d_{1},d_{2})\Leftrightarrow O(d_{1},b^{\prime})$. We have
$bR_{1}b^{\prime}$ and using the definition of $R_{1}$ and its symmetry, we
get that $O(d_{1},b)\Leftrightarrow O(d_{1},b^{\prime})$. Consequently $g$ is
an automorphism.

We have $\mathcal{B}\models\varphi_{1}[b,f(c_{1}),\ldots,f(c_{n})]$.
Consequently $\mathcal{B}\models\varphi_{1}[g(b),g(f(c_{1})),\ldots,\\\
g(f(c_{n}))]$, i.e.
$\mathcal{B}\models\varphi_{1}[b^{\prime},f(c_{1}),\ldots,f(c_{n})]$. By the
induction hypothesis, $\mathcal{A}\models\varphi_{1}[a,c_{1},\ldots,c_{n}]$
and hence $\mathcal{A}\models\exists x\varphi_{1}[c_{1},\ldots,c_{n}]$.
Case 2.2: $b\notin[b_{i}]$ and $b\notin[b_{i}^{\prime}]$ for every $i$
Let $k_{1},\ldots,k_{l}\in A$ $(l\leq n)$ be such that for every
$i=1,\ldots,l$, $[k_{i}]R_{2}[c_{j}]$ for some $j\in\\{1,\ldots,n\\}$. There
is $a\in A$ such that $a\notin[c_{1}],\ldots,[c_{n}],\
[k_{1}],\ldots,[k_{l}]$. We add to the language $\mathcal{L}$ the constants
$d$, $d_{1},\ldots,d_{n}$. Interpreting the new constants by $b$,
$f(c_{1}),\ldots,f(c_{n})$ or by $f(a)$, $f(c_{1}),\ldots,f(c_{n})$, we obtain
two structures for the extended language which we denote by
$\mathcal{B}^{\prime}=(\mathcal{B},b,f(c_{1}),\ldots,f(c_{n}))$ and
$\mathcal{B}^{\prime\prime}=(\mathcal{B},f(a),f(c_{1}),\ldots,f(c_{n}))$
correspondingly. Let $[m_{1}]$ be the only equivalence class for which
$[b]R_{2}[m_{1}]$, and $[m_{2}]$ be the only equivalence class for which
$[f(a)]R_{2}[m_{2}]$. We consider Ehrenfeucht-Fraïssè’s game with arbitrary
finite length $s$ and the following strategy for the second player: if the
first player chooses $b$ $(f(a))$, then the second player chooses $f(a)$
$(b)$. Otherwise, if the first player chooses an element out of
$[b]\cup[f(a)]\cup[m_{1}]\cup[m_{2}]$, then the second player chooses the same
element; if the first player chooses a new element of $[b]$, then the second
player chooses a new element of $[f(a)]$, different from $f(a)$ and the
converse; if the first player chooses a new element of $[m_{1}]$, then the
second player chooses a new element of $[m_{2}]$ and the converse; if the
first player chooses already chosen in the corresponding structure element $x$
in $[b]\cup[f(a)]\cup[m_{1}]\cup[m_{2}]$, then the second player chooses the
same element which then was chosen in the other structure. Let
$e_{1},\ldots,e_{s}$ and $e_{1}^{\prime},\ldots,e_{s}^{\prime}$ be
correspondingly of $\mathcal{B}^{\prime}$ and of $\mathcal{B}^{\prime\prime}$
in the order of their choosing. Let $h=\\{\langle
e_{i},e_{i}^{\prime}\rangle:\ i=1,\ldots,s\\}\cup\\{\langle
C^{\mathcal{B}^{\prime}},C^{\mathcal{B}^{\prime\prime}}\rangle:\ C\textmd{ - a
constant of the extended language}\\}$. Let $\mathcal{B}_{1}^{\prime}$ be the
substructure of $\mathcal{B}^{\prime}$, generated by $e_{1},\ldots,e_{s}$,
$b$, $f(c_{1}),\ldots,f(c_{n})$; $\mathcal{B}_{1}^{\prime\prime}$ be the
substructure of $\mathcal{B}^{\prime\prime}$, generated by
$e_{1}^{\prime},\ldots,e_{s}^{\prime}$, $f(a)$, $f(c_{1}),\ldots,f(c_{n})$. It
can be easily verified that $h$ is an isomorphism from
$\mathcal{B}_{1}^{\prime}$ to $\mathcal{B}_{1}^{\prime\prime}$. Consequently
for every closed formula $\varphi$ we have
$\mathcal{B}^{\prime}\models\varphi\Leftrightarrow\mathcal{B}^{\prime\prime}\models\varphi$
and hence
$\mathcal{B}^{\prime}\models\varphi_{1}(d,d_{1},\ldots,d_{n})\Leftrightarrow\mathcal{B}^{\prime\prime}\models\varphi_{1}(d,d_{1},\ldots,d_{n})$;
so
$\mathcal{B}\models\varphi_{1}[b,f(c_{1}),\ldots,f(c_{n})]\Leftrightarrow\mathcal{B}\models\varphi_{1}[f(a),f(c_{1}),\ldots,f(c_{n})]$.
But we have $\mathcal{B}\models\varphi_{1}[b,f(c_{1}),\ldots,f(c_{n})]$ and
thus $\mathcal{B}\models\varphi_{1}[f(a),f(c_{1}),\ldots,f(c_{n})]$. From the
induction hypothesis, $\mathcal{A}\models\varphi_{1}[a,c_{1},\ldots,c_{n}]$,
i.e. $\mathcal{A}\models\exists x\varphi_{1}[\overline{c}]$. Consequently $f$
is an elementary embedding of $\mathcal{A}$ in $\mathcal{B}$. $\Box$

###### Corollary 2.10

The theory $SAPP$ is complete.

Proof. Let $\mathcal{F}^{2}_{\mathbb{Q}}$ be the structure for the language
$\mathcal{L}$ with universe $\\{\bm{a}\textmd{ - line in}\\\ \textmd{Euclidean
plane: at least 2 of the points of }\bm{a}\textmd{ are with rational
coordinates}\\}$. The predicate symbol $O$ is interpreted by perpendicularity.
We will prove that $\mathcal{F}^{2}_{\mathbb{Q}}\models\lambda_{5}$. Let
$x_{1,2}$, $y_{1,2}\in\mathbb{Q}$ and $a$ be the line, determined by the
points $(x_{1},y_{1})$, $(x_{2},y_{2})$.
Case 1: $a$ does not coincide with and is not parallel to the ordinate axis
Let $b$ be an arbitrary line in Euclidean plane, perpendicular to $a$, and $k$
be the slope of $b$. Let $k_{1}$ be the slope of $a$. The line $m$ with
equation $y=kx$ is perpendicular to $a$. We have
$k=-\frac{1}{k_{1}}=-\frac{x_{2}-x_{1}}{y_{2}-y_{1}}\in\mathbb{Q}$. At least
two of the points of the line $m$ are with rational coordinates - $(0,0)$ and
$(1,k)$.
Case 2: $a$ coincides with or is parallel to the ordinate axis
The abscissa axis is in $F^{2}_{\mathbb{Q}}$. Consequently
$\mathcal{F}^{2}_{\mathbb{Q}}\models\lambda_{5}$. In a similar way it can be
proved that $\mathcal{F}^{2}_{\mathbb{Q}}\models\lambda_{1n}$ for every $n\geq
1$ and $\mathcal{F}^{2}_{\mathbb{Q}}\models\lambda_{2n}$ for every $n\geq 2$.
Clearly in $\mathcal{F}^{2}_{\mathbb{Q}}$ are true also $\lambda_{3}$,
$\lambda_{4}$ and $\lambda_{6}$. Consequently
$\mathcal{F}^{2}_{\mathbb{Q}}\models SAPP$.

Let $\mathcal{A}$ and $\mathcal{B}$ be arbitrary models of $SAPP$. Since
$\mathcal{F}^{2}_{\mathbb{Q}}$ is a countable model of $SAPP$,
$\mathcal{F}^{2}_{\mathbb{Q}}$ is elementary embedded in $\mathcal{A}$ and in
$\mathcal{B}$ (Proposition 2.9). Consequently $\mathcal{F}^{2}_{\mathbb{Q}}$
is elementary equivalent to $\mathcal{A}$ and to $\mathcal{B}$ and hence
$\mathcal{A}$ and $\mathcal{B}$ are elementary equivalent. Consequently $SAPP$
is complete. $\Box$

###### Proposition 2.11

(i) $=$ is not definable by $O$ in every model of $SAPP$;
(ii) $O$ is not definable by $=$ in every model of $SAPP$;
(iii) the ternary predicate $\rho(a,b,c)$ is not definable in
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}$ by $O$ and $=$;
(iv) the binary predicate $P(a,b)$ is definable in
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}$ by $O$ and $=$;
(v) the binary predicate $C(a,b)$ is definable in
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}$ by $O$ and $=$;
(vi) $O$ is not definable in $\mathcal{F}^{2}_{\mathbb{R},PCO\rho}$ by $P$,
$C$ and $=$.

Proof.

(i) Let $\mathcal{A}\models SAPP$. Suppose for the sake of contradiction that
there is a formula $\varphi(x,y)$ in which occurs only the predicate symbol
$O$, such that $\mathcal{A}\models\forall x\forall
y(x=y\leftrightarrow\varphi(x,y))$. Let $a\in A$ and $g:\ [a]\rightarrow[a]$
be a surjection which is not an injection. We define $f:\ A\rightarrow A$ in
the following way:

$f(b)=\left\\{\begin{array}[]{lll}b&&\textmd{if }b\notin[a]\\\
g(b)&&\textmd{otherwise }\end{array}\right.$

By induction on $\psi$ it can be easily proved that for every formula $\psi$,
if in $\psi$ do not occur other predicate symbols except $O$, $\psi$ has free
variables among $x_{1},\ldots,x_{n}$ and $a_{1},\ldots,a_{n}\in A$, then
$\mathcal{A}\models\psi[\overline{a}]$ iff
$\mathcal{A}\models\psi[\overline{f(a)}]$. Consequently for all $x^{\prime}$,
$y^{\prime}\in A$, $\mathcal{A}\models\varphi[x^{\prime},y^{\prime}]$ iff
$\mathcal{A}\models\varphi[f(x^{\prime}),f(y^{\prime})]$.

Since $g$ is not an injection, there are $b_{1}$, $b_{2}\in[a]$ such that
$b_{1}\neq b_{2}$ and $g(b_{1})=g(b_{2})$. Consequently $f(b_{1})=f(b_{2})$.
Clearly we have the following equivalences: $b_{1}=b_{2}$ iff
$\mathcal{A}\models\varphi[b_{1},b_{2}]$ iff
$\mathcal{A}\models\varphi[f(b_{1}),f(b_{2})]$ iff $f(b_{1})=f(b_{2})$.
Consequently $b_{1}=b_{2}$ \- a contradiction.

(ii) Let $\mathcal{A}\models SAPP$. Suppose for the sake of contradiction that
there is a formula $\varphi(x,y)$ in which occurs only the predicate symbol
$=$, such that $\mathcal{A}\models\forall x\forall
y(O(x,y)\leftrightarrow\varphi(x,y))$.

We consider $\mathcal{F}^{2}_{\mathbb{Q}}$. Let $a$ be a line in the plane of
which at least two of the points have rational coordinates, and $[b]$ be the
only equivalence class such that $[a]R_{2}[b]$. Let $[c]\neq[a]$ and
$[c]\neq[b]$. Let $[a]=\\{a_{0},a_{1},\ldots,a_{n},\ldots\\}$ and
$[c]=\\{c_{0},c_{1},\ldots,c_{n},\ldots\\}$. We define a function $f:\
F^{2}_{\mathbb{Q}}\rightarrow F^{2}_{\mathbb{Q}}$ in the following way:

$f(x)=\left\\{\begin{array}[]{lll}x&&\textmd{if }x\notin[a]\textmd{ and
}x\notin[c]\\\ c_{i}&&\textmd{if }x=a_{i}\textmd{ for some }i\\\
a_{i}&&\textmd{if }x=c_{i}\textmd{ for some }i\end{array}\right.$

By induction on $\psi$ it can be easily verified that for every formula
$\psi$, if in $\psi$ do not occur other predicate symbols except $=$, $\psi$
has free variables among $x_{1},\ldots,x_{n}$ and $a_{1},\ldots,a_{n}\in
F^{2}_{\mathbb{Q}}$, then
$\mathcal{F}^{2}_{\mathbb{Q}}\models\psi[\overline{a}]$ iff
$\mathcal{F}^{2}_{\mathbb{Q}}\models\psi[\overline{f(a)}]$.

$\mathcal{F}^{2}_{\mathbb{Q}}$ is countable and
$\mathcal{F}^{2}_{\mathbb{Q}}\models SAPP$ (it was proved in Corollary 2.10);
$\mathcal{A}\models SAPP$; so by Proposition 2.9 we obtain that
$\mathcal{F}^{2}_{\mathbb{Q}}$ is elementary embedded in $\mathcal{A}$.
Consequently $\mathcal{F}^{2}_{\mathbb{Q}}\models\forall x\forall
y(O(x,y)\leftrightarrow\varphi(x,y))$. We have $[a]R_{2}[b]$, so $O(a,b)$. We
have also $f(a)\in[c]$ and $[c]\neq[a]$, so $\neg O(f(a),b)$, i.e. $\neg
O(f(a),f(b))$. Clearly we have the following equivalences: $O(a,b)$ iff
$\mathcal{F}^{2}_{\mathbb{Q}}\models\varphi[a,b]$ iff
$\mathcal{F}^{2}_{\mathbb{Q}}\models\varphi[f(a),f(b)]$ iff $O(f(a),f(b))$.
Consequently $O(f(a),f(b))$ \- a contradiction.

(iii) Suppose for the sake of contradiction that there is a formula
$\varphi(x,y,z)$ in $\mathcal{L}$ such that
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models\forall x\forall y\forall
z(\rho(x,y,z)\leftrightarrow\varphi(x,y,z))$. Let $a$, $b$ and $c$ be three
lines in the plane which intersect at one point. Let $a^{\prime}$ be parallel
to $a$. Clearly $\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models\varphi[a,b,c]$
and $\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\not\models\varphi[a^{\prime},b,c]$.
We define $h:\ F^{2}_{\mathbb{R}}\rightarrow F^{2}_{\mathbb{R}}$ in the
following way:

$h(x)=\left\\{\begin{array}[]{lll}x&&\textmd{if }x\neq a,a^{\prime}\\\
a^{\prime}&&\textmd{if }x=a\\\ a&&\textmd{if }x=a^{\prime}\end{array}\right.$

It can be easily verified that $h$ is a bijection and preserves the predicates
$O$ and $=$. Consequently
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models\varphi[a,b,c]$ iff
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models\varphi[h(a),h(b),h(c)]$. Thus
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models\varphi[h(a),h(b),h(c)]$, i.e.
$\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models\varphi[a^{\prime},b,c]$ \- a
contradiction.

(iv) We have $\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models\forall x\forall
y(P(x,y)\leftrightarrow(x\neq y\wedge\exists z(O(x,z)\wedge O(y,z))))$.

(v) We have $\mathcal{F}^{2}_{\mathbb{R},PCO\rho}\models\forall x\forall
y(C(x,y)\leftrightarrow\exists z(O(x,z)\wedge\neg O(y,z)))$.

(vi) The proof is similar as for (ii). $\Box$

##  3 Decidability and complexity of the first-order theory

###### Proposition 3.1

The problem if a closed formula in $\mathcal{L}$ logically follows from $SAPP$
is PSPACE-complete.

Proof. We consider $EQ^{\infty}=\\{\varphi:\ \varphi\textmd{ is a closed
formula in the language }\mathcal{L}_{1}=\langle\ ;\ ;=\rangle\textmd{ and
}\varphi\textmd{ is true in all infinite structures}\\}$ [1]. The membership
problem in $EQ^{\infty}$ is PSPACE-complete [1].

First we will prove that the problem if a closed formula in $\mathcal{L}$
logically follows from $SAPP$ is in PSPACE. It is enough to juxtapose to every
closed formula $\varphi$ in $\mathcal{L}$ a closed formula $\varphi_{1}$ in
$\mathcal{L}_{1}$ and to ensure that $\varphi_{1}$ can be obtained from
$\varphi$ algorithmically with use of memory polynomial in the size of
$\varphi$, and $SAPP\models\varphi$ iff $\varphi_{1}\in EQ^{\infty}$.

Let $\bm{\mathcal{A}^{\ast}}$ be the substructure of
$\mathcal{F}^{2}_{\mathbb{R}}$, which is obtained by eliminating of the lines
parallel to or coinciding with the abscissa axis, the lines parallel to or
coinciding with the ordinate axis and the lines with equation of the kind
$y=bx$.

###### Lemma 3.2

The structure $\mathcal{A}^{\ast}$ is a model of $SAPP$.

Proof. Let $n\geq 1$. We will prove $\mathcal{A}^{\ast}\models\lambda_{1n}$.
Let $b_{1},\ldots,b_{n}$, $c\in A^{\ast}$ and $O(c,b_{1}),\ldots,O(c,b_{n})$.
We will prove that there is $d\in A^{\ast}$ such that $d\neq
b_{1},\ldots,b_{n}$ and $O(c,d)$. We have that $b_{1},\ldots,b_{n}$ are
parallel and consequently have the same slope $m$. Let the $y$-intercepts of
$b_{1},\ldots,b_{n}$ be $q_{1},\ldots,q_{n}$. Let $q\neq 0$,
$q_{1},\ldots,q_{n}$. Let $d$ be the line with equation $y=mx+q$. Clearly $d$
has the desired properties.

Let $n\geq 2$. We will prove that $\mathcal{A}^{\ast}\models\lambda_{2n}$. Let
$b_{1},\ldots,b_{n}\in A^{\ast}$. We will prove that there is $c\in A^{\ast}$
such that $\neg O(c,b_{1}),\ldots,\neg O(c,b_{n})$. Let the slopes of
$b_{1},\ldots,b_{n}$ be correspondingly $m_{1},\ldots,m_{n}$. Let $m\neq 0$,
$-\frac{1}{m_{1}},\ldots,-\frac{1}{m_{n}}$. Let $c$ be the line with equation
$y=mx+1$. Clearly $c$ has the desired properties.

Clearly the other formulas of $SAPP$ are true in $\mathcal{A}^{\ast}$. $\Box$

###### Lemma 3.3

For every closed formula $\varphi$ in the language $\mathcal{L}$,
$SAPP\models\varphi$ iff $\mathcal{A}^{\ast}\models\varphi$.

Proof. Clearly $SAPP\models\varphi$ implies
$\mathcal{A}^{\ast}\models\varphi$. Let $\mathcal{A}^{\ast}\models\varphi$ and
$\mathcal{B}\models SAPP$. We will prove that $\mathcal{B}\models\varphi$.
$\mathcal{A}^{\ast}$ is a model of $SAPP$ and $SAPP$ is complete (Corollary
2.10); so $\mathcal{A}^{\ast}$ is elementary equivalent to every model of
$SAPP$; so $\mathcal{A}^{\ast}$ is elementary equivalent to $\mathcal{B}$.
Consequently $\mathcal{B}\models\varphi$. $\Box$

Let $\bm{\mathcal{R}}$ be the structure for $\mathcal{L}_{1}$ with universe
$\mathbb{R}\setminus\\{0\\}$.

###### Lemma 3.4

For any closed formula $\varphi$ in $\mathcal{L}_{1}$,
$\mathcal{R}\models\varphi$ iff $\varphi\in EQ^{\infty}$.

Proof. Clearly $\varphi\in EQ^{\infty}$ implies $\mathcal{R}\models\varphi$.
Let $\mathcal{R}\models\varphi$. We will prove $\varphi\in EQ^{\infty}$. Let
$\mathcal{A}$ be an infinite structure. We will prove that
$\mathcal{A}\models\varphi$. We consider the theory $T=\\{\varphi\\}$. Let $C$
be a set of constants such that the cardinality of $C$ coincides with the
cardinality of $A$. $T$ has an infinite model ($\mathcal{R}$) and can be
considered as a theory in the language $\mathcal{L}_{2}=\langle C;\ ;=\rangle$
with cardinality - the cardinality of $A$. Thus by Löwenheim-Skolem theorem we
obtain that $T$ has a model $\mathcal{B}$ for the language $\mathcal{L}_{2}$
such that the cardinality of $B$ is the maximal of $\omega$ and the
cardinality of $A$, i.e. the cardinality of $A$. We consider $\mathcal{B}$ as
a structure for $\mathcal{L}_{1}$ and since in $\varphi$ do not occur
constants, we have again $\mathcal{B}\models\varphi$. $\mathcal{A}$ and
$\mathcal{B}$ are structures for $\mathcal{L}_{1}$ and the cardinality of $A$
coincides with the cardinality of $B$; so $\mathcal{A}$ and $\mathcal{B}$ are
isomorphic; so $\mathcal{A}\models\varphi$. $\Box$

Let $a$ be a line with equation $y=bx+c$. We use the following notations:
$\bm{a^{1}}=b$, $\bm{a^{2}}=-\frac{1}{b}$, $\bm{a^{3}}=c$. It is convenient to
call $a^{1}$, $a^{2}$ and $a^{3}$ coordinates of the line $a$.

To every formula $\varphi$ in the language $\mathcal{L}$ we juxtapose a
formula $\widehat{\varphi}$ in the language $\mathcal{L}_{1}$ in the following
way:
1) $\bm{\varphi}$ \- atomic
$(\bullet)$ If $\varphi$ is $O(x_{1},x_{2})$, then $\widehat{\varphi}$ is
$x^{1}_{1}=x^{2}_{2}$.
$(\bullet)$ If $\varphi$ is $x_{1}=x_{2}$, then $\widehat{\varphi}$ is
$(x^{1}_{1}=x^{1}_{2})\wedge(x^{3}_{1}=x^{3}_{2})$.

2) $\bm{\varphi}$ is $\bm{\neg\varphi^{\prime}}$
$\widehat{\varphi}$ is $\neg\widehat{\varphi^{\prime}}$.

3) $\bm{\varphi}$ is $\bm{\varphi^{\prime}\wedge\varphi^{\prime\prime}}$
$\widehat{\varphi}$ is
$\widehat{\varphi^{\prime}}\wedge\widehat{\varphi^{\prime\prime}}$.

4) $\bm{\varphi}$ is $\bm{\exists x_{n}\varphi^{\prime}}$ and
$\bm{\varphi^{\prime}}$ has free variables $\bm{x_{1},\ldots,x_{n}}$
$\widehat{\varphi}$ is $\exists x^{1}_{n}\exists x^{2}_{n}\exists
x^{3}_{n}(\widehat{\varphi^{\prime}}\wedge\kappa_{n})$, where for every
natural number $n$, $\kappa_{n}$ is a formula with free variables $x^{1}_{1}$,
$x^{2}_{1},\ldots,x^{1}_{n}$, $x^{2}_{n}$, defined in the following way:

$\kappa_{n}:\ x^{1}_{n}\neq
x^{2}_{n}\wedge\bigwedge_{i<n}(x^{1}_{i}=x^{1}_{n}\leftrightarrow
x^{2}_{i}=x^{2}_{n})\wedge\bigwedge_{i<n}(x^{1}_{i}=x^{2}_{n}\leftrightarrow
x^{2}_{i}=x^{1}_{n})$

###### Definition 3.5

Let $n$ be a natural number, $a^{1}_{1}$, $a^{2}_{1}$,
$a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$,
$a^{3}_{n}\in\mathbb{R}\setminus\\{0\\}$ and for every $i\in\\{1,\ldots,n\\}$,
$\mathcal{R}\models\kappa_{i}[a^{1}_{1},a^{2}_{1},\ldots,a^{1}_{i},a^{2}_{i}]$.
We say that $b^{1}_{1}$, $b^{2}_{1}$, $b^{3}_{1},\ldots,b^{1}_{n}$,
$b^{2}_{n}$, $b^{3}_{n}$ are corresponding to $a^{1}_{1}$, $a^{2}_{1}$,
$a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$, $a^{3}_{n}$ if for every
$i\in\\{1,\ldots,n\\}$,

1) $b^{1}_{i}$, $b^{2}_{i}$, $b^{3}_{i}\in\mathbb{R}\setminus\\{0\\}$

2) if
$a^{1}_{i}\notin\\{a^{1}_{1},a^{2}_{1},\ldots,a^{1}_{i-1},a^{2}_{i-1}\\}$,
then $b^{1}_{i}\notin\\{b^{1}_{1},b^{2}_{1},\ldots,b^{1}_{i-1},b^{2}_{i-1}\\}$

3) if $a^{1}_{i}=a^{1}_{k}$ for some $k\in\\{1,\ldots,i-1\\}$, then
$b^{1}_{i}=b^{1}_{k}$

4) if $a^{1}_{i}=a^{2}_{k}$ for some $k\in\\{1,\ldots,i-1\\}$, then
$b^{1}_{i}=b^{2}_{k}$

5) $b^{2}_{i}=-\frac{1}{b^{1}_{i}}$

6) $b^{3}_{i}=a^{3}_{i}$

By induction on $j$ it can be easily proved the following

###### Lemma 3.6

Let $b^{1}_{1}$, $b^{2}_{1}$, $b^{3}_{1},\ldots,b^{1}_{n}$, $b^{2}_{n}$,
$b^{3}_{n}$ be corresponding to $a^{1}_{1}$, $a^{2}_{1}$,
$a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$, $a^{3}_{n}$. Then for any $j$ and
$i$, if $1\leq i<j\leq n$, then
1) $b^{1}_{j}=b^{1}_{i}$ implies $a^{1}_{j}=a^{1}_{i}$;
2) $b^{1}_{j}=b^{2}_{i}$ implies $a^{1}_{j}=a^{2}_{i}$.

###### Lemma 3.7

Let $b^{1}_{1}$, $b^{2}_{1}$, $b^{3}_{1},\ldots,b^{1}_{n}$, $b^{2}_{n}$,
$b^{3}_{n}$ be corresponding to $a^{1}_{1}$, $a^{2}_{1}$,
$a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$, $a^{3}_{n}$ and $\varphi$ be
$O(x,y)$ or $x=y$. Then for any $i$, $j\in\\{1,\ldots,n\\}$,
$\mathcal{R}\models\widehat{\varphi}[a^{1}_{i},a^{2}_{i},a^{3}_{i},a^{1}_{j},a^{2}_{j},a^{3}_{j}]$
iff
$\mathcal{R}\models\widehat{\varphi}[b^{1}_{i},b^{2}_{i},b^{3}_{i},b^{1}_{j},b^{2}_{j},b^{3}_{j}]$.

Proof. Let $i$, $j\in\\{1,\ldots,n\\}$.
Case 1: $i=j$
The proof is trivial.
Case 2: $i\neq j$
Without loss of generality $i<j$.
Case 2.1: $\varphi$ is $O(x,y)$
$\widehat{\varphi}$ is $x^{1}=y^{2}$. We must prove the following two
equivalences:
1) $a^{1}_{i}=a^{2}_{j}$ iff $b^{1}_{i}=b^{2}_{j}$
2) $a^{1}_{j}=a^{2}_{i}$ iff $b^{1}_{j}=b^{2}_{i}$

Since
$\mathcal{R}\models\kappa_{j}[a^{1}_{1},a^{2}_{1},\ldots,a^{1}_{j},a^{2}_{j}]$,
$a^{1}_{i}=a^{2}_{j}$ iff $a^{2}_{i}=a^{1}_{j}$. Since $b^{1}_{j}\cdot
b^{2}_{j}=-1$ and $b^{1}_{i}\cdot b^{2}_{i}=-1$, $b^{1}_{i}=b^{2}_{j}$ iff
$b^{1}_{j}=b^{2}_{i}$. Consequently it suffices to prove the second
equivalence. By condition 4) of Definition 3.5, $a^{1}_{j}=a^{2}_{i}$ implies
$b^{1}_{j}=b^{2}_{i}$. By Lemma 3.6, $b^{1}_{j}=b^{2}_{i}$ implies
$a^{1}_{j}=a^{2}_{i}$.
Case 2.2: $\varphi$ is $x=y$
$\widehat{\varphi}$ is $(x^{1}=y^{1})\wedge(x^{3}=y^{3})$.
We must prove the following equivalence:
$(a^{1}_{i}=a^{1}_{j}\textmd{ and }a^{3}_{i}=a^{3}_{j})$ iff
$(b^{1}_{i}=b^{1}_{j}\textmd{ and }b^{3}_{i}=b^{3}_{j})$
By conditions 3) and 6) of Definition 3.5 we get that
$(a^{1}_{i}=a^{1}_{j}\textmd{ and }a^{3}_{i}=a^{3}_{j})$ implies
$(b^{1}_{j}=b^{1}_{i}\textmd{ and }b^{3}_{i}=b^{3}_{j})$.
By Lemma 3.6 and condition 6) of Definition 3.5 we get that
$(b^{1}_{j}=b^{1}_{i}\textmd{ and }b^{3}_{i}=b^{3}_{j})$ implies
$(a^{1}_{j}=a^{1}_{i}\textmd{ and }a^{3}_{i}=a^{3}_{j})$. $\Box$

###### Lemma 3.8

Let $b^{1}_{1}$, $b^{2}_{1}$, $b^{3}_{1},\ldots,b^{1}_{n}$, $b^{2}_{n}$,
$b^{3}_{n}$ be corresponding to $a^{1}_{1}$, $a^{2}_{1}$,
$a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$, $a^{3}_{n}$ and $1\leq j_{1}\leq
j_{2}\leq\ldots\leq j_{m}\leq n$. Then $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$ are
corresponding to $a^{1}_{j_{1}}$, $a^{2}_{j_{1}}$,
$a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$, $a^{3}_{j_{m}}$.

Proof. Since $b^{1}_{1}$, $b^{2}_{1}$, $b^{3}_{1},\ldots,b^{1}_{n}$,
$b^{2}_{n}$, $b^{3}_{n}$ are corresponding to $a^{1}_{1}$, $a^{2}_{1}$,
$a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$, $a^{3}_{n}$, for every
$i\in\\{1,\ldots,m\\}$,
1)
$\mathcal{R}\models\kappa_{i}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{i}},a^{2}_{j_{i}}]$;

2) $b^{1}_{j_{i}}$, $b^{2}_{j_{i}}$,
$b^{3}_{j_{i}}\in\mathbb{R}\setminus\\{0\\}$;

3) $b^{2}_{j_{i}}=-\frac{1}{b^{1}_{j_{i}}}$;

4) $b^{3}_{j_{i}}=a^{3}_{j_{i}}$.

Let $i\in\\{1,\ldots,m\\}$. We consider
Case 1:
$a^{1}_{j_{i}}\notin\\{a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{i-1}},a^{2}_{j_{i-1}}\\}$
We will prove that
$b^{1}_{j_{i}}\notin\\{b^{1}_{j_{1}},b^{2}_{j_{1}},\ldots,b^{1}_{j_{i-1}},b^{2}_{j_{i-1}}\\}$.
Suppose for the sake of contradiction the converse. By Lemma 3.6,
$a^{1}_{j_{i}}\in\\{a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{i-1}},a^{2}_{j_{i-1}}\\}$
which is the desired contradiction.
Case 2:
$a^{1}_{j_{i}}\in\\{a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{i-1}},a^{2}_{j_{i-1}}\\}$
Clearly:
1) if $a^{1}_{j_{i}}=a^{1}_{j_{k}}$ for some $k\in\\{1,\ldots,i-1\\}$, then
$b^{1}_{j_{i}}=b^{1}_{j_{k}}$;
2) if $a^{1}_{j_{i}}=a^{2}_{j_{k}}$ for some $k\in\\{1,\ldots,i-1\\}$, then
$b^{1}_{j_{i}}=b^{2}_{j_{k}}$.
$\Box$

###### Lemma 3.9

Let $\varphi$ be a formula for $\mathcal{L}$ with free variables
$x_{1},\ldots,x_{m}$. Let $b^{1}_{1}$, $b^{2}_{1}$,
$b^{3}_{1},\ldots,b^{1}_{n}$, $b^{2}_{n}$, $b^{3}_{n}$ be corresponding to
$a^{1}_{1}$, $a^{2}_{1}$, $a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$,
$a^{3}_{n}$. Then for any $j_{1},\ldots,j_{m}\in\\{1,\ldots,n\\}$,
$\mathcal{R}\models\widehat{\varphi}[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}}]$
iff
$\mathcal{R}\models\widehat{\varphi}[b^{1}_{j_{1}},b^{2}_{j_{1}},b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}},b^{3}_{j_{m}}]$.

Proof. Induction on $\varphi$. For the base of induction we use Lemma 3.7. If
$\varphi$ is $\neg\varphi^{\prime}$ or
$\varphi^{\prime}\wedge\varphi^{\prime\prime}$, the proof is trivial. Let
$\varphi$ be $\exists x_{m+1}\varphi^{\prime}$ and $\varphi^{\prime}$ has free
variables $x_{1},\ldots,x_{m+1}$. Let $b^{1}_{1}$, $b^{2}_{1}$,
$b^{3}_{1},\ldots,b^{1}_{n}$, $b^{2}_{n}$, $b^{3}_{n}$ be corresponding to
$a^{1}_{1}$, $a^{2}_{1}$, $a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$,
$a^{3}_{n}$. Let $j_{1},\ldots,j_{m}\in\\{1,\ldots,n\\}$. Without loss of
generality $j_{1}\leq\ldots\leq j_{m}$. We will prove that
$\mathcal{R}\models\exists x^{1}_{m+1}\exists x^{2}_{m+1}\exists
x^{3}_{m+1}(\widehat{\varphi^{\prime}}\wedge\kappa_{m+1})[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}}]$
iff
$\mathcal{R}\models\exists x^{1}_{m+1}\exists x^{2}_{m+1}\exists
x^{3}_{m+1}(\widehat{\varphi^{\prime}}\wedge\kappa_{m+1})[b^{1}_{j_{1}},b^{2}_{j_{1}},b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}},b^{3}_{j_{m}}]$.

$\bm{\Rightarrow)}$ There are $c^{1}$, $c^{2}$,
$c^{3}\in\mathbb{R}\setminus\\{0\\}$ such that
$\mathcal{R}\models(\widehat{\varphi^{\prime}}\wedge\kappa_{m+1})[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}},c^{1},c^{2},c^{3}]$.

  * •

If
$c^{1}\notin\\{a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}}\\}$,
we choose a real number $d^{1}$, different from $0$, such that
$d^{1}\notin\\{b^{1}_{j_{1}},b^{2}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}}\\}$.

  * •

If $c^{1}=a^{1}_{j_{k}}$ for some $k\in\\{1,\ldots,m\\}$, we denote
$d^{1}=b^{1}_{j_{k}}$.

  * •

If $c^{1}=a^{2}_{j_{k}}$ for some $k\in\\{1,\ldots,m\\}$, we denote
$d^{1}=b^{2}_{j_{k}}$.

We denote $d^{2}=-\frac{1}{d^{1}}$, $d^{3}=c^{3}$. Using Lemma 3.8, we get
that $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$, $b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$,
$b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$, $d^{1}$, $d^{2}$, $d^{3}$ are corresponding
to $a^{1}_{j_{1}}$, $a^{2}_{j_{1}}$, $a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$,
$a^{2}_{j_{m}}$, $a^{3}_{j_{m}}$, $c^{1}$, $c^{2}$, $c^{3}$. By the induction
hypothesis,
$\mathcal{R}\models\widehat{\varphi^{\prime}}[b^{1}_{j_{1}},b^{2}_{j_{1}},b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}},b^{3}_{j_{m}},\\\
d^{1},d^{2},d^{3}]$. Since for every $k\in\\{1,\ldots,m\\}$,
$b^{1}_{j_{k}}\cdot b^{2}_{j_{k}}=-1$ and $d^{1}\cdot d^{2}=-1$,
$\mathcal{R}\models\kappa_{m+1}[b^{1}_{j_{1}},b^{2}_{j_{1}},b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}},b^{3}_{j_{m}},d^{1},d^{2},d^{3}]$.

$\bm{\Leftarrow)}$ There are $d^{1}$, $d^{2}$,
$d^{3}\in\mathbb{R}\setminus\\{0\\}$ such that
$\mathcal{R}\models(\widehat{\varphi^{\prime}}\wedge\kappa_{m+1})[b^{1}_{j_{1}},b^{2}_{j_{1}},b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}},\\\
b^{2}_{j_{m}},b^{3}_{j_{m}},d^{1},d^{2},d^{3}]$. By Lemma 3.8,
$b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$, $b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$,
$b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$ are corresponding to $a^{1}_{j_{1}}$,
$a^{2}_{j_{1}}$, $a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$,
$a^{3}_{j_{m}}$ and hence
$\mathcal{R}\models\kappa_{k}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{k}},a^{2}_{j_{k}}]$
for every $k\in\\{1,\ldots,m\\}$.
Case 1:
$d^{1}\notin\\{b^{1}_{j_{1}},b^{2}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}}\\}$
Let $e^{1}$ be a real number, different from zero, such that
$e^{1}\notin\\{b^{1}_{j_{1}},b^{2}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}}\\}$.
We denote $e^{2}=-\frac{1}{e^{1}}$, $e^{3}=d^{3}$. It can be easily proved
that $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$, $b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$,
$b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$, $e^{1}$, $e^{2}$, $e^{3}$ are corresponding
to $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$, $b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$,
$b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$, $d^{1}$, $d^{2}$, $d^{3}$. By the induction
hypothesis,
$\mathcal{R}\models\widehat{\varphi^{\prime}}[b^{1}_{j_{1}},b^{2}_{j_{1}},b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}},b^{3}_{j_{m}},e^{1},e^{2},e^{3}]$.

Let $c^{1}$ and $c^{2}$ be different real numbers such that $c^{1}$,
$c^{2}\notin\\{0,a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{m}},\\\
a^{2}_{j_{m}}\\}$. We will prove that $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$,
$e^{1}$, $e^{2}$, $e^{3}$ are corresponding to $a^{1}_{j_{1}}$,
$a^{2}_{j_{1}}$, $a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$,
$a^{3}_{j_{m}}$, $c^{1}$, $c^{2}$, $e^{3}$. Obviously
$\mathcal{R}\models\kappa_{m+1}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},c^{1},c^{2}]$.
Since $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$, $b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$,
$b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$ are corresponding to $a^{1}_{j_{1}}$,
$a^{2}_{j_{1}}$, $a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$,
$a^{3}_{j_{m}}$, we have that conditions $2)$, $3)$ and $4)$ of Definition 3.5
are fulfilled for every step from $1$ to $m$. Obviously they are fulfilled
also for step $m+1$. Clearly conditions $5)$ and $6)$ of Definition 3.5 are
fulfilled at every step. Thus $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$,
$e^{1}$, $e^{2}$, $e^{3}$ are corresponding to $a^{1}_{j_{1}}$,
$a^{2}_{j_{1}}$, $a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$,
$a^{3}_{j_{m}}$, $c^{1}$, $c^{2}$, $e^{3}$. By the induction hypothesis,
$\mathcal{R}\models\widehat{\varphi^{\prime}}[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}},c^{1},c^{2},e^{3}]$
iff
$\mathcal{R}\models\widehat{\varphi^{\prime}}[b^{1}_{j_{1}},b^{2}_{j_{1}},b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}},b^{3}_{j_{m}},e^{1},e^{2},e^{3}]$.
Consequently
$\mathcal{R}\models\widehat{\varphi^{\prime}}[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,\\\
a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}},c^{1},c^{2},e^{3}]$. We have also
that
$\mathcal{R}\models\kappa_{m+1}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},c^{1},c^{2}]$.
Thus
$\mathcal{R}\models(\widehat{\varphi^{\prime}}\wedge\kappa_{m+1})[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}},c^{1},c^{2},e^{3}]$,
i.e. $\mathcal{R}\models\\\ \exists x^{1}_{m+1}\exists x^{2}_{m+1}\exists
x^{3}_{m+1}(\widehat{\varphi^{\prime}}\wedge\kappa_{m+1})[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}}]$.
Case 2:
$d^{1}\in\\{b^{1}_{j_{1}},b^{2}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}}\\}$
We proved that $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$ are
corresponding to $a^{1}_{j_{1}}$, $a^{2}_{j_{1}}$,
$a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$, $a^{3}_{j_{m}}$ and
hence $b^{1}_{j_{k}}\cdot b^{2}_{j_{k}}=-1$ for every $k\in\\{1,\ldots,m\\}$.
We have also that $d^{1}=b^{1}_{j_{k}}$ or $d^{1}=b^{2}_{j_{k}}$ for some
$k\in\\{1,\ldots,m\\}$ and
$\mathcal{R}\models\kappa_{m+1}[b^{1}_{j_{1}},b^{2}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}},d^{1},d^{2}]$.
Consequently $d^{1}\cdot d^{2}=-1$.
Case 2.1: $d^{1}=b^{1}_{j_{k}}$ for some $k\in\\{1,\ldots,m\\}$
We denote $c^{1}=a^{1}_{j_{k}}$, $c^{2}=a^{2}_{j_{k}}$. We will prove that
$b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$, $b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$,
$b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$, $d^{1}$, $d^{2}$, $d^{3}$ are corresponding
to $a^{1}_{j_{1}}$, $a^{2}_{j_{1}}$, $a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$,
$a^{2}_{j_{m}}$, $a^{3}_{j_{m}}$, $c^{1}$, $c^{2}$, $d^{3}$. We proved that
$\mathcal{R}\models\kappa_{l}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{l}},a^{2}_{j_{l}}]$
for every $l\in\\{1,\ldots,m\\}$. We will prove that
$\mathcal{R}\models\kappa_{m+1}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},c^{1},c^{2}]$.
Since
$\mathcal{R}\models\kappa_{k}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{k}},a^{2}_{j_{k}}]$,
$a^{1}_{j_{k}}\neq a^{2}_{j_{k}}$, i.e. $c^{1}\neq c^{2}$. It remains to prove
that for every $l\in\\{1,\ldots,m\\}$, ($a^{1}_{j_{l}}=a^{1}_{j_{k}}$ iff
$a^{2}_{j_{l}}=a^{2}_{j_{k}}$) and ($a^{1}_{j_{l}}=a^{2}_{j_{k}}$ iff
$a^{2}_{j_{l}}=a^{1}_{j_{k}}$). If $l=k$, then these equivalences are obvious.
If $l<k$, then they follow from
$\mathcal{R}\models\kappa_{k}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{k}},a^{2}_{j_{k}}]$;
if $l>k$, then they follow from
$\mathcal{R}\models\kappa_{l}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{l}},a^{2}_{j_{l}}]$.
Thus
$\mathcal{R}\models\kappa_{m+1}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},c^{1},c^{2}]$.
Conditions 2), 3) and 4) of Definition 3.5 are fulfilled for every step from
$1$ to $m$ because $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$ are
corresponding to $a^{1}_{j_{1}}$, $a^{2}_{j_{1}}$,
$a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$, $a^{3}_{j_{m}}$.
Obviously at step $m+1$ condition 2) of Definition 3.5 is fulfilled.

We will prove that condition 3) of Definition 3.5 is fulfilled at step $m+1$.
Let $c^{1}=a^{1}_{j_{l}}$ for some $l\in\\{1,\ldots,m\\}$. We will prove that
$d^{1}=b^{1}_{j_{l}}$. Using that $c^{1}=a^{1}_{j_{k}}=a^{1}_{j_{l}}$ and the
fact that $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$ are
corresponding to $a^{1}_{j_{1}}$, $a^{2}_{j_{1}}$,
$a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$, $a^{3}_{j_{m}}$, we
obtain that $b^{1}_{j_{k}}=b^{1}_{j_{l}}$. Consequently $d^{1}=b^{1}_{j_{l}}$.

We will prove that condition 4) of Definition 3.5 is fulfilled at step $m+1$.
Let $c^{1}=a^{2}_{j_{l}}$ for some $l\in\\{1,\ldots,m\\}$.
Case a: $l>k$
Since
$\mathcal{R}\models\kappa_{l}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{l}},a^{2}_{j_{l}}]$,
$a^{1}_{j_{k}}=a^{2}_{j_{l}}$ iff $a^{2}_{j_{k}}=a^{1}_{j_{l}}$ and hence
$a^{1}_{j_{l}}=a^{2}_{j_{k}}$. We have that $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$ are
corresponding to $a^{1}_{j_{1}}$, $a^{2}_{j_{1}}$,
$a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$, $a^{3}_{j_{m}}$ and by
condition 4) of Definition 3.5 we get $b^{1}_{j_{l}}=b^{2}_{j_{k}}$.
Consequently $b^{1}_{j_{k}}=b^{2}_{j_{l}}$ and hence $d^{1}=b^{2}_{j_{l}}$.
Case b: $k\geq l$
We have proved that $a^{1}_{j_{k}}\neq a^{2}_{j_{k}}$, so $k\neq l$. Thus
$k>l$. We have that $a^{1}_{j_{k}}=a^{2}_{j_{l}}$ and $b^{1}_{j_{1}}$,
$b^{2}_{j_{1}}$, $b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$,
$b^{3}_{j_{m}}$ are corresponding to $a^{1}_{j_{1}}$, $a^{2}_{j_{1}}$,
$a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$, $a^{3}_{j_{m}}$.
Consequently $b^{1}_{j_{k}}=b^{2}_{j_{l}}$ and hence $d^{1}=b^{2}_{j_{l}}$.

Consequently condition 4) of Definition 3.5 is fulfilled at step $m+1$.
Clearly for every step, conditions 5) and 6) of Definition 3.5 are fulfilled.
Thus we proved that $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$,
$d^{1}$, $d^{2}$, $d^{3}$ are corresponding to $a^{1}_{j_{1}}$,
$a^{2}_{j_{1}}$, $a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$,
$a^{3}_{j_{m}}$, $c^{1}$, $c^{2}$, $d^{3}$. By the induction hypothesis,
$\mathcal{R}\models\widehat{\varphi^{\prime}}[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}},c^{1},c^{2},d^{3}]$
iff
$\mathcal{R}\models\widehat{\varphi^{\prime}}[b^{1}_{j_{1}},b^{2}_{j_{1}},b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}},b^{2}_{j_{m}},b^{3}_{j_{m}},\\\
d^{1},d^{2},d^{3}]$. Consequently
$\mathcal{R}\models\widehat{\varphi^{\prime}}[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}},c^{1},c^{2},d^{3}]$.
We have also that
$\mathcal{R}\models\kappa_{m+1}[a^{1}_{j_{1}},a^{2}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},c^{1},c^{2}]$.
Consequently $\mathcal{R}\models\exists x^{1}_{m+1}\exists x^{2}_{m+1}\exists
x^{3}_{m+1}(\widehat{\varphi^{\prime}}\wedge\kappa_{m+1})[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},a^{2}_{j_{m}},a^{3}_{j_{m}}]$.
Case 2.2: $d^{1}=b^{2}_{j_{k}}$ for some $k\in\\{1,\ldots,m\\}$
We denote $c^{1}=a^{2}_{j_{k}}$, $c^{2}=a^{1}_{j_{k}}$. In a similar way as in
Case 2.1 we prove that $b^{1}_{j_{1}}$, $b^{2}_{j_{1}}$,
$b^{3}_{j_{1}},\ldots,b^{1}_{j_{m}}$, $b^{2}_{j_{m}}$, $b^{3}_{j_{m}}$,
$d^{1}$, $d^{2}$, $d^{3}$ are corresponding to $a^{1}_{j_{1}}$,
$a^{2}_{j_{1}}$, $a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}}$, $a^{2}_{j_{m}}$,
$a^{3}_{j_{m}}$, $c^{1}$, $c^{2}$, $d^{3}$ and $\mathcal{R}\models\exists
x^{1}_{m+1}\exists x^{2}_{m+1}\exists
x^{3}_{m+1}(\widehat{\varphi^{\prime}}\wedge\kappa_{m+1})[a^{1}_{j_{1}},a^{2}_{j_{1}},a^{3}_{j_{1}},\ldots,a^{1}_{j_{m}},\\\
a^{2}_{j_{m}},a^{3}_{j_{m}}]$. $\Box$

###### Lemma 3.10

Let $\varphi$ be a formula in $\mathcal{L}$ with free variables
$x_{1},\ldots,x_{n}$ and $a_{1},\ldots,a_{n}\\\ \in A^{\ast}$. Then
$\mathcal{A}^{\ast}\models\varphi[a_{1},\ldots,a_{n}]$ iff
$\mathcal{R}\models\widehat{\varphi}[a^{1}_{1},a^{2}_{1},a^{3}_{1},\ldots,a^{1}_{n},a^{2}_{n},a^{3}_{n}]$.

Proof. Induction on $\varphi$. The base of induction, the cases when $\varphi$
is $\neg\varphi^{\prime}$ or $\varphi$ is
$\varphi^{\prime}\wedge\varphi^{\prime\prime}$ are trivial. Let $\varphi$ be
$\exists x_{n+1}\varphi^{\prime}$ and $\varphi^{\prime}$ has free variables
$x_{1},\ldots,x_{n+1}$. Let $a_{1},\ldots,a_{n}\in A^{\ast}$. We will prove
that $\mathcal{A}^{\ast}\models\exists
x_{n+1}\varphi^{\prime}[a_{1},\ldots,a_{n}]$ iff $\mathcal{R}\models\exists
x^{1}_{n+1}\exists x^{2}_{n+1}\exists
x^{3}_{n+1}(\widehat{\varphi^{\prime}}\wedge\kappa_{n+1})[a^{1}_{1},a^{2}_{1},a^{3}_{1},\ldots,a^{1}_{n},a^{2}_{n},a^{3}_{n}]$.
$\bm{\Rightarrow)}$ The proof is trivial.
$\bm{\Leftarrow)}$ There are $a^{1}_{n+1}$, $a^{2}_{n+1}$,
$a^{3}_{n+1}\in\mathbb{R}\setminus\\{0\\}$ such that
$\mathcal{R}\models(\widehat{\varphi^{\prime}}\wedge\kappa_{n+1})[a^{1}_{1},a^{2}_{1},a^{3}_{1},\ldots,\\\
a^{1}_{n},a^{2}_{n},a^{3}_{n},a^{1}_{n+1},a^{2}_{n+1},a^{3}_{n+1}]$. If
$a^{1}_{n+1}\notin\\{a^{1}_{1},a^{2}_{1},\ldots,a^{1}_{n},a^{2}_{n}\\}$, let
$b^{1}_{n+1}$ be a real number, different from $0$, not belonging to
$\\{a^{1}_{1},a^{2}_{1},\ldots,a^{1}_{n},a^{2}_{n}\\}$; if
$a^{1}_{n+1}=a^{1}_{k}$ for some $k\in\\{1,\ldots,n\\}$, we denote
$b^{1}_{n+1}=a^{1}_{k}$; if $a^{1}_{n+1}=a^{2}_{k}$ for some
$k\in\\{1,\ldots,n\\}$, we denote $b^{1}_{n+1}=a^{2}_{k}$. We denote
$b^{2}_{n+1}=-\frac{1}{b^{1}_{n+1}}$. Clearly the definition is correct. It
can be easily verified that $a^{1}_{1}$, $a^{2}_{1}$,
$a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$, $a^{3}_{n}$, $b^{1}_{n+1}$,
$b^{2}_{n+1}$, $a^{3}_{n+1}$ are corresponding to $a^{1}_{1}$, $a^{2}_{1}$,
$a^{3}_{1},\ldots,a^{1}_{n}$, $a^{2}_{n}$, $a^{3}_{n}$, $a^{1}_{n+1}$,
$a^{2}_{n+1}$, $a^{3}_{n+1}$. By Lemma 3.9,
$\mathcal{R}\models\widehat{\varphi^{\prime}}[a^{1}_{1},a^{2}_{1},a^{3}_{1},\ldots,a^{1}_{n},a^{2}_{n},a^{3}_{n},a^{1}_{n+1},a^{2}_{n+1},a^{3}_{n+1}]$
iff
$\mathcal{R}\models\widehat{\varphi^{\prime}}[a^{1}_{1},a^{2}_{1},a^{3}_{1},\ldots,a^{1}_{n},a^{2}_{n},a^{3}_{n},b^{1}_{n+1},b^{2}_{n+1},a^{3}_{n+1}]$.
Consequently
$\mathcal{R}\models\widehat{\varphi^{\prime}}[a^{1}_{1},a^{2}_{1},a^{3}_{1},\\\
\ldots,a^{1}_{n},a^{2}_{n},a^{3}_{n},b^{1}_{n+1},b^{2}_{n+1},a^{3}_{n+1}]$.
Let $a_{n+1}$ be the line with equation $y=b^{1}_{n+1}x+a^{3}_{n+1}$.
Obviously $a_{n+1}\in A^{\ast}$. The coordinates of $a_{n+1}$ are
$b^{1}_{n+1}$, $b^{2}_{n+1}$, $a^{3}_{n+1}$. By the induction hypothesis,
$\mathcal{A}^{\ast}\models\varphi^{\prime}[a_{1},\ldots,a_{n},a_{n+1}]$ iff
$\mathcal{R}\models\widehat{\varphi^{\prime}}[a^{1}_{1},a^{2}_{1},a^{3}_{1},\ldots,a^{1}_{n},\\\
a^{2}_{n},a^{3}_{n},b^{1}_{n+1},b^{2}_{n+1},a^{3}_{n+1}]$. Consequently
$\mathcal{A}^{\ast}\models\varphi^{\prime}[a_{1},\ldots,a_{n},a_{n+1}]$ and
hence $\mathcal{A}^{\ast}\models\exists
x_{n+1}\varphi^{\prime}[a_{1},\ldots,a_{n}]$. $\Box$

It can be easily verified that $\widehat{\varphi}$ can be obtained
algorithmically from $\varphi$ by using of memory, polynomial in the size of
$\varphi$.

By Lemma 3.3, Lemma 3.10 and Lemma 3.4, $SAPP\models\varphi$ iff
$\mathcal{A}^{\ast}\models\varphi$ iff $\mathcal{R}\models\widehat{\varphi}$
iff $\widehat{\varphi}\in EQ^{\infty}$.

Now we will prove that the problem if a closed formula in $\mathcal{L}$
logically follows from $SAPP$ is PSPACE-hard. We will prove that for every
closed formula in $\mathcal{L}_{1}=\langle\ ;\ ;=\rangle$ $\varphi_{1}$,
$\varphi_{1}\in EQ^{\infty}$ iff $SAPP\models\varphi_{1}$. The formula
$\varphi_{1}$ is a formula in $\mathcal{L}$ too. By Lemma 3.3,
$SAPP\models\varphi_{1}$ iff $\mathcal{A}^{\ast}\models\varphi_{1}$. Similarly
of Lemma 3.4 we prove that $\mathcal{A}^{\ast}\models\varphi_{1}$ iff
$\varphi_{1}\in EQ^{\infty}$. Thus we proved that for every closed formula in
$\mathcal{L}_{1}$ $\varphi_{1}$, $\varphi_{1}\in EQ^{\infty}$ iff
$SAPP\models\varphi_{1}$. We have also that the membership problem in
$EQ^{\infty}$ is PSPACE-hard. Consequently the problem if a closed formula in
$\mathcal{L}$ logically follows from $SAPP$ is PSPACE-hard. $\Box$

##  4 Some additional results

###### Proposition 4.1

The theory $SAPP$ is not finitely axiomatizable.

Proof. For the sake of contradiction suppose that $SAPP$ is axiomatized by a
finite set of formulas $\Gamma$. Let the maximal quantifier rank of a formula
of $\Gamma$ be $n$. We denote $k=n+1$. Obviously $k>0$. Let $S$ be the set of
the lines with equation of the kind $y=ax+b$, where
$a\in\\{1,\ldots,k,-1,-\frac{1}{2},\ldots,-\frac{1}{k}\\}$,
$b\in\\{1,\ldots,k\\}$. Obviously $S\subseteq F^{2}_{\mathbb{Q}}$. Let
$\mathcal{S}$ be the substructure of $\mathcal{F}^{2}_{\mathbb{Q}}$ with
universe $S$. We consider the structures $\mathcal{F}^{2}_{\mathbb{Q}}$ and
$\mathcal{S}$ and Ehrenfeucht-Fraïssè’s game with length $k$. It can be easily
found a winning strategy for the second player. Consequently
$\mathcal{F}^{2}_{\mathbb{Q}}$ and $\mathcal{S}$ are $k$ elementary
equivalent. Consequently for every formula $\varphi$ of $\Gamma$,
$\mathcal{F}^{2}_{\mathbb{Q}}\models\varphi$ iff $\mathcal{S}\models\varphi$.
Consequently $\mathcal{S}\models\Gamma$ and hence $\mathcal{S}\models SAPP$
but $\mathcal{S}\not\models\lambda_{1k}$ \- a contradiction. $\Box$

It can be easily proved the following proposition:

###### Proposition 4.2

The theory $SAPP$ is $\omega$-categorical.

###### Proposition 4.3

The theory $SAPP$ is not $\alpha$-categorical for every uncountable
cardinality $\alpha$.

Proof. We denote by $\mathbb{Z}^{\ast}$ the set of all non-zero integers. Let
$\alpha$ be an arbitrary uncountable cardinal. Let
$A=\alpha\times\mathbb{Z}^{\ast}$; $B=\mathbb{Z}^{\ast}\times\alpha$. We
consider the structure $\mathcal{A}=(A,O,=)$, where
$O((x_{1},x_{2}),(y_{1},y_{2}))\stackrel{{\scriptstyle
def}}{{\Longleftrightarrow}}x_{1}=y_{1}$ and $x_{2}\cdot y_{2}<0$. We consider
also the structure $\mathcal{B}=(B,O,=)$, where
$O((x_{1},x_{2}),(y_{1},y_{2}))\stackrel{{\scriptstyle
def}}{{\Longleftrightarrow}}\frac{x_{1}}{y_{1}}=-1$.

Clearly $A$ and $B$ have cardinality $\alpha$.

It can be easily proved the following lemma:

###### Lemma 4.4

(i) Every equivalence class of $A$ is countable and has the form
$\\{(\gamma,1),(\gamma,2),\ldots,(\gamma,n),\ldots\\}$ or
$\\{(\gamma,-1),(\gamma,-2),\ldots,(\gamma,-n),\ldots\\}$, where
$\gamma<\alpha$;
(ii) Every equivalence class of $B$ is uncountable and has the form
$\\{(s,\beta):\ \beta<\alpha\\}$, where $s\in\mathbb{Z}^{\ast}$.

Using Lemma 4.4, it can be easily verified that $\mathcal{A}\models SAPP$ and
$\mathcal{B}\models SAPP$.

Suppose for the sake of contradiction that there is an isomorphism $f:\
\mathcal{A}\rightarrow\mathcal{B}$. We will prove the following lemma:

###### Lemma 4.5

For any $x$, $y\in A$, $[x]=[y]$ iff $[f(x)]=[f(y)]$.

Proof. $\bm{\Rightarrow)}$ Obviously $\neg O(f(x),f(y))$. There is $z\in B$
such that $O(f(y),z)$. Since $f$ is an isomorphism, $z=f(z_{1})$ for some
$z_{1}\in A$. Obviously $O(y,z_{1})$ and hence $O(x,z_{1})$; so $O(f(x),z)$;
so $[z]R_{2}[f(x)]$ but we also have $[z]R_{2}[f(y)]$, so $[f(x)]=[f(y)]$.
$\bm{\Leftarrow)}$ The proof is symmetric. $\Box$

Let $\gamma<\alpha$. We have $(\gamma,1)\in A$. By Lemma 4.4, $[(\gamma,1)]$
is countable and has the form
$\\{(\gamma,1),(\gamma,2),\ldots,(\gamma,n),\ldots\\}$. We have
$f((\gamma,1))=(s,\delta)$, where $s\in\mathbb{Z}^{\ast}$, $\delta<\alpha$. By
Lemma 4.4, $[(s,\delta)]=\\{(s,\beta):\ \beta<\alpha\\}$. Using Lemma 4.5, we
get that for every positive integer $i$, $f((\gamma,i))=(s,\beta_{i})$, where
$\beta_{i}<\alpha$ and $\beta_{i}\neq\beta_{j}$ for $i\neq j$. Since $\alpha$
is uncountable cardinal, there is $\eta<\alpha$ such that $\eta\neq\beta_{i}$
for every $i$. We have $(s,\eta)=f(t)$ for some $t\in A$ and
$[(s,\eta)]=[(s,\delta)]$. By Lemma 4.5, $[(s,\eta)]=[(s,\delta)]$ iff
$[t]=[(\gamma,1)]$; so $[t]=[(\gamma,1)]$; so $t=(\gamma,i)$ for some positive
integer $i$. We have $f((\gamma,i))=(s,\beta_{i})=f(t)=(s,\eta)$ \- a
contradiction. Consequently there is no isomorphism $f:\
\mathcal{A}\rightarrow\mathcal{B}$.

Thus $SAPP$ is not $\alpha$-categorical. $\Box$

## References

  * [1] Balbiani, P. and Tinchev, T., (2007).  Line-based affine reasoning in Euclidean plane. Journal of Applied Logic, 5(3):421-434.
  * [2] Basu, S. (1999).  New results on quantifier elimination over real closed fields and applications to constraint databases. JACM, 46(4):537-555.
  * [3] Basu, S., Pollack, R. and Roy, M.-F. (1996).  On the combinatorial and algebraic complexity of quantifier elimination. Journal ACM, 43(6):1002-1045.
  * [4] Beth, E. and Tarski, A. (1956).  Equilaterality as the only primitive notion of Euclidean geometry. Indag. Math., 18:462-467.
  * [5] Collins, G. E. (1998).  Quantifier elimination by cylindrical algebraic decomposition - twenty years of progress. In Caviness, B. F. and Johnson, J. R., editors, Quantifier Elimination and Cylindrical Algebraic Decomposition, pp. 8-23. Springer-Verlag, New York.
  * [6] Gupta, H. N. (1965).  Contributions to the axiomatic foundations of geometry. Doctoral dissertation, University of California, Berkeley, 407 pp.
  * [7] Heintz, J., Roy, M. and Solerno, P. (1990).  Sur la complexite du principe de Tarski-Seidenberg. Bull. Soc. Math. France, 118:101-126.
  * [8] Hilbert, D. (1950).  Foundations of Geometry. La Salle, Illinois.
  * [9] Monk, L. (1974).  Elementary recursive decision procedures. Ph. D. thesis, University of California, Berkeley.
  * [10] Pasch, M. (1882).  Vorlesungen über neuere Geometrie. B.G.Teubner, Leipzig.
  * [11] Pieri, M. (1908).  La geometria elementare istituita sulle nozioni ’punto’ é ’sfera’. Memorie di Matematica e di Fisica della Società Italiana delle Scienze, 15:345-450.
  * [12] Renegar, J. (1992).  On the computational complexity and geometry of the first-order theory of the reals. J. Symb. Comput., 13(3):255-352.
  * [13] Schwabhäuser, W. and Szczerba, L. (1975).  Relations on lines as primitive notions for Euclidean geometry. Fund. Math., LXXXII:347–355.
  * [14] Schwabhäuser, W., Szmielew, W. and Tarski, A. (1983).  Metamathematische Methoden in der Geometrie. Hochschultext, Springer-Verlag, Berlin, viii+482 pp.
  * [15] Scott, D. (1959).  Dimension in elementary Euclidean geometry. In Henkin et al., pp. 53-67.
  * [16] Szczerba, L. and Tarski, A. (1965).  Metamathematical properties of some affine geometries. In Bar-Hillel, Y., editor, Proceedings of the 1964 International Congress for Logic, Methodology and Philosophy of Science, Studies in Logic and the Foundations of Mathematics, Amsterdam. North-Holland Publishing Company.
  * [17] Szczerba, L. and Tarski, A. (1979).  Metamathematical discussion of some affine geometries. Fund. Math., 104:155-192.
  * [18] Tarski, A.  A decision method for elementary algebra and geometry. prepared for publication by J.C.C. McKinsey, U.S. Air Force Project RAND, R-109, the RAND Corporation, Santa Monica, 1948, iv+60 pp.; a second, revised edition was published by the University of California Press, Berkeley and Los Angeles, CA, 1951, iii+63 pp.
  * [19] Tarski, A. (1956).  A general theorem concerning primitive notions of Euclidean geometry. Indagationes Mathematicae, 18:468-474.
  * [20] Tarski, A. (1959).  What is elementary geometry?, The axiomatic method, with special reference to geometry and physics (L. Henkin, P. Suppes, and A. Tarski, editors), North-Holland Publishing Company, Amsterdam, pp. 16-29.
  * [21] Tarski, A. (1967).  The completeness of elementary algebra and geometry. Institut Blaise Pascal, Paris, iv+50 pp.
  * [22] Tarski, A. and Givant, S. (1999).  Tarski’s System of Geometry. The Bulletin of Symbolic Logic, 5(2):175-214. JSTOR, www.jstor.org/stable/421089.
  * [23] Veblen, O. (1904).  A system of axioms for geometry. Transactions of the American Mathematical Society, 5:343-384.
  * [24] Veblen, O. (1914).  The foundations of geometry. In Young, J., editor, Monographs on topics of modern mathematics, relevant to the elementary field, pp. 1–51. Longsman, Green, and Company, New York.