Is Euclid's Fourth Postulate Redundant? Euclid's Elements start with five Postulates, including the fifth one, the famous Parallel Postulate.  Less well, known however is the Postulate that forms the basis for motivation behind the fifth: the fourth one, which states that "all right angles are equal."  Students who see this for the first time might find this puzzling, because obviously two angles which are equal to a 90 degree angle are equal to each other, since Common Notion 1 says that "things which are equal to the same thing are are also equal to one another".  But then they realize that the matter is so straightforward: the definition of a right angle is an angle produced when two lines intersect each other and produce equal adjacent angles, and it's not clear why an angle produced by one such pair of lines should bear any relation to an angle produced by another such pair of lines.   
So Euclid's fourth Postulate is not redundant for the reason that beginning students might think.  But my question is, is it nevertheless a redundant postulate, although for far less trivial reasons?  David Hilbert, in his Foundations of Geometry (Grundlagen der Geometrie in German), claims to prove Euclid's fourth Postulate in theorem 15 (on page 19 of the PDF or page 13 according to the book's internal page numbering), prefacing the proof by saying "it is possible to deduce the following simple theorem, which Euclid held - although it seems to me wrongly - to be an axiom."
Now it's fair to say that Hilbert was working in a different (and more rigorous) system of axioms than Euclid was, but I think Hilbert's proof should be seriously considered for two reasons.  First of all, why would he dub Euclid's decision to call "all right angles are equal" a Postulate as "wrong" if it merely reflected a stylistic difference concerning what you choose as starting assumptions and what you consider theorems?  But more importantly, by tracing back all the assumptions used in the proof of theorem 15, it seems to me that only four of Hilbert's axioms are ultimately used: IV 3, IV 4, IV 5, and IV 6.  And I don't think Euclid would have objected to any of these statements:
IV 3 follows directly from Euclid's Common Notion 2.
IV 4 is partly stated in Euclid's Book I Proposition 23, which doesn't depend on the fourth postulate, and the part of IV 4 which (I think) is not stated is easily provable in Euclid's system.
IV 5 follows from Euclid's Common Notion 1.
IV 6 is just part of Euclid's Book I Proposition 4, which doesn't depend on the fourth postulate at all. 
So could Euclid have proven his fourth Postulate as a theorem instead of just assuming it?  
Any help would be greatly appreciated.
Thank You in Advance.
EDIT: It seems to me that the key idea driving Hilbert's proof is that Euclid's Book I Proposition 4, i.e. the Side-Angle-Side (SAS) congruence theorem, implies that the supplements of equal angles are equal.  Can anyone confirm or deny that this implication is in fact valid, and if it is valid, that the conclusion can be used to show that all right angles are equal?
 A: Euclid's right-angle postulate excludes the existence of cone points: right angles at the vertex of a cone are smaller than right angles elsewhere on the cone. So this postulate cannot be proved insofar as the other axioms apply on a cone, which one could argue that they do.
A: Yes, Euclid Fourth postulate can be derived from (a modern formalization of) the other postulates and common notions. Our axiomatization includes the five line axiom, which corresponds to SAS.
We have machine checked proof of this fact. This work is described in this paper: https://arxiv.org/abs/1710.00787
The formal proof of the Fourth postulate can found in this file:
https://github.com/GeoCoq/GeoCoq/blob/master/Elements/OriginalProofs/lemma_Euclid4.v
More readable proofs will come later.
A: It looks as though Euclid wanted to delay Proposition 22 (and hence Proposition 23) until after the Triangle Inequality (Proposition 20). Since Euclid's proof of the Triangle Inequality requires the fourth postulate, he couldn't use Proposition 23 to prove the postulate. [A superposition argument won't work, because it would require us to already know that the two right angles are equal.]
Hilbert could prove Euclid's fourth postulate using Proposition 23, since he took Proposition 23 as his axiom IV 4.
A: You've asked a very interesting question: Whether or not Euclid's 4th Postulate is independent of the other 4 postulates. It appears that the answer is in the affirmative. The argument for it is available online here:
"What’s the Deal with Euclid’s Fourth Postulate?"
"In February, I wrote about Euclid’s parallel postulate, the black sheep of the big, happy family of definitions, postulates, and axioms that make up the foundations of Euclidean geometry."
By Evelyn Lamb on April 21, 2014
"An illustration from Oliver Byrne's 1847 edition of Euclid's Elements. Euclid's fourth postulate states that all the right angles in this diagram are congruent. Image: Public domain, via Wikimedia Commons."
https://blogs.scientificamerican.com/roots-of-unity/whate28099s-the-deal-with-euclide28099s-fourth-postulate/
A: You've asked a very interesting question: Whether or not Euclid's 4th Postulate is independent of the other 4 postulates. It appears that the answer is in the affirmative (according to Evelyn Lamb's "Scientific American" article cited below). The argument for it is available online here:
"What’s the Deal with Euclid’s Fourth Postulate?"
"In February, I wrote about Euclid’s parallel postulate, the black sheep of the big, happy family of definitions, postulates, and axioms that make up the foundations of Euclidean geometry."
By Evelyn Lamb on April 21, 2014

"An illustration from Oliver Byrne's 1847 edition of Euclid's Elements. Euclid's fourth postulate states that all the right angles in this diagram are congruent. Image: Public domain, via Wikimedia Commons."
https://blogs.scientificamerican.com/roots-of-unity/whate28099s-the-deal-with-euclide28099s-fourth-postulate/
PS1: I think part of our Modern difficulty with this Postulate can be better understood in the context of our Theory of Equivalence Relations, which is inconsistent with the views of the Ancient Greek Mathematicians" X=X would be mere Incidence for the Greeks (Sameness). And X=Y is two equal things: think of a Balance Scale, the substance on the Left of the Scale, X, is Equal (in Weight) to the substance on the Right of the Balance Scale; in this instance, there is no Sameness. But the case of a Point(s) being Congruent with another Point(s) is nonsense since a Given point has a distinct Locus (Location) - no two points can be in the same place; so Congruence is an Anachronism we Moderns imposed on the Ancient Greeks.
PS2: My understanding of "All Right Angles are Equal" is to define Right Angles (Geometrical entities) by the Common Notion of Equality. I believe that Hilbert exhibits the Tyranny of the Majority. At the time that Hilbert presented his system of geometry (1899), France had been defeated, England was still devoted to Classical Ancient Greek Geometry, and so Germany dominated the world in Mathematics. So his idea of Primitive Terms (undefined) took hold. But there were and are other ways of reconstructing Euclid according to more modern standards. I suggest looking closely at his 23 Definitions, as well as his other book, "Euclid's Data."
PS3: The proof of this postulate is on page 95, Proposition 9.6, "Any two right angles are congruent to each other," by Robin Hartshorne, in his 2010 book, "Geometry: Euclid and Beyond." However, the proof apparently relies on the refined Hilbert Axioms. However, he also recognizes the observation of Hilbert, who cites Proclus:
"Note: Thus the congruence of all right angles can be proved and does not need to be taken as an axiom as Euclid did (Postulate 4). The idea of this proof already appears in Proclus."
PS4: The Proclus argument (proof): "Postulate IV. And that all right angles are equal to one another," is on pages 147-150, in the 1992 translation by Glenn R. Morrow, "Proclus A Commentary on the First Book of Euclid's Elements" (Princeton University Press).
PS5:  David Hilbert, on pages 20-21 of his Foundations of Geometry, 1971 translation by Leo Unger, has THEOREM 21. "All right angles are congruent to each other." And Hilbert further states in his Footnote 1 that the idea of the proof is in Proclus. Here's Hilbert's Footnote 1:
"The idea of the proof can be found as early as the commentator PROCLUS, who indeed, instead of Theorem 14 used the hypothesis that the construction of one right angle always yields another right angle, i.e., yields an angle that is equal to its supplementary angle."
No one has yet made any comment on the "Scientific American" Article, "What’s the Deal with Euclid’s Fourth Postulate," by Evelyn Lamb (April 21, 2014). She appears to say (informally) that Space may not necessarily be "Uniform," so Euclid's postulate asserts the uniformity of Space. Furthermore, she tells use that Einstein established the non-uniformity of physical space by asserting that such a space is distorted by the gravitational field in it.
It's available online here: https://blogs.scientificamerican.com/roots-of-unity/whate28099s-the-deal-with-euclide28099s-fourth-postulate/
