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.
