FOM: geometrical reasoning

[Jerry Seligman]

Steve Simpson (25 Feb 1999 20:59:56) asks:

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

A good question.  I have something to say about this (below), but I
expect there are others who can answer it better. There is an e-mail
discussion group on diagrammatic reasoning  (diagrams at clsi.stanford.edu).
I will solicit answers from members of the list and post the results here.

>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?

Yes.  But it is difficult to take this line of thought further.
Since each diagram occurring in a proof is equivalent to a sentence of
elementary geometry, a  diagrammatic proof in geometry can be translated,
step by step,
into a sequence of sentences of elementary geometry.  The result cannot
be expected to be a proof in any proof system for predicate logic, but we
might
hope that there is a weaker condition, which if satisfied would show that the
original proof is preserved by the translation in some significant
way.  Here are several proposals for such a condition, all of which can be
seen to
be inadequate.

(1) Each sentence in the sequence is provable from previous
sentences and Tarski's axioms.

(2) Each sentence in the sequence is either one of Tarski's axiom
or is provable from earlier sentences in the sequence.

(3) There is a sound set of rules (effective procedures) for manipulating
sentences of
elementary geometry, and the sequence conforms to those rules.

(4)  Rules exist, as specified in (3), and they are derivable in, say, a
natural deduction
system for predicate logic together with Tarski's axioms.

Sequences of sentences derived from diagrammatic proofs in geometry will
satisfy
conditions (1) and (3), for straightforward reasons, given  only the
completeness of
Tarski's axiomatisation and the soundness (and effectiveness) of the
diagrammatic system.
The structure of the proofs is irrelevant to whether or not these
conditions are satisfied,
and so neither of them can be said to isolate a non-trivial sense in which
the  proof is
preserved in translation.   Conditions (2) and (4) demand  that a lot more
structure is
preserved, but they are not satisfied by sequences derived from
diagrammatic proofs.

Given that the systematic study of diagrammatic reasoning reveals that
diagrammatic proofs
have a quite different structure to sentential proofs (even if no general
structure has been
found), the onus is on the person who claims that these proofs are
reducible to sentential proofs
to provide a specific a non-trivial sense in which this is true.

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

Yes.  You can easily convince yourself of this by playing with the
program Hyperproof (Barwise and Etchemendy, CSLI Publications,
1995; ISBN: 1881526119).  A diagram of a chessboard containing
polyhydra of various shapes and sizes is manipulated to construct
proofs about the arrangement of the pieces.  The user can use both
diagrammatic and sentential inferences, even within one proof,
so it is easy to get a sense of when diagrammatic methods make
the proofs shorter.

The reason for the shortness of diagrammatic proofs is that they exploit
constraints built in to the representational medium.  Consider reasoning by
cases.
In predicate logic, one to look at every logically possible case.
Typically one starts with a  long disjunction or a sequence of disjunctions
and shows that each disjunct or combination of disjuncts is either
inconsistent
with the premises, or (together with the premises) implies the conclusion.
In a diagrammatic system, cases that are inconsistent with the premises are
not
even expressible, and so there is less work to do.   Much of the logical power
of diagrams is built into their syntax.

I do not know of any examples of very short diagrammatic proofs, of
the order demonstrated for induction (c.f. Friedman, FOM 25 Feb 1999 18:02:52).

>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.

So far as I know. I'd be interested what the proof theorists on FOM have
anything
to say on this matter.




Jeremy M. Seligman
Department of Philosophy, The University of Auckland, Private Bag 92019,
Auckland, New Zealand
Tel: +64-9-373-7599 xtn. 7992, Fax:  +64-9-373-7408, Time Zone: GMT +13 hours