Early afternoon: advisor meeting. Talked through material up to and including the completeness proof with Frank, and no major errors popped up. Woo! Usually being forced to explain something to another human being is the next best thing to excessive hubris for finding bugs. Making a strange sort of red-queen progress on soundness. I keep formulating new lemmas to replace older, erroneous ones, but my understanding of the system as a whole is growing quite well. I think the right thing to induct on is very nearly in sight. Just need to get all of the quantifiers going in the right directions...
Office hours: nobody came. Signed up on the NaNoWriMo site at last. Have been wanting to do this ever since hearing about it through
catamorphism mid-last November. I still have very little clue what to write. The project I was working on during the summer is way too ambitious to adapt, and I think they frown on having jumped the gun anyway.