`object`

, defined in first-order logic, represents a point. We do not directly have a concept of lines, angles, or circles (nor can these be defined in the obvious way as sets of points, as this is a first-order theory).
tvar (object x y z w u v A B C D Q)
tvar (object x′ y′ z′ u′)
var (object a b c xx yy)
tvar (formula antecedent)
#
# == Congruence of line segments ==
# We introduce congruence of line segments; `(x y ≡ w z)`

means that the line segment `x y`

is the same length as the line segment `w z`

. This property is also known as equidistance.
term (formula (≡ x y z w))
#
# There are a variety of ways of expressing the idea that congruence is not affected by the order in which we list the line segment's endpoints.
stmt (CongruenceLeftCommutativity () () (↔ (≡ x y z w) (≡ y x z w)))
stmt (CongruenceRightCommutativity () () (↔ (≡ x y z w) (≡ x y w z)))
stmt (CongruenceCommutativity () () (↔ (≡ x y z w) (≡ y x w z)))
stmt (commuteCongruenceLeftInConsequent () ((→ antecedent (≡ x y z w)))
(→ antecedent (≡ y x z w)))
stmt (commuteCongruenceRightInConsequent () ((→ antecedent (≡ x y z w)))
(→ antecedent (≡ x y w z)))
stmt (commuteCongruenceInConsequent () ((→ antecedent (≡ x y z w)))
(→ antecedent (≡ y x w z)))
#
# The congruence relation has the attributes of an equivalence relation between line segments.
stmt (CongruenceReflexivity () () (≡ x y x y))
stmt (CongruenceSymmetry () () (↔ (≡ x y z w) (≡ z w x y)))
stmt (CongruenceTransitivity () () (→ (∧ (≡ x y z w) (≡ z w u v)) (≡ x y u v)))
stmt (CongruenceABBA () () (≡ x y y x))
stmt (swapCongruenceInConsequent () ((→ antecedent (≡ x y z w)))
(→ antecedent (≡ z w x y)))
#
# A segment which has zero length starts and ends at the same point (although saying "zero length" is a bit of a shortcut, as our theory is not based on real numbers or any other numbers).
stmt (CongruenceIdentity () () (→ (≡ x y z z) (= x y)))
stmt (CongruenceIdentityLeft () () (→ (≡ x x y z) (= y z)))
stmt (CongruenceTrivialIdentity () () (≡ y y x x))
stmt (CongruenceIdentityFromEquality () () (→ (= x y) (→ (≡ x y z w) (= z w))))
#
# == Segment construction ==
# A line segment can be extended beyond one of its endpoints by a specified distance (where by "distance" we mean a second line segment, which the constructed segment is to be congruent to). The segment extended this way is unique.
term (formula (between x y z))
stmt (SegmentConstruction ((w a) (x a) (y a) (z a)) () (∃ a (∧ (between w x a) (≡ x a y z))))
stmt (SegmentConstructionUniqueness () () (→ (∧ (∧ (∧ (∧ (¬ (= Q A)) (between Q A x)) (≡ A x B C)) (between Q A y)) (≡ A y B C)) (= x y)))
#
# == Five segment ==
#