{{interfaces | imports = Interface:Midpoint | exports = Interface:Orthogonality 1 }}

This is part of a series of modules which prove a variety of geometrical theorems starting with Tarski's axioms for geometry. We follow the formalization of Julien Narboux<ref>The formal proofs are at http://www.lix.polytechnique.fr/Labo/Julien.Narboux/tarski.html Formalization of Tarski's geometry in the Coq proof assistant and are described in Julien Narboux (2007), "http://citeseerx.ist.psu.edu/viewdoc/summary?doi= Mechanical Theorem Proving in Tarski’s Geometry", F. Botana and T. Recio (Eds.): ADG 2006, LNAI 4869, pp. 139–156</ref> which itself closely follows a treatise by Schwabhäuser, Szmielew, and Tarski.<ref>W. Schwabhäuser, W Szmielew, and A. Tarski (1983), ''Metamathematische Methoden in der Geometrie'', ISBN 0387129588</ref>

Here we prove results involving perpendicular lines. This also enables us to prove the existence of the midpoint of a line segment.

We import the theorems of propositional logic and predicate logic, and the geometry results so far and define some variables:

Right angles

thumb|right Our treatment of perpendicularity, on the page and following ones, is in terms of three related concepts. First is the perpendicularity of a line segment and another line segment which share an endpoint, in this diagram whether A B is perpendicular to B C. The second is whether a line segment is perpendicular to another line segment at a given point, for example whether A B is perpendicular to C D (or whether they are perpendicular if A B is specified by A and another point, not shown, on the line A B). The third is similar, but just whether there is a point where the two lines are perpendicular, without needing to mention that point explicitly.

We start with the first of those, a predicate which can be thought of as recognizing whether A B is perpendicular to B C{{{. We call it {{{is-right-angle even though it is not tied to any larger theory of angles (that will come later).<ref>Definition Per in Narboux</ref> The definition can be read as "∠ A B C is a right angle iff the symmetric point of C around B is as far from A as C is".

As usual, we'll need to restate the definition as a theorem.

A convenience rule

{{cleanup|moving applyCongruenceTransitivityInConsequent to where we define CongruenceTransitivity}}

Can interchange legs of a right angle

Although it isn't obvious from the definition, the roles of the two points which aren't the vertex are equivalent.<ref>l8_2 in Narboux</ref> To prove this, expand is-right-angle A B C according to the definition into ∃ c′ (B is-midpoint-of C c′ ∧ A C ≡ A c′). Then let a′ be the symmetric point of A around B. Since reflecting through a point preserves distances (SymmetricPointDistance), A c′ ≡ a′ C. This allows us to show is-right-angle C B A by the definition.

Picking a different point on a right angle's line

Given a right angle A B C where A B is a line (that is, A ≠ B), picking a different point A′ on the line A B also produces a right angle A′ B C.<ref>l8_3 in Narboux</ref>

Reflecting about the vertex

Reflecting one of the points of a right angle through the vertex of that angle produces a right angle. In symbols, is-right-angle A B C ∧ B is-midpoint-of C C′ → is-right-angle A B C′.<ref>l8_4 in Narboux</ref>.

The proof will start by expanding the definition of is-right-angle into ∃ c″ (B is-midpoint-of C c″ ∧ A C ≡ A c″). Then the result of reflecting C through B{{{ is unique, so {{{C″ = C′, which is our first lemma.

Degenerate cases

In defining is-right-angle we also encompassed degenerate cases, in this case where the vertex and one point defining a leg are the same.<ref>l8_5 in Narboux</ref>

One leg between two points on the perpendicular

There are a few cases which imply we are dealing with a degenerate is-right-angle. Here's one in which the point defining one leg is between two points which both lie on the perpendicular. Specifically, is-right-angle A B C ∧ is-right-angle A′ B C ∧ between A C A′ → B = C.<ref>l8_6 in Narboux</ref>

The proof first expands both occurrences of is-right-angle according to the definition to get points c′ and c″ for which (B is-midpoint-of C c′ ∧ A C ≡ A c′) ∧ (B is-midpoint-of C c″ ∧ A′ C ≡ A′ c″) ∧ between A C A′.

Then we apply SymmetricPointDistance to get C′ C″ ≡ C C, which in turn implies C′ = C″.

From here we get B is-midpoint-of C C by substituting C for C′, which in turn implies B = C.


We prove the builder for is-right-angle similarly to other builders: by applying builders for each of the expressions which make up the definition.<ref>not in Narboux</ref>


We now export to Interface:Orthogonality 1.



{{DEFAULTSORT:{{PAGENAME}}}} Category:Euclidean geometries (general) and generalizations Category:Foundations of classical theories (including reverse mathematics)

Login to edit