# Further study of "Elementary geometry" in the sense of Tarski

Tarski in the article "WHAT IS ELEMENTARY GEOMETRY" describes four candidates ($$\mathscr{E}_2,\mathscr{E}'_2,\mathscr{E}''_2,\mathscr{E}'''_2$$) to be called "Elementary geometry". Here the name "elementary" for a geometry comes from fact that it is formalized within elementary logic i.e., first-order predicate calculus (with may be little extension of language with non-first-order, fin-set variables).

Question: What was made after that paper in this direction? In particular did some problems mentioned in the paper and open for the moment of publication of the paper find their answers?

Here below I briefly write down the problems that Tarski addresses in the paper.

The symbolism of $$\mathscr{E}_2$$ consnists of first order variables $$x,y,\dots$$, two predicates $$\beta(xyz)$$ and $$\delta(xyzu)$$ for betweenness and equidistantness respectively, $$=$$,$$\neq$$,and the first-order quantifiers $$\forall$$,$$\exists$$.

The axiomatization of the theory $$\mathscr{E}_2$$ consists of twelwe axioms A1-A12 and infinite collection of continuity axioms A13:

A1: $$\forall xy\left[\beta(xyx)\to(x=y)\right]$$ (Identity axiom for betweenness)
A2: $$\forall xyzu\left[\beta(xyu)\wedge\beta(yzu)\to\beta(xyz)\right ]$$ (Transitivity axiom for betweenness)
A3: $$\forall xyzu\left[\beta(xyz)\wedge \beta(xyu)\wedge (x\neq y)\to \beta(xzu)\vee \beta(xuz)\right]$$ (Connectivity axiom)
A4: $$\forall xy\left[\delta(xyyx)\right]$$ (Reflexivity axiom for equidistance)
A5: $$\forall xyz \left[\delta(xyzz)\to (x=y)\right]$$ (Identity axiom for equidistance)
A6: $$\forall xyzuvw\left[\delta(xyzu)\wedge \delta(xyvw)\to \delta(zuvw)\right]$$ (Transitivity axiom for equidistance)
A7: $$\forall txyzu~\exists v\left[\beta(xtu)\wedge \beta(yuz)\to \beta(xvy)\wedge\beta(ztv)\right]$$ (Pash's axiom)
A8: $$\forall txyzu \exists vw\left[\beta(xut)\wedge\beta(yuz)\wedge (x\neq u)\to \beta(xzv)\wedge\beta(xyw)\wedge\beta(vtw)\right]$$ (Euclid)
A9:$$\forall xx'yy'zz'uu'\left[ \delta(xyx'y')\wedge\delta(yzy'z')\wedge\delta(xux'u')\wedge\delta(yuy'u')\wedge\\ ~~~~~~~~~~~~~~~~~~~~~~~~~~\beta(xyz)\wedge\beta(x'y'z')\wedge(x\neq y)\to \delta(zuz'u') \right] \textbf{(Five-segmet)}$$
A10:$$\forall xyuv \exists z\left[\beta(xyz)\wedge\delta(yzuv)\right]$$ (Segment construction) A11:$$\forall xyz\left[\neg\beta(xyz)\wedge \neg\beta(yzx)\wedge \neg\beta(zxy)\right]$$ (Lower dimension axiom)
A12:$$\forall xyzuv \left[ \delta(xuxv)\wedge\delta(yuyv)\wedge\delta(zuzv)\wedge (u\neq v)\to \beta(xyz)\vee\beta(yzx)\vee\beta(zxy)\right]$$
All sentences of the form:
A13:$$\forall vw\dots\{\exists z \forall xy\left[ \varphi\wedge \psi\to \beta(zxy)\right]\to \exists u \forall xy\left[ \varphi\wedge \psi\to \beta(xuy)\right]\}$$
where $$\varphi$$ stands for any formula in which the variables $$x,v,w,\dots$$, but neither $$y$$ nor $$z$$ nor $$u$$, occur free, and similarly for $$\psi$$, with $$x$$ and $$y$$ interchanged.

Below are stated fundamental properties of the theory $$\mathscr{E}_2$$ by Tarski.

Thm 1 (Representation theorem). For $$\mathfrak{M}$$ to be a model of $$\mathscr{E}_2$$ it is neccessary and sufficient that $$\mathfrak{M}$$ be isomorphic with the cartesian space $$\mathfrak{C}_2(\mathfrak{F})$$ over some closed field $$\mathfrak{F}$$.

A theory is called complete if every sentence $$\sigma$$ (formulated in the symbolism of the theory) holds either in every model of this theory or in no such model.

A theory is called consistent if it has at least one model.

Thm 2 (Completeness theorem). (i) A sentence formulated in $$\mathscr{E}_2$$ is valid if and only if it holds in $$\mathfrak{C}_2(\mathfrak{R})$$ (whre $$\mathfrak{R}$$ is the field of real numbers);

(ii) the theory $$\mathscr{E}_2$$ is complete (and consistent).

Since every complete and axiomatizable theory with standard formalization is decidable, therefore $$\mathscr{E}_2$$ is decidable.

Thm 3. (Decision theorem). The theory $$\mathscr{E}_2$$ is decidable.

the theory has no finite axiomatization.

Thm 4 (Non-finitizability theorem). The theory $$\mathscr{E}_2$$ is not finitely axiomatizable.

In what follows he discusses two other possible interpretations of the term "elementary geometry"; which are embodied in two different formalized theories, $$\mathscr{E}'_2$$ and $$\mathscr{E}''_2$$.

The theory $$\mathscr{E}'_2$$ is obtained from $$\mathscr{E}_2$$ is by including in the symbolism of $$\mathscr{E}'_2$$ new variables $$X,Y,\dots$$ assumed to range over arbitrary finite sets and the membership symbol $$\in$$ to denote the membership relation between points and finite sets. As axioms are again chosen A1-A13 (but now with stronger expressibility).

In $$\mathscr{E}'_2$$ one can formulate e.g., the notions of a polygon with arbitrary many vertices, and of the circumference and the area of a circle, which cannot be expresssed in $$\mathscr{E}_2$$.

On time of publication three of above theorems when referred to $$\mathscr{E}'_2$$ are open for Tarski - the problem of representation, completeness, and finite axiomatizability.

Only the decision problem for $$\mathscr{E}'_2$$ has found so far a definite solution:

Thm 5. The theory $$\mathscr{E}'_2$$ is undecidable, and so are all its consistent extensions.

This follows from the fact that Peano's arithmetic is (relatively) interpetable in $$\mathscr{E}'_2$$.

To obtain $$\mathscr{E}''_2$$ Tarski leaves the symbolism of $$\mathscr{E}_2$$ unchanged but weakens the axiom system of $$\mathscr{E}_2$$. In fact he replaces the infinite collection of axioms A13, by a single sentence, A13', which expresses the fact that a segment which joins two points, one inside and one outside a given circle, always intersect the circle:

A13': $$\forall xyzx'z'u \exists y'\left[\delta(uxux')\wedge\delta(uzuz')\wedge\beta(uxz)\wedge\beta(xyz)\to \delta(uyuy')\wedge\beta(x'y'z')\right]$$

The weakening applies in particular to existential theorems which cannot be established by neans of so called elementary geometrical constructions (using exclusively ruler and compass), e.g., to the theorem on the trisection of an arbitrary angle.

The three problems which were open for $$\mathscr{E}'_2$$ admit of simple definite answer when referred to $$\mathscr{E}''_2$$.

Thm 6. For $$\mathfrak{M}$$ to be a model of $$\mathscr{E}''_2$$ it is necessary and sufficient that $$\mathfrak{M}$$ be isomorphic to Cartesian space $$\mathfrak{C}_2(\mathfrak{F})$$ over some Euclidean field $$\mathfrak{F}$$.

Using this he easily obtains incompleteness, and from description it is obvious that $$\mathscr{E}''_2$$ is finitely axiomatizable.

On the other hand, the decision problem for $$\mathscr{E}''_2$$ remains open for tarski on moment of publication. Tarski climes that the answer is negative, he even climes that no finitely axiomatizable theory of $$\mathscr{E}_2$$ is decidable.

The difference between $$\mathscr{E}_2$$ and $$\mathscr{E}''_2$$ vanishes on the level of universal sentences.

Thm 7. A universal sentence formulated in $$\mathscr{E}_2$$ is valid in $$\mathscr{E}_2$$ if and only if it is valid in $$\mathscr{E}''_2$$.

To the end Tarski mentions that one could discuss some further theories e.g., the theory $$\mathscr{E}'''$$ which has the same symbolism as $$\mathscr{E}'_2$$ and the same axioms as $$\mathscr{E}''_2$$, but write nothing about the properties of the last.

• The first place to look is the monograph Schwabhäuser, Szmielew, Tarski, Metamathematische Methoden in der Geometrie, 1983. Jul 4 '19 at 16:34

As you note, Tarski claimed that no finitely axiomatizable subtheory of $$\mathcal{E}_2$$ is decidable. Since $$\mathcal{E}_2$$ and the theory of real-closed ordered fields are bi-interpretable, Tarski's conjecture was essentially established by M. Ziegler (Einige unentscheidbare Körpertheorien Enseign. Math. (2) 28 (1982), no. 3-4, 269–280), who showed that every nontrivial finitely axiomatized subtheory of the theory of real-closed ordered fields is not decidable.
• Thank you a lot it is the answer I was waited for. Is it known something about representation, completeness, and finite axiomatizability of $\mathscr{E}'_2$ Jul 4 '19 at 19:50