4 ms·

would it be possible to rewrite Euclid's Elements with a proof assistent like Coq?

by mjfl 9y ago

sanxiyn 9y ago
Yes, and it has been done: http://geocoq.github.io/GeoCoq/ http://geocoq.github.io/GeoCoq/ This is actually seriously non-trivial, because Euclid isn't rigorous enough for Coq. For example, you need definition of betweenness and Pasch's axiom at the very least.
- mjfl 9y ago
  neat!
simplicio 9y ago
Euclids rigor was remarkable for 300 BC, but its not really what we think of as rigorous now. Even the first theorm has several fairly obvious flaws (as the linked commentary points out). So you probably wouldn't have much Euclid left if you tried to make a machine checked version of Euclid. Many people post-300BC have done more rigorous treatments of plane geometry. Most famously Hilbert, who had (IIRC) 21 axioms.
thaumasiotes 9y ago
We don't even understand some of the things Euclid was trying to say. One of his postulates is "all right angles are equal". How do you recognize two angles as "right" other than by measuring their equality?
- Koshkin 9y ago
  To me, the postulate does make sense: right(a) & right(b) => a = b vs. acute(a) & acute(b) => ?
  - thaumasiotes 9y ago
    How can you define a "right angle" in a way that doesn't let you immediately prove that any two right angles are equal? Euclid did -- if he could have proved it, "all right angles are equal" would be a theorem, not a postulate. Similarly, how are you distinguishing "right" angles from "acute" angles?
    - Koshkin 9y ago
      Actually, the equality is part of Euclid's definition of the right angle: ῞Οταν δὲ εὐθεῖα ἐπ᾿ εὐθεῖαν σταθεῖσα τὰς ἐφεξῆς γωνίας ἴσας ἀλλήλαις ποιῇ, ὀρθὴ ἑκατέρα τῶν ἴσων γωνιῶν ἐστι, καὶ ἡ ἐφεστηκυῖα εὐθεῖα κάθετος καλεῖται, ἐφ᾿ ἣν ἐφέστηκεν. On the other hand, there is nothing wrong with leaving the property of an angle being 'right' undefined and postulating that all angles that possess this property are equal. (The notion of acuteness requires the ability to compare angles; those 'smaller' than the right angle are 'acute'.)
      - thaumasiotes 9y ago
        > there is nothing wrong with leaving the property of an angle being 'right' undefined and postulating that all angles that possess this property are equal Yes there is; it makes the postulate completely useless. Stating "all angles possessing a certain property which cannot be assessed are equal to each other" is useless, identical to declaring "any two equal angles are equal". Actually -- are there proofs in the Elements which invoke that postulate?
        Koshkin 9y ago
        Well, in a theory based on axioms some notions must be left undefined (which does not make them useless), so why not the notion of the right angle?
        thaumasiotes 9y ago
        Because then you have no way of identifying right angles. That leaves you with a claim you can make about right angles, and no angles you can ever apply the claim to. That is the same as not having the claim at all. Consider this modified classic syllogism: 1. All men are mortal. 2. No one can ever know whether any particular object is or isn't a man. 3. Therefore, Socrates is mortal. See the problem? It may still be possible to prove that Socrates is mortal, but you can't prove that or anything else with the postulate "all men are mortal", because that postulate, by hypothesis, doesn't apply to anything.
- schoen 9y ago
  Euclid was working in a context of classical geometric construction with compass and straightedge. If you have a line and a point not on the line, you can classically construct a perpendicular through the point. Use a compass centered on the given point, open to an arbitrary radius greater than the distance between the given point and the line. Draw a circle, which will intersect the line at two points A and B. Now draw a second circle centered on A and passing through B, and a third circle centered on B and passing through A. The second and third circles intersect in two points, C and D, one on each side of the given line. Draw a new line through C and D. This line is perpendicular to the original line and forms four right angles with it. A way to check whether a given angle is right is to pick an arbitrary point on one of the lines and draw a circle centered there and passing through an arbitrary point on the other line. The circle will then pass through a second point on the other line. You can construct the perpendicular bisector of the segment formed by the two points in which the circle intersects the second line, and see whether the bisector is identical to the first line. (Although I'm not sure that's the right classical solution because I don't recall whether "noticing whether two constructed lines are identical" or "noticing whether a constructed line intersects a given point" are allowed tasks in classical construction.)
  - thaumasiotes 9y ago
    > [...] Draw a new line through C and D. This line is perpendicular to the original line and forms four right angles with it. You could define a right angle this way, but that only makes sense if "right angles" were already interesting before you worked out how to construct them. That process is valuable because it produces right angles; right angles aren't valuable by virtue of being the result of that process. If you believe that, you still need to ask why certain angles were labeled "right", bearing in mind that whatever the reason was, it cannot have implied that two "right" angles were necessarily equal to each other.
    - schoen 9y ago
      It seems like they have tons of meaning in terms of squares, parallel lines, and many parts of triangle geometry, including the Pythagorean theorem and the angle sum in a triangle being two rights angles.

would it be possible to rewrite Euclid's Elements with a proof assistent like Coq?

by mjfl 9y ago

would it be possible to rewrite Euclid's Elements with a proof assistent like Coq?

Yes, and it has been done: http://geocoq.github.io/GeoCoq/ http://geocoq.github.io/GeoCoq/ This is actually seriously non-trivial, because Euclid isn't rigorous enough for Coq. For example, you need definition of betweenness and Pasch's axiom at the very least.

mjfl 9y ago
neat!

simplicio 9y ago

Euclids rigor was remarkable for 300 BC, but its not really what we think of as rigorous now. Even the first theorm has several fairly obvious flaws (as the linked commentary points out). So you probably wouldn't have much Euclid left if you tried to make a machine checked version of Euclid. Many people post-300BC have done more rigorous treatments of plane geometry. Most famously Hilbert, who had (IIRC) 21 axioms.

thaumasiotes 9y ago

We don't even understand some of the things Euclid was trying to say. One of his postulates is "all right angles are equal". How do you recognize two angles as "right" other than by measuring their equality?

Koshkin 9y ago
To me, the postulate does make sense: right(a) & right(b) => a = b vs. acute(a) & acute(b) => ?
- thaumasiotes 9y ago
  How can you define a "right angle" in a way that doesn't let you immediately prove that any two right angles are equal? Euclid did -- if he could have proved it, "all right angles are equal" would be a theorem, not a postulate. Similarly, how are you distinguishing "right" angles from "acute" angles?
  - Koshkin 9y ago
    Actually, the equality is part of Euclid's definition of the right angle: ῞Οταν δὲ εὐθεῖα ἐπ᾿ εὐθεῖαν σταθεῖσα τὰς ἐφεξῆς γωνίας ἴσας ἀλλήλαις ποιῇ, ὀρθὴ ἑκατέρα τῶν ἴσων γωνιῶν ἐστι, καὶ ἡ ἐφεστηκυῖα εὐθεῖα κάθετος καλεῖται, ἐφ᾿ ἣν ἐφέστηκεν. On the other hand, there is nothing wrong with leaving the property of an angle being 'right' undefined and postulating that all angles that possess this property are equal. (The notion of acuteness requires the ability to compare angles; those 'smaller' than the right angle are 'acute'.)
    - thaumasiotes 9y ago
      > there is nothing wrong with leaving the property of an angle being 'right' undefined and postulating that all angles that possess this property are equal Yes there is; it makes the postulate completely useless. Stating "all angles possessing a certain property which cannot be assessed are equal to each other" is useless, identical to declaring "any two equal angles are equal". Actually -- are there proofs in the Elements which invoke that postulate?
      - Koshkin 9y ago
        Well, in a theory based on axioms some notions must be left undefined (which does not make them useless), so why not the notion of the right angle?
        thaumasiotes 9y ago
        Because then you have no way of identifying right angles. That leaves you with a claim you can make about right angles, and no angles you can ever apply the claim to. That is the same as not having the claim at all. Consider this modified classic syllogism: 1. All men are mortal. 2. No one can ever know whether any particular object is or isn't a man. 3. Therefore, Socrates is mortal. See the problem? It may still be possible to prove that Socrates is mortal, but you can't prove that or anything else with the postulate "all men are mortal", because that postulate, by hypothesis, doesn't apply to anything.
schoen 9y ago
Euclid was working in a context of classical geometric construction with compass and straightedge. If you have a line and a point not on the line, you can classically construct a perpendicular through the point. Use a compass centered on the given point, open to an arbitrary radius greater than the distance between the given point and the line. Draw a circle, which will intersect the line at two points A and B. Now draw a second circle centered on A and passing through B, and a third circle centered on B and passing through A. The second and third circles intersect in two points, C and D, one on each side of the given line. Draw a new line through C and D. This line is perpendicular to the original line and forms four right angles with it. A way to check whether a given angle is right is to pick an arbitrary point on one of the lines and draw a circle centered there and passing through an arbitrary point on the other line. The circle will then pass through a second point on the other line. You can construct the perpendicular bisector of the segment formed by the two points in which the circle intersects the second line, and see whether the bisector is identical to the first line. (Although I'm not sure that's the right classical solution because I don't recall whether "noticing whether two constructed lines are identical" or "noticing whether a constructed line intersects a given point" are allowed tasks in classical construction.)
- thaumasiotes 9y ago
  > [...] Draw a new line through C and D. This line is perpendicular to the original line and forms four right angles with it. You could define a right angle this way, but that only makes sense if "right angles" were already interesting before you worked out how to construct them. That process is valuable because it produces right angles; right angles aren't valuable by virtue of being the result of that process. If you believe that, you still need to ask why certain angles were labeled "right", bearing in mind that whatever the reason was, it cannot have implied that two "right" angles were necessarily equal to each other.
  - schoen 9y ago
    It seems like they have tons of meaning in terms of squares, parallel lines, and many parts of triangle geometry, including the Pythagorean theorem and the angle sum in a triangle being two rights angles.