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.)
I’m Greg Restall, and this is my personal website. I teach philosophy and logic as Professor of Philosophy at the University of Melbourne. ¶ From August 2021, I will be the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews. ¶ Start at the home page of this site—a compendium of recent additions around here—and go from there to learn more about who I am and what I do. ¶ This is my personal site on the web. Nothing here is in any way endorsed by the University of Melbourne.