Call for geometry reference
84 views
Skip to first unread message
Florin Vasiliu
Mar 5, 2020, 12:50:02 PM3/5/20
to Calculational Mathematics
Dear calculational community,
The topic is geometry, for which, in my case, fascination was kept alive by this circle's writings: the elegant, well-phrased proofs for the theorems of Ceva, Pompeiu, Morley (especially in EWD1266a), and Sylvester; the construction of the regular pentagon, with heuristics (WF83); the analysis of alternative proofs for the existence of the Euler line ("On the Shape of Mathematical Arguments").
However, I feel my understanding of —even elementary, Euclidean— geometry is still built on sand. For this reason, I ask, if you could please share, whether you have encountered any axiomatic development (textbook, article) at least close to calculational standards of rigour. As a computing undergraduate —willing to spare much time for the geometric track as well— I wish to obtain a basis for critical reading of Coxeter or, say, the book on machine proofs by Shang-Ching Chou et al. (possibly an inspiration for prof. Dijkstra's beautiful triangle calculus experiment). Frustrating experiences so far include Hartshorne's and Moise's texts, but I would keep ploughing through them on suggestion of the more competent.
Thank you for considering this!
Best regards,
Florin Vasiliu
Greetings!
I address you with a kind request, if you can help. A main interest of mine, shared by many of you I believe, is lending contribution in establishing firmer, cleaner foundations —and, ultimately, calculational expositions— for various branches of mathematics.The topic is geometry, for which, in my case, fascination was kept alive by this circle's writings: the elegant, well-phrased proofs for the theorems of Ceva, Pompeiu, Morley (especially in EWD1266a), and Sylvester; the construction of the regular pentagon, with heuristics (WF83); the analysis of alternative proofs for the existence of the Euler line ("On the Shape of Mathematical Arguments").
However, I feel my understanding of —even elementary, Euclidean— geometry is still built on sand. For this reason, I ask, if you could please share, whether you have encountered any axiomatic development (textbook, article) at least close to calculational standards of rigour. As a computing undergraduate —willing to spare much time for the geometric track as well— I wish to obtain a basis for critical reading of Coxeter or, say, the book on machine proofs by Shang-Ching Chou et al. (possibly an inspiration for prof. Dijkstra's beautiful triangle calculus experiment). Frustrating experiences so far include Hartshorne's and Moise's texts, but I would keep ploughing through them on suggestion of the more competent.
Thank you for considering this!
Best regards,
Florin Vasiliu
Lucas Brunno Luna
Mar 6, 2020, 11:06:37 AM3/6/20
to Calculational Mathematics
Dear Florin,
Some time ago I also took an interest in the subject of a firm foundation for Euclidean Geometry that would allow for a rigorous calculational development of the theory. Alfred Tarski et al. seem to have taken substantial steps in that direction. Although my familiarity with their work is still very superficial, it does seem quite promising.
This paper might serve as an introduction: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.9012
The above paper points out a distinction between first- and second-order theories, though I admit that I myself am quite ignorant of the relevance, and whether we should bother. Perhaps you or some other member of this group could enlighten me on this subject.
I also intend to have a look at a collection of essays by various authors, including Tarski, entitled "The axiomatic method. With special reference to geometry and physics" from Studies in Logic and the Foundations of Mathematics. They might be of your interest as well. I found a scanned version at the Internet Archive (under the title "The Axiomatic Method"), but I can't tell whether it's legal...
Goodbye for now, and feel free to share whatever progress you make in this area.
Some time ago I also took an interest in the subject of a firm foundation for Euclidean Geometry that would allow for a rigorous calculational development of the theory. Alfred Tarski et al. seem to have taken substantial steps in that direction. Although my familiarity with their work is still very superficial, it does seem quite promising.
This paper might serve as an introduction: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.9012
The above paper points out a distinction between first- and second-order theories, though I admit that I myself am quite ignorant of the relevance, and whether we should bother. Perhaps you or some other member of this group could enlighten me on this subject.
I also intend to have a look at a collection of essays by various authors, including Tarski, entitled "The axiomatic method. With special reference to geometry and physics" from Studies in Logic and the Foundations of Mathematics. They might be of your interest as well. I found a scanned version at the Internet Archive (under the title "The Axiomatic Method"), but I can't tell whether it's legal...
Goodbye for now, and feel free to share whatever progress you make in this area.
Jeremy Weissmann
Mar 6, 2020, 11:44:14 AM3/6/20
to mathmeth
Dear Florin,
Calculational approaches to a subject are fine, but one should be warned that if one insists only on a calculational approach from the start, one will likely not get very far.
Have a look at the first few pages of EWD1123, "The unification of three calculi" . Notice the step on page 2 where Dijkstra re-axiomatizes his formalism. This is a good example of how calculational frameworks can arise: there has to be some understanding of what are the right concepts to formalize, whether the properties which describe the concepts lend themselves well to a calculational framework.
When I was in the Netherlands, working on (among other things) graph theory with Wim Feijen and others, I was able to make some headway here and there formalizing various aspects of graph theory, but came very far from a complete from a unified calculational framework. Indeed, no such framework may be possible or desirable. My finest algorithmic design in graph theory (admittedly a simple theorem) is presented in JAW17, which was my first exercise in top-down algorithm design. I have yet to discover a way that formalism could improve the design.
Similarly, Wim Feijen has some nice WFs (WF147 & 148) about needing both Predicate Calculus and the Relational Calculus, even though each can theoretically be phrased in terms of the other and hence dispensed with.
The moral of the story being: first focus on discipline in thought. Proceed thoughfully as you progress. Don't make unnecessary distinctions. Seek opportunities to generalize and abstract where you can. And when formalism can present itself, experiment with it!
But, first and foremost, ground yourself in clean, elegant expositions of the field. For geometry, you could start with any decent high school text, like:
Geometry for Enjoyment and Challenge
or:
Kiselev's Geometry
When you start to experiment, let us know what you come up with!
+j
--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/92b0b4f4-4613-4c0c-ac1a-e4c9be2924ee%40googlegroups.com.
Florin Vasiliu
Mar 7, 2020, 3:45:49 AM3/7/20
to Calculational Mathematics
My thanks to both individuals for your thoughtful answers and comments!
To Mr. Luna:
The letter from Tarski and Givant looks very much like what I was hoping to receive when I issued my request. The collection of writings on axiomatic method certainly seems a treasure trove as well. Thank you for your openness in sharing these! (They are not casual reading however, so it may be a while before I've studied enough to get back to you.)
To Mr. Weissmann:
I am indeed a bit of an extreme formalist; perhaps it's due to a, yet unpursued, ideal of mine with respect to automated checking and proving. My use of the word "calculational" refers to employing formal notation with complete disregard to meaning, only taking into account a repertoire of manipulations. I understand this perspective may not lend itself well to shaping the foundation of a field; your remark about this is beneficial to me. But even considering the potential undesirability for complete formalization in the case of geometry, most elementary treatments have much to improve with respect to disregarding meaning, especially in the reliance on diagrams for extracting implicit assumptions, based on "our intuition of space". An unsatisfactory, yet —via standard axiomatizations— unavoidable, appeal to a picture is exposed in EWD975.
With regard to EWD1123, I perceive that such a precise yet brief presentation of the predicate calculus is only possible after abstracting away from the underlying space, with its named variables —this latter step being reflected in the introduction of the everywhere operator, and crucial in the context of dealing with predicate transformers—. I gather the proper calculational framework arises at this higher level, with its associated, abstract "structure" type.
I shall definitely study your note JAW17 and re-read through my Kiselev as well. Thank you for all your insightful comments and recommendations! They are extremely valuable to me, especially as coming from someone much more experienced in these matters. I shall also follow the guidelines you have set ("moral of the story" paragraph) in my further reading and report back later.
Best regards,
Florin Vasiliu
To Mr. Luna:
The letter from Tarski and Givant looks very much like what I was hoping to receive when I issued my request. The collection of writings on axiomatic method certainly seems a treasure trove as well. Thank you for your openness in sharing these! (They are not casual reading however, so it may be a while before I've studied enough to get back to you.)
To Mr. Weissmann:
I am indeed a bit of an extreme formalist; perhaps it's due to a, yet unpursued, ideal of mine with respect to automated checking and proving. My use of the word "calculational" refers to employing formal notation with complete disregard to meaning, only taking into account a repertoire of manipulations. I understand this perspective may not lend itself well to shaping the foundation of a field; your remark about this is beneficial to me. But even considering the potential undesirability for complete formalization in the case of geometry, most elementary treatments have much to improve with respect to disregarding meaning, especially in the reliance on diagrams for extracting implicit assumptions, based on "our intuition of space". An unsatisfactory, yet —via standard axiomatizations— unavoidable, appeal to a picture is exposed in EWD975.
With regard to EWD1123, I perceive that such a precise yet brief presentation of the predicate calculus is only possible after abstracting away from the underlying space, with its named variables —this latter step being reflected in the introduction of the everywhere operator, and crucial in the context of dealing with predicate transformers—. I gather the proper calculational framework arises at this higher level, with its associated, abstract "structure" type.
I shall definitely study your note JAW17 and re-read through my Kiselev as well. Thank you for all your insightful comments and recommendations! They are extremely valuable to me, especially as coming from someone much more experienced in these matters. I shall also follow the guidelines you have set ("moral of the story" paragraph) in my further reading and report back later.
Best regards,
Florin Vasiliu
Jeremy Weissmann
Mar 7, 2020, 8:12:54 AM3/7/20
to calculationa...@googlegroups.com
Dear Florin,
Thank you for your response. To clarify, I am a huge fan of calculation to work in mathematics. Just as I am a huge fan of using mathematics to study the world. However, it is important to recognize that simply using a tool is not enough: one has to use it well.
I can use mathematics to study love, quantifying as much as I can with numbers, say. But I don’t think that will get me very far. That’s not to say I can’t think closely and rationally about love, be organized, etc. I don’t simply have to throw it all to the wind. But the extreme abstractions of mathematics I don’t think are helpful.
Analogously, within mathematics, I want to use formalism for all the reasons we love (greater abstraction and clarity, the possibility of syntactic analysis to drive proof design, etc), but one has to recognize where it may not be appropriate. Even where it is appropriate, the question of how to formalize is a great intellectual act. That was my point of leading you to the EWDs and WFs. Almost everyone uses some sort of formalism to study logic, but the framework designed by Dijkstra and others took years to come to fruition, and the beauty and flexibility of that system shows the result of those years of careful thinking. It doesn’t suffice to just write down some symbols — not if you actually want to USE your formalism to calculate.
I have read many of Dijkstra’s experiments in geometry, admittedly many years ago. There is something there but they are far from encouraging. Similarly with other axiomatic approaches to geometry. If the goal is to streamline mathematical thought they haven’t gotten there yet! The amount of careful analysis and invention needed to prove simple theorems is tremendous. Does that mean the whole project is useless? No. It does mean that one has to keep going back to the original concepts and consider them, refine them, generalize them, and find the right patterns to pick out and try to subject to formalism. Towards that end, it is important to study really clean conceptual expositions of the field.
Looking forward to seeing your own experiments in geometry!
+j
PS. You reminded me that when I taught geometry I did use calculations to prove various things about angle and triangle congruence, parallel lines, etc.
On Mar 7, 2020, at 03:45, Florin Vasiliu <florinv...@gmail.com> wrote:
--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/ef29b90f-42f3-4efb-b953-1f07d116fbee%40googlegroups.com.
Jeremy Weissmann
Mar 7, 2020, 8:19:16 AM3/7/20
to calculationa...@googlegroups.com
Incidentally, EWD975 is a good example of what I’m talking about. It’s one of my favorite EWDs, but this is not calculational geometry!! Yes, there are some numbers and symbols, but the proof and argumentation are mostly conceptual. The reasoning is careful and considered, and very well-organized. But this is not a reflection of formalizing an area of mathematics and then calculating.
And with respect to EWD1123, my point is that the step where Dijkstra introduces the everywhere operator reflects a development that took years. Yes, he does it in a couple of lines, but coming up with a fortuitous calculational framework will take years to design.
+j
On Mar 7, 2020, at 03:45, Florin Vasiliu <florinv...@gmail.com> wrote:
--
Florin Vasiliu
Mar 8, 2020, 7:35:43 AM3/8/20
to Calculational Mathematics
Dear Mr. Weissmann,
Thank you for taking the time to further elaborate. Don't worry, I am aware I could not possibly propose a thought-streamlining formalism without first attaining a thorough conceptual grasp of the subject. And I do not underestimate the effort and ingenuity involved in the process. I'm sorry for the misunderstanding about EWD975; I mentioned it not as an example of calculational geometry, but as evidence that there is work to be done in improving foundations. All this considered, I think you can understand my interest even in weak formalisms —with regard to their power in delivering effective proofs—. They constitute a —perhaps not promising, yes— starting point and I think knowledge of these is helpful in seeing what can go wrong and stimulating a remedy. Keep in mind as well, high-school wasn't so long ago for me: I haven't already forgotten all of the basics, as taught in textbooks.
Regards,
Florin Vasiliu
Thank you for taking the time to further elaborate. Don't worry, I am aware I could not possibly propose a thought-streamlining formalism without first attaining a thorough conceptual grasp of the subject. And I do not underestimate the effort and ingenuity involved in the process. I'm sorry for the misunderstanding about EWD975; I mentioned it not as an example of calculational geometry, but as evidence that there is work to be done in improving foundations. All this considered, I think you can understand my interest even in weak formalisms —with regard to their power in delivering effective proofs—. They constitute a —perhaps not promising, yes— starting point and I think knowledge of these is helpful in seeing what can go wrong and stimulating a remedy. Keep in mind as well, high-school wasn't so long ago for me: I haven't already forgotten all of the basics, as taught in textbooks.
Regards,
Florin Vasiliu
Jeremy Weissmann
Mar 8, 2020, 7:52:02 AM3/8/20
to calculationa...@googlegroups.com
But I thought you said the basics felt on shaky ground! Maybe I was confused...
On Mar 8, 2020, at 07:35, Florin Vasiliu <florinv...@gmail.com> wrote:
--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/87d7699c-92d3-4904-b6a3-d168ed08d55a%40googlegroups.com.
Florin Vasiliu
Mar 8, 2020, 8:39:34 AM3/8/20
to Calculational Mathematics
Yes, it's my fault for not adding another sentence: the basics feel on shaky ground in spite of all the resources I've studied thus far. This mainly because of implicit appeals to diagrams and other unjustified assumptions. The "calculational standard of rigour" was my way to express an ideal of clarity and explicitness, whether completely formal or not. I apologize for prolonging the confusion (and filling people's inboxes, in case they weren't interested).
Jeremy Weissmann
Mar 8, 2020, 10:00:43 AM3/8/20
to calculationa...@googlegroups.com
What were your elementary geometry texts?
On Mar 8, 2020, at 08:39, Florin Vasiliu <florinv...@gmail.com> wrote:
Yes, it's my fault for not adding another sentence: the basics feel on shaky ground in spite of all the resources I've studied thus far. This mainly because of implicit appeals to diagrams and other unjustified assumptions. The "calculational standard of rigour" was my way to express an ideal of clarity and explicitness, whether completely formal or not. I apologize for prolonging the confusion (and filling people's inboxes, in case they weren't interested).
--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/50366470-493b-451f-a09c-647c235afc80%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages