FOM: Re: Diagrams: Re: Geometric Reasoning

[Pat Hayes]

Dear Walter

>(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!

This is a fascinating topic, but I think it is really distinct from what
Joe Shipman calls 'visual proofs'. Joe (and others) are referring to the
use of diagrams of a particular subjectmatter playing a role in proofs
about that subjectmatter: hence, Euclidian diagrams in Euclidean geometry,
topologically morphable diagrams in proofs in Knot theory, etc..  But the
above is about the logical structure of the proofs themselves. These are
what might be called meta-diagrams, ie diagrams in the metalanguage of
proof theory.

I have a problem with calling these 'diagrams' at all. I too "see" proofs
in the ways you describe, and use this in teaching logic 101. But while the
relevant structures here can be displayed visually and can be usefully
'imaged' by we human thinkers, they are essentially algebraic.
Treestructures and graphs can be projected into R2, but they are profoundly
different in mathematical nature: they have no continuity, no natural
metrics, no dimensionality, etc.. They are 'diagrammatic' only in the very
limited sense of not being 'linear', ie not having a natural embedding into
the integers, and hence not traditionally thought of as 'text' in a
semiotic sense. But even this is misleading, since the 'natural' structure
of linguistic text more like a tree than a line, but one which is encoded
using familiar parsing conventions rather than a simple
structure-preserving mapping. These familiar encodings (eg as used by LISP)
suffice to straightforwardly encode arbitrary directed graphs as linear
strings in much the same way.

Best wishes

Pat Hayes

---------------------------------------------------------------------
IHMC, University of West Florida		(850)434 8903   home
11000 University Parkway			(850)474 2091   office
Pensacola,  FL 32514			(850)474 3023   fax
phayes at ai.uwf.edu
http://www.coginst.uwf.edu/~phayes