# Creative Commons Attribution-Share Alike 3.0 Unported (http://creativecommons.org/licenses/by-sa/3.0/) # {{modules # | parameters = [[Interface:Classical propositional calculus|Classical propositional calculus]], [[Interface:First-order logic with quantifiability|first-order logic]] # | importedby = [[Line segment inequality]] # | exportedby = [[Connectivity for betweenness]] # }} # # {{geometry series brief}} # # We build on [[Interface:Classical propositional calculus|propositional logic]] and [[Interface:First-order logic with quantifiability|first-order logic]] (including equality): # param (CLASSICAL Classical_propositional_calculus.ghi () "") param (FIRSTORDER First-order_logic_with_quantifiability.ghi (CLASSICAL) "") # # The kind `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 === # # File:Five segment.svg|Outer five segment # File:Inner five segment.svg|Inner five segment # # The five segment theorems are variations of the familiar congruences for triangles (although without any explicit reference to angles). stmt (OuterFiveSegment () () (→ (∧ (∧ (∧ (∧ (∧ (∧ (¬ (= x y)) (between x y z)) (between x′ y′ z′)) (≡ x y x′ y′)) (≡ y z y′ z′)) (≡ x u x′ u′)) (≡ y u y′ u′)) (≡ z u z′ u′)) ) stmt (InnerFiveSegment () () (→ (∧ (∧ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x z x′ z′)) (≡ y z y′ z′)) (≡ x u x′ u′)) (≡ z u z′ u′)) (≡ y u y′ u′))) stmt (FiveSegment () () (→ (∧ (∧ (∧ (∧ (¬ (= A B)) (collinear A B C)) (≅ A B C A′ B′ C′)) (≡ A D A′ D′)) (≡ B D B′ D′)) (≡ C D C′ D′))) # # === Three segment === # The three segment theorems can be thought of as degenerate cases of five segment, or as basic properties of points on a line. stmt (OuterThreeSegment () () (→ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x y x′ y′)) (≡ y z y′ z′)) (≡ x z x′ z′))) stmt (InnerThreeSegment () () (→ (∧ (∧ (∧ (between x y z) (between x′ y′ z′)) (≡ x z x′ z′)) (≡ y z y′ z′)) (≡ x y x′ y′))) # # === Some degenerate triangle congruence theorems === stmt (BetweennessDegenerateTriangle () () (→ (∧ (between A B C) (≅ A B C A′ B′ C′)) (between A′ B′ C′))) stmt (CollinearityDegenerateTriangle () () (→ (∧ (collinear A B C) (≅ A B C A′ B′ C′)) (collinear A′ B′ C′))) stmt (InnerDegenerateTriangle ((A b′) (B b′) (C b′) (A′ b′) (C′ b′)) () (→ (∧ (between A B C) (≡ A C A′ C′)) (∃ b′ (∧ (between A′ b′ C′) (≅ A B C A′ b′ C′))))) stmt (CollinearityConstructDegenerateTriangle ((A c′) (B c′) (C c′) (A′ c′) (B′ c′)) () (→ (∧ (collinear A B C) (≡ A B A′ B′)) (∃ c′ (≅ A B C A′ B′ c′)))) # # == Tarski's axioms == # We repeat those axioms which are not subsumed by the theorems we have proved so far. Explanations are at [[Interface:Tarski's geometry axioms]]. stmt (Pasch ((x a) (u a) (z a) (y a) (v a)) () (→ (∧ (between x u z) (between y v z)) (∃ a (∧ (between u a y) (between v a x))))) tvar (formula φx ψy) var (object xx yy) stmt (Continuity ((φx yy) (φx a) (φx b) (ψy xx) (ψy a) (ψy b) ) () (→ (∃ a (∀ xx (∀ yy (→ (∧ φx ψy) (between a xx yy))))) (∃ b (∀ xx (∀ yy (→ (∧ φx ψy) (between xx b yy))))))) stmt (LowerDimension () () (∃ a (∃ b (∃ c (∧ (∧ (¬ (between a b c)) (¬ (between b c a))) (¬ (between c a b)) ))))) stmt (UpperDimension () () (→ (∧ (∧ (∧ (≡ x u x v) (≡ y u y v)) (≡ z u z v)) (¬ (= u v))) (∨ (∨ (between x y z) (between y z x)) (between z x y)))) stmt (AxiomEuclid ((x b a) (u b a) (v b a) (y b a) (z b a)) () ( → (∧ (∧ (between x u v) (between y u z)) (¬ (= x u))) (∃ a (∃ b (∧ (∧ (between x y a) (between x z b)) (between a v b)))))) tvar (object x0 x1 x2 x3 y0 y1 y2 y3) stmt (CongruenceBuilder () () ( → (∧ (∧ (∧ (= x0 y0) (= x1 y1)) (= x2 y2)) (= x3 y3)) (↔ (≡ x0 x1 x2 x3) (≡ y0 y1 y2 y3)) )) stmt (BetweennessBuilder () () ( → (∧ (∧ (= x0 y0) (= x1 y1)) (= x2 y2)) (↔ (between x0 x1 x2) (between y0 y1 y2)) )) stmt (CollinearityBuilder () () ( → (∧ (∧ (= x0 y0) (= x1 y1)) (= x2 y2)) (↔ (collinear x0 x1 x2) (collinear y0 y1 y2)) )) # # == References == # # # {{DEFAULTSORT:{{PAGENAME}}}} # [[Category:Euclidean geometries (general) and generalizations]] # [[Category:Foundations of classical theories (including reverse mathematics)]]