FOM: Geometric Reasoning

[Walter Whiteley]

I have a number of reactions to the ongoing exchanges on geometric
/ diagrammatic reasoning (which I am just catching up on).  I was trained
in logic (see below) but my major work these days is in discrete applied
geometries (what shape of buildings are rigid, correct pictures of 3-D
polyhedra, programming for CAD,  computer aided geometric design, ... ).
I have also participated in several workshops on 'diagrammatic reasoning' and
discuss the issues regularly with my mathematics students.

I will separate my comments out into two messages.

(a)   One issue is the relative complexity of solving specific problems
in various forms of geometry.  While not immediately identical to the
split between first-order proofs with formula and diagrammatic proofs,
I have, for about 30 years, considered the split between analytic and synthetic
geometry and translating formulae from one form to the other.  [To me, that
was one of the root questions in classical invariant theory.  At least till the
algebraists moved in and declared it 'dead'.  History has finally proven
them wrong.]

A couple of papers on this are:
B. Sturmfels and W. Whiteley:  Synthetic factoring of invariant computations;
   J. Symbolic Computation 11 (1991), 439-453.
   [Giving an algorithmic translation from analytic to synthetic geometry
    for projective geometric statements - basically translating the
    fundamental theorem of projective geometry.  Points out the complexity
    of general translations.  Gives a specific example of a relatively simple
    property in analytic geometry - 10 points on a quadric in 3-space -
    and the absence of any meaningful translation into synthetic geometry
    - the search for a 3-D analog of Pascal's Theorem.  This is an unsolved
    problem posed around the 1810s.  Tackled, implicitly, by people like
    Turnbull and Young (of Young tableau fame)]
W. Whiteley:  Invariant theory and computations in symbolic analytic geometry,
    J. Symbolic Computation 11 (1991), 549-578.
    [Describing standard forms for proofs of invariant formula - theorems of
    projective geometry -  via standard form metatheorems about 
    first-order proofs from specific axioms systems, including Hilbert's 
    Nullstellensatz and the RealStellensatz which are derived by 
    partial cut-elimination.]
W. Whiteley: Analytic vs synthetic geometry for computers,  Learning and
   Geometry:   Computational Approaches, D. Kueker and C. Smith (eds.),
   Birkhauser 1996, 121-141

>From those studies, it is clear that the translation process can take a simple
statement to a very complex statement.  One of the situations being examined
was the 'automated theorem provers' for elementary geometry, which have the
capacity to generate certain non-degeneracy-type additional assumptions when
the initial statement of the proposed theorem is incomplete.  A problem with
this is that the additional assumptions are in analytic form, even if the
original statements were in synthetic projective form.  An issue is:
how to transfer the assumptions back into the synthetic domain?

(b)  When I have done proof theory, my basic set-up is 'diagrammatic'.
>From my training in natural logic (a la Solomon Feferman, one of my teachers)
I think of proofs as trees, with axioms at the leaves and rules at the
branching.   I 'see' the structure of a proof in this form, and study
things like cut-elimination as a way to get the branching done at the top,
channel into a Herbrand formula, then follow the trunk of quantifier rules
down to the ground - the desired conclusion (in appropriate form).
I wonder how many people have an 'image' of a formal proof which is used,
informally and diagrammatically, in our analysis of these things.
On another occasion, I have described 'trees' as diagrams in one and a half
dimensions.  Not truly 2-dimensional - but not reasonably displayed in
one dimension.

Similarly, the 'structured proofs' in some other systems, particularly as
promoted by Leslie Lamport, based on 'structured programming' use lots
of visual clues to help us organize the reading of the proof
(and the writing of the proof). For those of us who have taught
computer scientists to crank out their formal proofs, it is evident
that formal logic, as used, is a highly visual subject!

(c)  In some studies a few years ago with an undergraduate student,
we concluded that, for reasoning with more that four, maybe five sets,
Venn diagrams are 'unreasonable': not something you would actually reason with.
This is related to the 'error' in some of the formal studies of Venn Diagrams,
where the rule:  'take a Venn diagram and erase a curve' is either subject
to extremely subtle, almost invisible assumptions, or is wrong.  In a general
Venn diagram, with large numbers of curves, there are only a few
curves which can be removed and still leave a Venn Diagram in the formal
sense.  (The proof of this uses the Jordon curve theorem etc.)

If you actually want to reason in a diagrammatic way about these situations, a
binary tree, and further annotation, works better that the typical
Venn Diagram (with further annotation for quantifiers).

(d)  It is interesting, from the point of view of teaching, learning and
practice, how widely computer scientists use various types of diagrams.
The typical computer science text has far more diagrams than the typical
math text!  Computer scientists are developing increasing numbers of visual
tools. Not because they do something a text cannot do, but because they help us
think / problem solve etc. in a different way.  [In some settings, with
areas like time critical safety systems, they will have two screens up
simultaneously, on for text and one visual.  Whatever is done in one is
immediately transferred to the other.  You choose where to work at any
given point in the design and specification.]

(e)  I think there actually are more 'images' going on in math, but the
tradition has been to excise them from the public discourse, and not up
to the proper standards of rigor.  At the least, this is terrible pedagogy.
Teachers have the image to organize what they write, and the student
stares at the strange sequence of formulas
and wonders:  where did this come from!

It is also misrepresents how mathematicians, in general, solve problems.
The book of Hadamard, recently reissued by Princeton University Press, as:
    Jacques Hadamard  The Mathematician's Mind:  The psychology of
    Invention in the Mathematical Field. Princeton Science Library
    Princeton University Press (Reissued with new preface 1996)
is an important description of the role of the image in developing central
mathematical 'insights' (a visual word!).   'Theorem' has the same root
as 'theater'.  It relates fundamentally to what we 'see'!

In the next message I will comment on how (some) practicing geometers
use diagrams, and on an very important, and new, type of diagram:
the dynamic diagram.

Walter Whiteley
Discrete Geometer
York University
Toronto Ontario