[FOM] 622: Adventures in Formalization 6

[Larry Paulson]

> On 20 Sep 2015, at 08:33, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> iii. I am particularly interested in the EASIEST, EARLIEST possible
> places where complexity seems to set in - where imperfections become
> apparent - where heuristics become seductive - where theory looks
> ineffective.
> iv. Specifically, I am particularly interested in the EASIEST,
> EARLIEST possible places where the way mathematicians - or a certain
> effective productive kind of mathematician - want to do things, think
> things, write things, starts to DIFFER from the way Proving technology
> works.

Let’s imagine proving that there is no injection from a set of N elements into a set of N-1 elements. The first complication is that we already have to decide whether N denotes an integer or a natural number, even if we have the explicit assumption N>0. And we have to make this decision whether we are working in raw ZFC or in most typed formalisms. In general, the coexistence of a variety of number systems causes a lot of tedium, and setting up the obvious chain of inclusions from the natural numbers to the complex numbers (so that we can regard N as a complex number if we want to) is not straightforward.

Now let’s confine ourselves to the natural numbers. The next question is whether N-1 exists. Here, using a formalism in which you talk about partiality explicitly leads to further complications; if on the other hand you assume that everything is defined, then we have N-1 < N, since we know that N is nonzero.

And that’s before we even get to the question we started with, namely proving that no injection exists. A formal argument isn’t difficult, but requires a certain amount of technical skill that seems way out of proportion when the conclusion is so obvious. Another example of this phenomenon, which I have encountered recently, concerns contours in the complex plane: piecewise continuously differentiable functions defined on a closed interval. It should be obvious that joining two such contours end to end, or reversing a contour, or taking a segment of a contour, yields another contour. Yet in my experience, proving that the required derivatives exist and are continuous is unreasonably laborious. Probably I am missing a trick, but why should clever tricks be necessary here?

To end on a more positive note, I recently wanted to formalise the Stone-Weierstrass theorem, and a colleague sent me the following paper:

http://www.ams.org/journals/proc/1981-081-01/S0002-9939-1981-0589143-8/S0002-9939-1981-0589143-8.pdf

This is 3 1/2 pages of fairly dense calculations, and I found it quite intimidating. But in fact the formalisation was straightforward; it took a week or two, but mostly in odd hours (I was at a conference for much of the time). Explicit technical lemmas proved in detail seem much easier to deal with than obvious truths.

Larry Paulson