Welcome to our community

Be a part of something great, join today!

Formal developments in Geometry

solakis

Active member
Dec 9, 2012
304
I wonder if we can have a 1st order Goemetry
 

caffeinemachine

Well-known member
MHB Math Scholar
Mar 10, 2012
834
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
Dec 9, 2012
304

caffeinemachine

Well-known member
MHB Math Scholar
Mar 10, 2012
834
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
Dec 9, 2012
304
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
Mar 10, 2012
834
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
Dec 9, 2012
304
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
Mar 5, 2012
8,774
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).