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.)

← 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.

- greg@consequently.org
- keybase.io/consequently, to sign or encrypt a message to send to me privately.
- @consequently on Twitter.
- @consequently on Instagram.
- @consequently on GitHub.

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.