Thursday 6 November 2014

Boy do I ever not like this proof structure stuff.

This is a post I've been meaning to write for, well, more than three weeks now. In a way, it's almost better I put it off, since my opinions have somewhat changed.

When it was first introduced, I thought the rigid structure used to prove statements in this course was just incredibly tedious. It wasn't a huge problem, however, since anything we were asked to prove was pretty simple and direct.

When I got to writing up the assignment though, having to stick to such a rigid structure really bothered me. I've got some math background, so having to break every thought into a sentence that begins with either "Assume", "Let", or "Then" just feels silly, and the impossibility of giving even mildly complicated statements was so frustrating. It sure didn't help that typesetting it in Latex was a pain (for an indication of how dumb my approach was, all proofs were plopped into a flalign* environment, with \quads as indents. It looked great, but boy was it tedious). I was ready to write this right after that, but, of course, I put it off, since I'm too busy to write blog posts for dour TAs and google search crawlers.

Now, after having studied for the midterm, I've started to come around and appreciate the value of the way lines in a proof are linked, at least as an introduction to formal logic. It's not like you can get away with writing decent proofs without at least a tacit understanding of inference rules, and in some sense, being introduced to it explicitly would have saved me some pain in a previous life. 

However, I do still have problems with the way proofs are being taught in this course. The whole formal background isn't discussed--inference rules were given as almost a side note in lecture, and the reasoning behind using statements like "assume" and "let" isn't explained any better than in a more standard introduction to proof. While its formal roots are showing, this course is not an introduction to formal logic. Things like "you don't get to choose x if you're trying to prove a universal" will be permanently burned into everyone's minds, but the fact that you can't choose \(x\) to depend on \(y\) in a statement like $$\exists\,x,\,\, \forall\, y$$ was barely mentioned, despite being less obvious.

At the same time, the rigidity of the structure makes proving things more difficult than it would be otherwise. Implication between lines is not always clear, so a statement like 

$$\text{Since } \lfloor y\rfloor \in \mathbb{Z} \text{ and } \lfloor y \rfloor \leq x \text{, } \lfloor y \rfloor \leq \lfloor x\rfloor $$  
becomes unnecessarily difficult and cumbersome to follow when split into tiny steps (see A2 solutions, for an example). 

It's kind of like asking someone to write an essay but limiting them to use certain keywords and format it in jot notes. It can be illustrative if the content is relatively simple, but as soon as things become difficult or more nuanced, it's more of a hindrance than it is a help. 

I know that an introduction to proofs can be a nightmare, and forcing people to conform to a rigid structure is useful in ensuring everyone understands how to introduce universals, existentials, and impications, but ultimately, learning to write proofs is difficult no matter what. Forcing a rigid structure on all proofs in the course without getting into the background of why such a structure is important really limits the content for little gain; there are countless proofs within grasp of the math prerequisites given for this course, but so far we've been limited to proofs about the floor function and products modulo an integer. One would hope that using in using a more unconventional approach to introducing proofs, it might more readily bring a student to a baseline level of knowledge, but I have some trouble believing that learning in this way generally prepares someone for more advanced topics any more effectively than another approach. As it stands, I feel like the majority of the three or so weeks spent covering proofs can be summarized in a few lines:


  1. If proving a Universal -> write "assume x in [domain]", conclude "for all x ..."
  2. If proving an Existential -> write "let x = __. Then x in [domain]", conclude "exists x ..."
  3. If proving an Implication -> write "assume [antecedent]",conclude "A => C"


There's more to it than that, but the more difficult ideas (like what to do with conjunction and disjunction) have almost been left to the student to figure out--as they always are in an introduction to proof.

No comments:

Post a Comment