New Paper: Truth Values and Proof Theory

It’s good to get back into writing. Here’s a paper “Truth Values and Proof Theory” that I’ve been thinking about for a long time. I presented a research seminar on this material last year – it’s taken me this long to write it up, due to other commitments.

Here’s the abstract:

In this paper I present an account of truth values for classical logic, intuitionistic logic, and the modal logic S5, in which truth values are not a fundamental category from which the logic is defined, but rather, feature as an idealisation of more fundamental logical features arising out of the proof theory for each system. The result is not a new set of semantic structures, but a new understanding of how the existing semantic structures may be understood in terms of a more fundamental notion of logical consequence.

I like these results, as they’re a mix of motivating philosophy, and formal proofs. I think I’m getting a better understanding of the relationship between the [Cut] rule in a sequent calculus and the maximality conditions involved in the behaviour of things like two-valued evaluations, possible worlds and points in model structures for other sorts of logics. It’s not a coincidence that sequents have two sides, and that there are two truth values. I don’t think I’ve plumbed the depth of the connections between proof theory and model theory, but at the very least in writing this paper up I’ve got a better idea of some of the interesting questions around this area.

It’s one of those ‘bonus’ results that I’ve got out of this research a uniform way of proving completeness for classical logic, Kripke and Beth models for intuitionistic logic, and universal models for S5, all with exactly the same sort of structure. That was a surprise to me when I saw those results just fall out.

Comments on the paper, of course, are welcome. Don’t comment on it here, but on the paper page.

Now I’ve got to figure out how to massage these results into the book. (It’s a pity my backlog of other writing-up tasks is so long, but that seems to be the natural state of the academic these days.)


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, where most updates are posted.


This site is powered by Netlify, GitHub, Hugo, Bootstrap, and coffee.   ¶   © 1992– Greg Restall.