Proofs, pictures, and Euclid (Q707897): Difference between revisions

This is a presentation of the author's own version of \textit{Euclides vindicatus}, only in this view, \textit{ab omni naevo} refers to any flaws in the \textit{rigor} of its deductive logic, and not to an attempt to prove the Fifth Postulate. In a first part, the author presents the standard view that, in Euclid's proofs, diagrams ``would at best serve as a heuristic, illustrative device,'' and that ``his reliance on pictures in his arguments disqualifies them as rigorous proofs.'' Turning this widely held view on its head, the author argues, in the second and main part of this paper, for the centrality of diagrams in a certain rigorous proof system that mimics Euclid's reasoning, by introducing a formal system \(Eu\) in which diagrams play an active role. In the first part, the views of Proclus, Berkeley, Kant, Leibniz, and, in particular, of those instrumental in establishing the purified, diagram-free, view of the nature of rigorous proof, Frege (who demands and states ``and in this I go beyond Euclid -- that all modes of inference be specified in advance''), Pasch, Hilbert, and Klein, all of whom are ``explicit on the superiority of abstract axioms over diagrams.'' \(Eu\) is a heterogeneous system in that although it has a conventional sentential syntax, it also has a discrete diagram symbol type. It was introduced by the author in his dissertation [Intuition formalized: Ancient and modern methods of proof in elementary Euclidean geometry. Ph.D.\ Dissertation, Carnegie Mellon University (2006)], and was inspired by \textit{K. Manders} [``The Euclidean diagram'', in: P. Mancosu (ed.), The philosophy of mathematical practice. Oxford: Oxford University Press. 80--133 (2008; Zbl 1163.03001)], who has emphasized that both text and diagram have their roles in establishing a result in Euclid's \textit{Elements}. A related formal system has been presented by \textit{J. Avigad}, \textit{E. Dean}, and \textit{J. Mumma} [Rev. Symb. Log. 2, No.~4, 700--768 (2009; Zbl 1188.03008)].