 Realizing this conception in a formal system of proof amounts, as in Shin  1994,  to specifying the syntax and semantics of diagrams. On the syntactic side, this means defining Euclid’s diagrams as formal objects precisely, and giving rules whereby diagrams as formal object figure in derivations of Euclid’s propositions. On the semantic side, this means specifying how derivable expressions are to be interpreted geometrically, or in other words how exactly are they to be understood as representing Euclid’s propositions.