A rigid framework

Well, I am back from Yosemite, but not in quite the way I had hoped. I was climbing the Prow on Washington Column with Aaron McMillan (a grad student from Berkeley, student of Weinstein's) and on our second day I took a fall resulting in a broken ankle and the end of our climbing vacation. If you are interested in the long version you can find the story here.

Anyhow, I am sitting at home now with my leg encased in a rigid boot which will have to stay on for the next six weeks or so while the bones rejoin themselves. It got me thinking about the idea of such 'rigid frames' in teaching - actually in teaching analysis, since I'm thinking about my course for next fall. Bear with me for a moment while I try to explain what I mean.

Suppose that you're asked to give a proof of something like "the limit of a uniformly convergent sequence of continuous functions is continuous". As a professional mathematician you might just say "$3\epsilon$ argument", or you might write out a more detailed proof. But whatever you did - or, at least, whatever I would do - probably doesn't explicitly express every one of the many quantifiers that are involved in this statement, or explicitly delimit the scope of every one of the free variables that may be introduced during the proof. To be required to do so would be excessively rigid and constraining, like my ankle boot. As mathematicians we've developed the bones and muscles that allow us to work correctly with a less than wholly formal style of argumentation; and that's a vital skill. But, I'm wondering, do we give our students enough "rigid support" so that their mathematical "bones" can develop? Or do we overload them by presuming on strength that isn't there yet? If I just took off my boot now and tried to walk, the results would be disastrous; my bones aren't ready for that yet.

Specifically, one of the things that I try to emphasize in teaching analysis is taking apart an argument or definition involving multiple quantifiers into a hierarchy of more elementary units, which are nested within each other like subroutines in a computer program. And I then try to explain that to each of these elementary units corresponds a "proof skeleton", so that for instance to the elementary unit $\forall x\in A, P(x)$ ($P$ being some possibly complex proposition) corresponds the proof skeleton:

Let $x$ (or some other symbol not yet used) be an arbitrary member of $A$. Then (argument), leading to the conclusion $P(x)$. We have shown that $P(x)$ is truw for an arbitrary member $x\in A$, so we have proved $\forall x\in A, P(x)$. (end of scope of symbol $x$)

Nesting these proof skeleta in a way corresponding to the multiply-quantified statement to be proved gives a quite rigid framework - a "cast" - for the proof. Of course it is still necessary to supply the actual argument! In my experience though students sometimes need more guidance with the structure of the proof than the individual computations comprising it; and this system supplies it.

I am wondering about writing some software which will generate these "skeleta" semi-automatically and will force students to write proofs into them. Not for ever of course - just until the "bones" grow strong. Of course the worry is that then the teaching suddenly becomes about software and not about mathematics. Still, I think it could be a helpful tool. Maybe something like this exists already. Does anyone know?