Can proof by picture be made rigorous?

Great Debates
1

I’ve wondered about this before, but encountering the page below prompted me to write this post. (Note: I have not read the book.)

http://cslipublications.stanford.edu/site/1575862948.html

For centuries, we’ve had informal logic; but I would say it wasn’t until the early twentieth century that we understood logic formally and its limitations. (I am not a historian of mathematics, so I could be wrong about this.)

Is it possible to formalize pictorial arguments as we formalized symbolic ones. There are things like commutative diagrams and Ferrers diagrams. But is there a more general theory?

2

Isn’t any system of geometry, Euclid’s or otherwise, a formalization of pictorial arguments? Or am I missing the point?

(point. tee hee)

3

In general, no. There will always be some specificity implied by a drawing that can’t be relied upon in the general case.

That said, order theory makes heavy use of (a certain type of very well-defined) diagrams, and there’s no lack of rigor there.

4

Yes, but that formalization is a symbolic one, i.e., one in which the means of proof is the transformation of strings of symbols. What I have in mind is a formal system that is pictorial in character.

5

If what you mean by a pictorial formal system is one where the means of proof is through a single illustration, I would guess that reasonably complex systems will quickly exhaust the capacity of an illustration. Consider that the repeated combination of axioms to form theorems would at its very simplest be a multi-rooted tree. Each of the axioms and theorems would require some sort of designation – are you going to use illustrations to designate them, or resort to symbols? A drawing of a tree can easily become unmanageable even without labels on the nodes.

Another way to look at it: What is a string but a series of ‘yes’ and ‘no’ symbols connected by an assumed exponential relationship? Can you come up with a pictoral representation scheme that allows you to depict exponentially many members of a set using linear space, that is as efficient and practical as a string? Bear in mind that there is really no difference between strings like ‘12589920’, and ‘x+y=3 => x=3-y’ and ‘print “hello world”;’ – all can be represented as a series of 0’s and 1’s. The only reason why one representation is chosen over another is that it is easier to read by humans. How can your pictoral system represent these concepts more clearly than the existing conventions? Ultimately, even your pictoral system must have a conversion to the same binary string as our current conventions, if it is to be isomorphic to them (and therefore correct).

In summary, a correct pictoral system is no different from a string. The representation isn’t as important as the underlying math, which would be the same whether it was communicated in binary, pictographs, or by Godel number.