Proof Terms are fun

Today, between marking assignments and working through a paper on proof theory for counterfactuals, I’ve been playing around with proof terms. They’re a bucketload of fun. The derivation below generates a proof term for the sequent \(\forall xyz(Rxy\land Ryz\supset Rxz),\forall xy(Rxy\supset Ryx),\forall x\exists y Rxy \succ \forall x Rxx\). The playing around is experimenting with different ways to encode the quantifier steps in proof terms. I think I’m getting somewhere with this. (But boy, typesetting these things is not easy.)

A whiteboard-to-LaTeX scanner would be really handy right about now. Anybody have one?

A photo posted by Greg Restall (@consequently) on Sep 1, 2016 at 4:42pm PDT