`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 E P Q)
tvar (object x′ y′ z′ u′ A′ B′ C′ D′)
var (object a b c a′ b′ c′ e f p)
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)))
#
# === Connectivity ===
stmt (BetweennessOuterConnectivity () ()
(→ (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))
(∨ (between A C D) (between A D C))))
stmt (BetweennessMiddleConnectivity () ()
(→ (∧ (∧ (¬ (= A B)) (between A B C)) (between A B D))
(∨ (between B C D) (between B D C))))
stmt (BetweennessInnerConnectivity () ()
(→ (∧ (between A B D) (between A C D))
(∨ (between A B C) (between A C B))))
#
# == 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)))
#
# Here is a similar construction, but from one of the given endpoints towards the other one, rather than away from it.
stmt (InnerSegmentConstruction
((Q p) (A p) (B p) (C p)) ()
(∃ p (∧ (∨ (between Q A p) (between Q p A)) (≡ Q p B C))))
#
# == 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))))
#
# == Inequality of line segments ==
# The formula `A B ≤ C D`

means that the line segment `A B`

is shorter than (or the same length as) the line segment `C D`

.
term (formula (≤ x y z w))
term (formula (≥ A B C D))
stmt (GreaterEqual () () (↔ (≥ A B C D) (≤ C D A B)))
#
# There are two equivalent ways of expressing this concept in terms of congruence. We can either cut off `C D`

with a point `e`

such that `A B ≡ C e`

, or we can extend `A B`

to a point `f`

such that `A f ≡ C D`

.
stmt (LessEqualCutoff
((A e) (B e) (C e) (D e)) ()
(↔ (≤ A B C D) (∃ e (∧ (between C e D) (≡ A B C e)))))
stmt (LessEqualExtension
((A f) (B f) (C f) (D f)) ()
(↔ (≤ A B C D) (∃ f (∧ (between A B f) (≡ A f C D)))))
#
# Given congruences between two pairs of line segments, a `≤`

relationship between the first pair carries over to the second pair.
stmt (LessEqualCongruence () ()
(→
(∧ (∧ (≤ A B C D) (≡ A B A′ B′)) (≡ C D C′ D′)) (≤ A′ B′ C′ D′)))
#
# === Total order ===
# It has the [[w:total order|properties of a total order]]:
tvar (object A0 A1 B0 B1 C0 C1)
stmt (LessEqualTransitivity () () (→ (∧ (≤ A0 A1 B0 B1) (≤ B0 B1 C0 C1)) (≤ A0 A1 C0 C1)))
stmt (LessEqualAntisymmetry () () (→ (∧ (≤ A0 A1 B0 B1) (≤ B0 B1 A0 A1)) (≡ A0 A1 B0 B1)))
stmt (LessEqualTotality () () (∨ (≤ A0 A1 B0 B1) (≤ B0 B1 A0 A1)))
#
# A number of other properties follow from those.
stmt (LessEqualReflexivity () () (≤ A0 A1 A0 A1))
term (formula (< A0 A1 B0 B1))
stmt (LessThan () () (↔ (< A0 A1 B0 B1) (∧ (≤ A0 A1 B0 B1) (¬ (≡ A0 A1 B0 B1)))))
term (formula (> B0 B1 A0 A1))
stmt (GreaterThan () () (↔ (> B0 B1 A0 A1) (< A0 A1 B0 B1)))
#
# === Empty segments and inequality ===
stmt (ZeroSmallest () () (≤ A A B C))
stmt (LessEqualZero () () (→ (≤ A B C C) (= 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′)))
#
# For the previous theorems, two distances are needed because the point `C′`

is not known to be on the line containing `A`

, `B`

, and `C`

. If we know that the points which are to be shown equal are on the same line, and the same side of the point `A`

, then one congruence suffices.
stmt (BetweennessOneDistanceUniqueness () ()
(→ (∧ (between A B C) (≡ A B A C)) (= B C)))
stmt (SameSegmentOneDistanceUniqueness () ()
(→ (∧ (∧ (between A D B) (between A E B)) (≡ A D A E)) (= D E)))
#
# == 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 ===
#