In Euclidea, you don’t manipulate the proofs but unless you’re just brute-forcing the levels you have constructed a proof mentally. Similarly, if Euclidea is implemented correctly, it generates the proof internally and checks it (even if these stages are fused). I wouldn’t rely on a game for building large developments and indeed Euclidea lacks abstraction and modularity as far as I can tell but the same developer may have a freeform environment with these features. Euclidea is an activity that mentally scratches the same itch as proving and in the same or very similar theory to TFA.
No. A construction says what to draw; a proof says why you’ve drawn the right thing.
Say we want to find the midpoint M of AB. Construction:
“Draw the circle centered at A through B and the circle centered at B through A. Let the two circles meet at C, D. Let AB meet CD at M.”
Proof:
“Since AC = AB = BC, C lies on the perpendicular bisector of AB. Since AD = AB = BD, D lies on it as well. Hence CD is the perpendicular bisector of AB. That means AM = BM, so M is the midpoint of AB.”
In your example, let’s strip each statement of phrasing (“meet at” means the same as “intersect”, etc). Also, each requires external knowledge of the relationship between radii and right angles. These bits can presumably be reduced to the same clauses as well.
So. Is more information encoded in the proof than the construction?
Is one of two equivalent prolog programs just written upside down, while the other says “hence” a non-zero number of times??
My example was so simple that it would be taken as obvious for an experienced reader. With any nontrivial problem, the proof would have much more information than the construction. For example, the proof might require the construction of auxiliary objects not used in the main construction.
This is beautifully showcased by a 3Blue1Brown video about an extremely clever proof of the equivalence of three constructions of an ellipse: https://www.youtube.com/watch?v=pQa_tWZmlGs.
I’m not Godel, but my ad absurdum was meant to be slightly weirder than the objection that seems to have come across. I’ll try this way.
I had a flash of a question about whether the external information required in either case offsets the information provided by the objects in the proof (implicitly, explicitly, or artificially). I was thinking in terms of both formal logic and entropy, loosely.
The (usefully simple) construction here implies use of a compass or string. In a sense, the physical constraints of a compass encode the same information as the lemmas and theorems do abstractly.
“Brah, you should google metaphysics and Bertrand Russell,” is probably about right But, I’m sure there is a term that I just don’t know or can’t recall.
Perhaps an answer to one version of your question is that the Tarski–Seidenberg theorem implies that Euclidean geometry is decidable: there exists an algorithm that finds a proof for any theorem of Euclidean geometry. This algorithm, however, is too slow to be practical in general (double exponential time). The proofs it finds definitely don’t correspond one-to-one with the constructions in any reasonable sense.
The compass encodes a constant-radius constraint, and the string encodes a sum-of-distances constraint, but it’s not at all obvious why these two constraints turn out to be the same under a uniform stretching. There are plenty of similar-looking hypotheses that turn out to be false (for example, a curve of constant offset to an ellipse looks a lot like an ellipse but isn’t one).
