Axioms for the Euclidean Plane

Here is a set theoretic version of Tarski's axioms where:

p is the set of points in the Euclidean plane.

B(x,y,z) means y is between x and z. Or y is on the line segment xz, possibly at the endpoints.

m(a,b)=m(c,d) means the length (or measure) of lines segments ab and cd are equal. It is like a metric in p, except
that it assigns no value to the distance between two points. It indicates only when points are equidistant. Note 
that the transitiviy of "=" is built into DC Proof.


Let p be a set, the set of points in the Euclidean plane

1	Set(p)
	Premise

Identity of Betweeness

2	ALL(a):ALL(b):[a ε p & b ε p & B(a,b,a) => a=b]
	Premise

Existence of at least three non-collinear points in p.(More than 1 dimension)

3	EXIST(a):EXIST(b):EXIST(c):[a ε p & b ε p & c ε p & ~B(a,c,b) & ~B(b,a,c) & ~B(a,b,c)]
	Premise

Axiom of Pasch. Line segments, which connect any two vertices of a given triangle with the sides opposite
the vertices, will intersect at a point inside the triangle.

4	ALL(a):ALL(b):ALL(c):ALL(d):ALL(e):[a ε p & b ε p & c ε p & d ε p & e ε p
	& B(a,d,b) & B(b,e,c)
	=> EXIST(f):[f ε p & B(a,f,e) & B(c,f,d)]]
	Premise

Identity of Congruence

5	ALL(a):ALL(b):ALL(c):[a ε p & b ε p & c ε p & m(a,b)=m(c,c) => a=b]
	Premise

Reflexivity of Congruence

6	ALL(a):ALL(b):[a ε p & b ε p => m(a,b)=m(b,a)]
	Premise

Segment Construction. Given any two line segments ab and cd, ab can be "extended" by a line segment congruent to cd.

7	ALL(a):ALL(b):ALL(c):ALL(d):[a ε p & b ε p & c ε p & d ε p
	=> EXIST(e):[e ε p & B(a,b,e) & m(b,e)=m(c,d)]]
	Premise

Three points c, d, e, which are equidistant from two distinct points a, b, determine a line. (Less than 3 dimensions)

8	ALL(a):ALL(b):ALL(c):ALL(d):ALL(e):[a ε p & b ε p & c ε p & d ε p & e ε p
	& ~a=b
	& m(a,c)=m(b,c) & m(a,d)=m(b,d) & m(a,e)=m(b,e)
	=> B(c,d,e) | B(c,e,d) | B(e,c,d)]
	Premise

Axiom of Euclid. Given any angle abc and any point e in its interior, there exists a line segment fg, which
includes e, with an endpoint on each side of the angle.

9	ALL(a):ALL(b):ALL(c):ALL(d):ALL(e):[a ε p & b ε p & c ε p & d ε p & e ε p
	& B(b,d,e) & B(a,d,c) & ~b=d
	=> EXIST(f):EXIST(g):[f ε p & g ε p & B(b,a,f) & B(b,c,g) & B(f,e,g)]]
	Premise

Five Segment. Given any two triangles abc and a'b'c', with d on ac and d' on a'c', ab=a'b', ad=a'd', dc=d'c',
and bd=b'd', then bc=b'c' and both triangles are congruent.

10	ALL(a):ALL(a'):ALL(b):ALL(b'):ALL(c):ALL(c'):ALL(d):ALL(d'):[a ε p & a' ε p & b ε p & b' ε p & c ε p & c' ε p & d ε p & d' ε p
	& ~a=d
	& B(a,d,c) & B(a',d',c')
	& m(a,b)=m(a',b') & m(a,d)=m(a',d') & m(d,c)=m(d',c') & m(b,d)=m(b',d')
	=> m(b,c)=m(b',c')]
	Premise

Axiom of Continuity. For any two subsets a, b of p if there exists d such that all elements of a are between d and 
all elements of b, then there exists a g such that g is between all elements of a and all elements of b.

11	ALL(a):ALL(b):[Set(a) & Set(b)
	& ALL(c):[c ε a => c ε p]
	& ALL(c):[c ε b => c ε p]
	& EXIST(d):[d ε p & ALL(e):ALL(f):[e ε a & f ε b => B(d,e,f)]]
	=> EXIST(g):[g ε p & ALL(h):ALL(i):[h ε a & i ε a => B(h,g,i)]]]
	Premise