## Proof Terms are fun

#### 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 photo posted by Greg Restall (@consequently) on

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