Interface:Basic geometry

From Wikiproofs
Jump to: navigation, search
Module usage
Parameters
Classical propositional calculus, first-order logic
Imported by
None yet.
Exported by
Midpoint

Here we state a variety of basic geometrical theorems involving collinearity, midpoints, perpendiculars, and the like.

We build on propositional logic and first-order logic (including equality):

param (CLASSICAL Interface:Classical_propositional_calculus () () Unable to load parameter CLASSICAL(Interface:Classical_propositional_calculus)[]+: Unable to load module Interface:Classical_propositional_calculus

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 as sets of points, as this is a first-order theory).

Unknown command

Congruence of line segments[edit]

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.

Unknown command

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.

Unknown command

The congruence relation has the attributes of an equivalence relation between line segments.

Unknown command

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).

Unknown command

Betweenness[edit]

The other fundamental formula is betweenness; (between x y z) signifies "y is between x and z".

Unknown command

There are no points between a point and itself.

Unknown command

A point is between itself and any second point.

Unknown command

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.

Unknown command

The two endpoints of a betweenness relation are interchangeable.

Unknown command

Transitivity[edit]

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.

Unknown command

Connectivity[edit]

Unknown command

Segment construction[edit]

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.

Unknown command

Here is a similar construction, but from one of the given endpoints towards the other one, rather than away from it.

Unknown command

Inequality of line segments[edit]

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.

Unknown command

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.

Unknown command

Given congruences between two pairs of line segments, a relationship between the first pair carries over to the second pair.

Unknown command

Total order[edit]

It has the properties of a total order:

Unknown command

A number of other properties follow from those.

Unknown command

Empty segments and inequality[edit]

Unknown command

Collinearity[edit]

To say that three points are collinear is just to say that one of them is between the other two (in any order).[1]

Unknown command

A point, itself, and any second point are collinear.

Unknown command

Determining lines, or points, by distance to two points[edit]

If two given points are equidistant to each of two distinct points on a line, they are equidistant to every point on that line.

Unknown command

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.

Unknown command

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.

Unknown command

Triangle congruence[edit]

Triangle congruence defined[edit]

At least for now, we define triangle congruence here (rather than provide a theorem providing this definition, which corresponds to the familiar side-side-side property of triangle congruence). The definition allows degenerate triangles: the points may be collinear, and need not all be distinct from each other.

Unknown command

The corresponding sides of congruent (possibly degenerate) triangles are congruent.

Unknown command

Rotate the order of points in a triangle congruence.

Unknown command

Five segment[edit]

The five segment theorems are variations of the familiar congruences for triangles (although without any explicit reference to angles).

Unknown command

Three segment[edit]

The three segment theorems can be thought of as degenerate cases of five segment, or as basic properties of points on a line.

Unknown command

Some degenerate triangle congruence theorems[edit]

Unknown command

Existence of distinct points[edit]

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.

Unknown command

There exist three non-collinear points.

Unknown command

Given a line, there is a point which is not on that line.

Unknown command

Midpoints[edit]

A point is the midpoint of a line segment if it is between the endpoints and is equidistant from each one.

Unknown command

Whether a point is the midpoint does not depend on the order in which we list the endpoints.

Unknown command

An empty line segment has as its midpoint its endpoint.

Unknown command

Reflection through a point[edit]

Point symmetry, or reflection through a point, refers to the process of starting with a single point (which in special cases might be called the origin or the center) and mapping every point to a point directly opposite the given point (at the same distance).

The symmetric point exists and is unique.

Unknown command

Mapping to the symmetric point is one to one.

Unknown command

Mapping all points to the symmetric point preserves distance, line segment congruence, betweenness, and midpointness.

Unknown command

Midpoint exists and is unique[edit]

The midpoint exists[2] and is unique.[3][4]

Unknown command

Several other midpoint theorems[edit]

A point which is on a line with two distinct points and equidistant to both of them is the midpoint of the line segment between those points.

Unknown command
Color parallelogram.svg

The diagonals of a parallelogram bisect each other.[5] (By "parallelogram" here we mean a quadrilateral whose opposite sides are congruent; there is no direct statement concerning parallel lines).

Unknown command

Tarski's axioms[edit]

We repeat those axioms which are not subsumed by the theorems we have proved so far. Explanations are at Interface:Tarski's geometry axioms.

Unknown command

Builders[edit]

As usual, we need to state that equals can be substituted for equals via builders.

Unknown command

References[edit]

  1. Definition Col in Narboux
  2. TODO: add this
  3. l7_17 in Narboux
  4. Proposition 10 in book I of Euclid's Elements
  5. l7_21 in Narboux

Incomplete[edit]

Zeichen 123.svg This page is not yet done. To help finish it, edit the page (you can see if your edits are verifying by previewing them), go to Help:Contents if you haven't yet figured out how to edit and write proofs, or ask at WP:TEA if you have any questions.


This page has not yet been updated for all the theorems proved as part of the geometry series. For now, look at the latest interface file in the series.