MHB Formal developments in Geometry

[solakis1]

I wonder if we can have a 1st order Goemetry

 

[caffeinemachine]

I wonder if we can have a 1st order Goemetry

The logician Alfred Tarski devised a 1st order axiomatization for plane Euclidean geometry.

 

[solakis1]

The logician Alfred Tarski devised a 1st order axiomatization for plane Euclidean geometry.

Where in which book.

 

[caffeinemachine]

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.

 

[solakis1]

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]

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

 

[solakis1]

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

 

[I like Serena]

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).