I came across this tidbit on the
Lambda the Ultimate website. It's a pointer to a juicy
paper by some Carnegie Mellon folks.
Abstract. We present a formal system, E, which provides a faithful model of the proofs in Euclid’s Elements, including the use of diagrammatic reasoning.
"Diagrammatic reasoning" is the interesting part. People have recognized the Elements as an exemplar of rigorous reasoning for many centuries, but it took some time for the question to emerge, "are the diagrams a necessary component of the logical argument?" Liebniz believed they were not:
...it is not the figures which furnish the proof with geometers, though the style of the exposition may make you think so. The force of the demonstration is independent of the figure drawn, which is drawn only to facilitate the knowledge of our meaning, and to fix the attention; it is the universal propositions, i.e. the definitions, axioms, and theorems already demonstrated, which make the reasoning, and which would sustain it though the figure were not there.
The authors note that "there is no [historical] chain linking our contemporary diagrams with the ones that Euclid actually drew; it is likely that, over the years, diagrams were often reconstructed from the text". Their abstract seems to say that the design of E recognizes some essential role for the diagrams, so I assume one must exist. I haven't finished reading the paper yet. But the whole thing is very interesting.
No comments:
Post a Comment