Talk:Construction of Triangle from Given Lengths

This proof can't truly be completed using just Euclid's axioms, but then again, neither can Construction of Equilateral Triangle. Basically, circles are woefully underspecified in the system. However, if we assume the following additional postulate, everything works out:

Let $A$ be a circle, and $B$ a line (either straight or curve). Suppose some point in $B$ is inside $A$, and another is outside. Then $A$ and $B$ intersect.

From a formal point of view, this is a consequence of Jordan Curve Theorem; the inside and outside of a circle are not path-connected. For this proof, it's probably fine to use this principle implicitly, and just show that some point is inside and another is outside, intuitively justifying the conclusion.

For the special case of circles, with a more rigorous axiomatization, such as Axiom:Hilbert's Axioms or Axiom:Birkhoff's Axioms, we would use a principle of continuity. For example, we can parameterize one of the circles, and measure the distance to the center of the other. Since it varies continuously, we can apply the Intermediate Value Theorem to find a point where they intersect. Of course, there are a lot of details to work out (we would probably need to construct a projection from a line onto the circle in order to use the concept of "parameterization"), but it could definitely be done.

Any feedback on what to do here? --CircuitCraft (talk) 19:59, 7 September 2023 (UTC)

Find the sources which have done the work needed to add these minor points of rigor and detail, then set up a metastructure in $\mathsf{Pr} \infty \mathsf{fWiki}$ to handle axiom schemata that are effectively extensions of Euclid's axioms and definitions and whatever else is missing. I know it's out there, just haven't been all that motivated to hunt it down. --prime mover (talk) 22:13, 7 September 2023 (UTC)