Recent philosophical studies of visualization and diagrammatic reasoning in mathematics suggest that psychological data and cognitive models may have a role to play in the philosophy of mathematics. While not wishing to discourage interaction between psychology and the philosophy of mathematics, I will inject a note of caution. In particular, I will argue that it is often possible to tease apart logical and cognitive issues, and that one should strive to do so, in the absence of overriding reasons not to.
I will illustrate by describing joint work with Ed Dean and John Mumma which aims to give a formal characterization of the logical structure of proofs in Euclid's *Elements*. Our system allows both diagram- and text-based inferences, providing a representation of Euclidean reasoning that is much more faithful to the *Elements* than modern axiomatic formulations. I will show how the system informs our understanding of diagrammatic reasoning, while maintaining a distinction between logical and cognitive analysis.