`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′ A′ B′ C′)
var (object a b c a′ b′ c′)
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))))
stmt (NegatedCongruenceIdentityFromEquality () ()
(→ (∧ (¬ (= A B)) (≡ A B C D)) (¬ (= C D))))
#
# == Betweenness ==
# The other fundamental formula is betweenness; `(between x y z)`

signifies "y is between x and z".
#
term (formula (between x y z))
#
# There are no points between a point and itself.
stmt (IndivisibilityBidirectional () () (↔ (between x y x) (= x y)))
stmt (IndivisibilityFromEquality () () (→ (∧ (= x z) (between x y z)) (= x y)))
#
# A point is between itself and any second point.
stmt (BetweenABB () () (between A B B))
stmt (BetweenAAB () () (between A A B))
#
# In addition, this situation (a point is between itself and another) is the only way that betweenness can hold both as-is and with the first two points exchanged.
stmt (BetweennessEquality () () (→ (∧ (between A B C) (between B A C)) (= A B)))
#
# The two endpoints of a betweenness relation are interchangeable.
stmt (BetweennessSymmetry () () (↔ (between A B C) (between C B A)))
stmt (swapBetweennessInConsequent () ((→ antecedent (between A B C)))
(→ antecedent (between C B A)))
#
# === Transitivity ===
# In this section we present six similar theorems which involve four points on a line. Given two betweenness relationships, we conclude a third. Three of the six are just versions of the other three which are flipped left-to-right.
stmt (BetweennessInnerTransitivity () ()
(→ (∧ (between A B D) (between B C D)) (between A B C)))
stmt (BetweennessInnerTransitivityFlipped () ()
(→ (∧ (between A B C) (between A C D)) (between B C D)))
stmt (BetweennessOuterTransitivity () ()
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (between A B D)))
stmt (BetweennessOuterTransitivityFlipped () ()
(→ (∧ (∧ (between A B C) (between B C D)) (¬ (= B C))) (between A C D)))
stmt (BetweennessMiddleTransitivity () ()
(→ (∧ (between A B D) (between B C D)) (between A C D)))
stmt (BetweennessMiddleTransitivityFlipped () ()
(→ (∧ (between A B C) (between A C D)) (between A B D)))
#
# == 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.
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)))
#
# == Existence of distinct points ==
# Here we can construct a point distinct from a given point, or a point distinct from a given point extended along a given line segment.
stmt (PointConstructionDifferent ((A c) (B c)) ()
(∃ c (∧ (between A B c) (¬ (= B c)))))
stmt (AnotherPoint ((A b)) () (∃ b (¬ (= A b))))
#
# == Triangle congruence ==
# === Five segment ===
#