September 2, 2016

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

← First Degree Entailment, Symmetry and Paradox | News Archive | A Puzzle for Brandom's Account of Singular Terms →


I’m Greg Restall, and this is my personal website. ¶ I am the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews.



To receive updates from this site, you can subscribe to the  RSS feed of all updates to the site in an RSS feed reader, or follow me on Twitter at  @consequently, where I’ll update you if anything is posted.