FOM: Geometric reasoning

[Joe Shipman]

Geometric reasoning in the style of Euclid and Archimedes used to be the
model for logical rigor.  Once gaps were pointed out axioms were easily
provided to fill them (e.g. betweenness and continuity axioms).  It
cannot be this type of reasoning which is asserted to be unformalizable
in the predicate calculus, though it is useful to point out how axioms
of betweenness and continuity were implicitly used (in general by
declaring that points of intersection which existed in a diagram always
really did exist).

If by "geometric reasoning" is meant some sort of reasoning with
pictures that is not directly formalizable in the predicate calculus,
can anyone provide an example?  Most I can think of basically involve
asserting something as evident to geometric intuition that is hard to
prove (e.g. the Jordan Curve theorem), but even this is formalizable by
asserting  a new axiom.  This would be interesting enough, but I do not
think it is currently the case that any such statements are regarded as
valid but unproved in ZFC.  (The outstanding open problems in geometry
like the Poincare conjecture and the Kepler conjecture [a proof of which
was recently announced] are not intuitively obvious enough that a proof
depending on them would be acceptable; there may have been such problems
once but I don't think there are now.)

On the other hand, there may be certain results in low-dimensional
topology and geometry whose proofs involve complex operations on and
motions of, for example, 3-dimensional manifolds, which may be
impossible for a mathematician without good powers of visualization to
follow.  If the proofs have been published and accepted it may be
because those who did follow the proof were confident it could be
formalized in the predicate calculus, WITHOUT any such formalization
having actually been done (here I am not referring to a level of
formalization suitable for machine verification, just a level such that
a mathematician who couldn't make pictures in his head could follow the
proof).   This seems like the best place to look for reasoning that is
actually irreducible.  There may be theorems that some geometers or
topologists have been able to establish to their own satisfaction using
visualization but which have not been "proved" to the satisfaction of
mathematicians in general.  We need examples here!

-- Joe Shipman