FOM: geometrical reasoning

[Stephen G Simpson]

Many thanks to Jerry Seligman for his posting of 25 Feb 1999 17:34:17,
where he discusses structural features of diagrammatic proofs which
seem to make them look quite different from sentential (i.e. predicate
calculus) proofs.  I now have a copy of the Allwein/Barwise book
`Logical Reasoning with Diagrams' and it's obvious that a lot of
sophisticated research is going on here.

 > There is no general theory of diagram syntax and semantics, so it is
 > difficult to raise any of the above observations to the status of
 > theorems, or to see exactly what would have to be done to show that
 > diagrammatic proofs are all reducible to sentential proofs. 

Are there any candidates for diagrammatic proofs that might be
provably *not* reducible to sentential proofs, in *some* interesting
sense?

It seems that all diagrammatic proofs are reducible to sentential
proofs in at least a crude sense, because all `diagrammatic theorems'
(does this have a precise meaning?) seem to be expressible as
sentences of Tarski's elementary geometry, and Tarski's elementary
geometry is complete.  So at least there is always a sentential proof
of the same theorem, right?  

Whether there is always a sentential proof that (in some sense)
corresponds closely to the diagrammatic proof is another question, or
set of questions.  Perhaps one of Harvey's systems of `diagrammatic
elementary geometry' (my name for it) in 1 Feb 1999 04:52:48 might
help to provide a framework in which this kind of question could be
precisely asked and anwered.

Another question: Are there diagrammatic theorems that have short
diagrammatic proofs but no short sentential proofs?  

I don't know what might already be known about these questions, if
anything.

 > Perhaps more seriously, there is no general notion of *mathematical
 > proof* to help us understand what is to be preserved when it is
 > claimed that one proof is or is not reduced to another.

Can't we go even farther?  The problem of finding a precise notion of
what it means for one proof to be reducible to another seems wide
open, even if we restrict ourselves to the better-understood realm of
sentential proofs, and even if the proofs are within the same formal
system.

-- Steve