Had some discussion with fancybred about trying to come up with a syntactic proof of the soundness of the labelled deduction sequent calculus. It's a real tough nut.

Went climbing in the evening. I finally did that big white-with-black-squiggly V0+ traverse that's been up for all these weeks. The secret was doing it first instead of after I had already tired myself out. Also I did one of the new V1s.

After that hung out with Jen and watched another episode of Sagan's "Cosmos". Pretty awesome stuff.