`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 P Q)
tvar (object x′ y′ z′ u′ A′ B′ C′ D′)
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 (CongruenceIdentityFromEqualityImported () () (→ (∧ (= 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)))
#
# === Connectivity ===
stmt (BetweennessOuterConnectivity () ()
(→ (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D)) (∨ (between A C D) (between A D C))))
#
# == 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))))
#
# == Collinearity ==
# To say that three points are collinear is just to say that one of them is between the other two (in any order).Definition Col in Narboux
term (formula (collinear x y z))
stmt (Collinear () () (↔ (collinear x y z) (∨ (∨ (between x y z) (between y z x)) (between z x y))))
stmt (BetweennessCollinearity () () (→ (between x y z) (collinear x y z)))
stmt (CollinearityRotation () () (↔ (collinear x y z) (collinear y z x)))
stmt (Collinearity23 () () (↔ (collinear x y z) (collinear x z y)))
stmt (Collinearity12 () () (↔ (collinear x y z) (collinear y x z)))
stmt (Collinearity13 () () (↔ (collinear x y z) (collinear z y x)))
#
# A point, itself, and any second point are collinear.
stmt (CollinearityAAB () () (collinear A A B))
stmt (CollinearityABB () () (collinear A B B))
stmt (CollinearityABA () () (collinear A B A))
#
# == Determining lines, or points, by distance to two points ==
# If two given points are equidistant to each of two distinct points on a line, they are equidistant to every point on that line.
stmt (EquidistantLine () ()
(→ (∧ (∧ (∧ (¬ (= A B)) (collinear A B C)) (≡ A P A Q)) (≡ B P B Q)) (≡ C P C Q)))
#
# On a given line, the distance to two points can uniquely determine a point. We have two versions: one in which the two given points are distinct, and one in which they are endpoints of a line segment on which the point lies.
stmt (CollinearTwoDistanceUniqueness () ()
(→ (∧ (∧ (∧ (¬ (= A B)) (collinear A B C)) (≡ A C A C′)) (≡ B C B C′)) (= C C′)))
stmt (BetweennessTwoDistanceUniqueness () () (→ (∧ (∧ (between A C B) (≡ A C A C′)) (≡ B C B C′)) (= C C′)))
#
# == Triangle congruence ==
# === Triangle congruence defined ===
# We provide a term for congruence of (possibly degenerate) triangles, and a theorem corresponding to the familiar side-side-side property of triangle congruence. We allow degenerate triangles: the points may be collinear, and need not all be distinct from each other.
term (formula (≅ x y z x′ y′ z′))
stmt (TriangleCongruence () () (↔ (≅ x y z x′ y′ z′) (∧ (∧ (≡ x y x′ y′) (≡ x z x′ z′)) (≡ y z y′ z′))))
# The corresponding sides of congruent (possibly degenerate) triangles are congruent.
stmt (Congruence12 () () (→ (≅ A B C A′ B′ C′) (≡ A B A′ B′)))
stmt (Congruence23 () () (→ (≅ A B C A′ B′ C′) (≡ B C B′ C′)))
stmt (Congruence13 () () (→ (≅ A B C A′ B′ C′) (≡ A C A′ C′)))
#
# Rotate the order of points in a triangle congruence.
stmt (CongruenceRotation () () (↔ (≅ A B C A′ B′ C′) (≅ B C A B′ C′ A′)))
#
# === Five segment ===
#