FOM: geometrical reasoning
Stephen G Simpson
simpson at math.psu.edu
Thu Feb 25 20:59:56 EST 1999
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
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
> 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
More information about the FOM