# Formal developments in Geometry

#### solakis

##### Active member
I wonder if we can have a 1st order Goemetry

#### caffeinemachine

##### Well-known member
MHB Math Scholar
I wonder if we can have a 1st order Goemetry
The logician Alfred Tarski devised a 1st order axiomatization for plane Euclidean geometry.

#### solakis

##### Active member
The logician Alfred Tarski devised a 1st order axiomatization for plane Euclidean geometry.
Where in which book.

#### caffeinemachine

##### Well-known member
MHB Math Scholar
Where in which book.
I don't know that. I just know that he did. If you want to read the theory then you have to google about a bit.

#### solakis

##### Active member
I don't know that. I just know that he did. If you want to read the theory then you have to google about a bit.
Alfred Tarski in his book: INTRODUCTION TO LOGIC he developed the axiomatic theory for real Nos and nothing about Geometry.

No where in the internet there is a first order development of Geometry

#### caffeinemachine

##### Well-known member
MHB Math Scholar
Alfred Tarski in his book: INTRODUCTION TO LOGIC he developed the axiomatic theory for real Nos and nothing about Geometry.

No where in the internet there is a first order development of Geometry
I quote from wiki,

"In the 1920s and 30s, Tarski often taught high school geometry. Using some ideas of Mario Pieri, in 1926 Tarski devised an original axiomatization for plane Euclidean geometry, one considerably more concise than Hilbert's. Tarski's axioms form a first-order theory devoid of set theory, whose individuals are points, and having only two primitive relations. In 1930, he proved this theory decidable because it can be mapped into another theory he had already proved decidable, namely his first-order theory of the real numbers."

See Alfred Tarski - Wikipedia, the free encyclopedia

#### solakis

##### Active member
I quote from wiki,

"In the 1920s and 30s, Tarski often taught high school geometry. Using some ideas of Mario Pieri, in 1926 Tarski devised an original axiomatization for plane Euclidean geometry, one considerably more concise than Hilbert's. Tarski's axioms form a first-order theory devoid of set theory, whose individuals are points, and having only two primitive relations. In 1930, he proved this theory decidable because it can be mapped into another theory he had already proved decidable, namely his first-order theory of the real numbers."

See Alfred Tarski - Wikipedia, the free encyclopedia
According to wiki ,how then would we formalize the very 1st axiom of Geometry.

There is exactly one straight line on two distinct points

#### Klaas van Aarsen

##### MHB Seeker
Staff member
According to wiki ,how then would we formalize the very 1st axiom of Geometry.

There is exactly one straight line on two distinct points
Here's an axiomatization by Hilbert on geometry:
http://www.gutenberg.org/files/17384/17384-pdf.pdf

The actual axiom (apart from the necessary definitions) is:
I, 1. Two distinct points A and B always completely determine a straight line a. We write AB = a or BA = a.​

Note that points and lines are just abstract concepts that are referenced by the axioms.
They don't have to be anything like real-life points or lines.
For instance, a line might actually be a plane (in projective geometry).