Pasch's Axiom in Euclidean Geometry

U

0.5

T

0.5

show lines

Tarski axiomatized Euclidean plane geometry in first-order logic using two primitive relations: the formula

β(XYZ)

means "

Y

lies between

X

and

Z

", while

δ(XYZU)

means "

X

is as distant from

Y

as

Z

is from

U

". Using

β

, Pasch's axiom has the form

(∃V)(β(XTU)∧β(YUZ)⇒β(XVY)∧β((ZTV))

.

This Demonstration illustrates the axiom.