Proof Terms are fun — consequently.org

2 September 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 Sep 1, 2016 at 4:42pm PDT

about

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, and the Director of the Arché Philosophical Research Centre for Logic, Language, Metaphysics and Epistemology ¶ I like thinking about – and helping other people think about – logic and philosophy and the many different ways they can inform each other.

To receive updates from this site, subscribe to the RSS feed in your feed reader. Alternatively, follow me at @consequently@hcommons.social, where most updates are posted.

contact

Social media: @consequently@scholar.social.
Personal email: greg@consequently.org.
St Andrews profile.
My office is in Edgecliffe, The Scores.