While I was busy writing my most recent paper, “Proof Terms for Classical Derivations”, I heard that Raymond Smullyan had died at the age of 97. I posted a tweet with a photo of a page from the draft of the paper I was writing at the time, expressing loss at hearing of his death and gratitude for his life.

There are many reasons to love Professor Smullyan. I learned combinatory logic from his delightful puzzle book *To Mock a Mockingbird*, and he was famous for many more puzzle books like that. He was not only bright and sharp, he was also warmly humane. However, the focus of my gratitude was something else. In my tweet, I hinted at one reason why I’m especially grateful for Smullyan’s genius—his deep understanding of proof theory. I am convinced that his analysis of inference rules in the tableaux system for classical logic rewards repeated reflection. (See his *First-Order Logic*, Chapter 2, Section 1 for details.) I’ll try to explain why it’s important and insightful here.

It’s a new year, and it’s time for a new paper, so here is “Proof Terms for Classical Derivations” I’ve been working on these ideas for about a year, from some rough talks over most of 2016, to many conversations with my colleague Shawn as I attempted to iron out the details, to many more hours in front of whiteboards, I’ve finally got something I’m happy to show in public.

I’ve been interested in Robert Brandom’s inferentialism since I picked up a copy of Making it Explicit back in 1996. One interesting component of Brandom’s inferentialism is his account of what it is to be a singular term. There are a number of ways to understand inferentialism, but the important point here is the centrality of material inference to semantics. An inference like “Melbourne is south of Sydney, therefore Sydney is north of Melbourne” is a materially good inference.

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.

Talking to Jc Beall during his recent visit to Australia, I got thinking about *first degree entailment* again.

Here is a puzzle, which I learned from Terence Parsons in his “True Contradictions”. *First Degree Entailment* (fde) is a logic which allows for truth value *gaps* as well as truth value *gluts*. If you are agnostic between assigning paradoxical sentences gaps and gluts (and there seems to be no very good reason to prefer gaps over gluts or gluts over gaps if you’re happy with fde), then this looks no different, in effect, from assigning them a *gap* value? After all, on both views you end up with a theory that doesn’t commit you to the paradoxical sentence or its negation. How is the fde theory any different from the theory with gaps alone?

I think I have a clear answer to this puzzle—an answer that explains how being agnostic between gaps and gluts is a genuinely different position than admitting gaps alone. But to explain the answer and show how it works, I need to spell things out in more detail. If you want to see how this answer goes, read on.

- “Fixed Point Models for Theories of Properties and Classes,”
*Australasian Journal of Logic*(14:1), Article No. 8. Abstract pdf - “First Degree Entailment, Symmetry and Paradox,”
*Logic and Logical Philosophy*, 26:1 (2017), 3-18 Abstract pdf - “Proof Terms for Classical Derivations,” article in progress. Abstract pdf
- “Existence and Definedness: the semantics of possibility and necessity,” article in progress. Abstract pdf
- Review of
*Advances in Proof-Theoretic Semantics*edited by Thomas Piecha and Peter Schroeder-Heister,*Notre Dame Philosophical Reviews*(2016) Abstract

*A Concrete Category of Classical Proofs*, TACL 2017 (28 June 2017). coming soon*A Category of Classical Proofs*, Melbourne Logic Group (19 May 2017).*Proof Identity, Invariants and Hyperintensionality*, DIP Colloquium, Amsterdam (7 March 2017).*Proof Terms for Classical Derivations*, LIRa Seminar, Amsterdam (6 March 2017).*Logical Pluralism: Meaning, Rules and Counterexamples*, Pluralisms Workshop, Bonn (3 March 2017).

- UNIB10002: Logic, Language and Information, February–May 2017. completed
- PHIL30043: The Power and Limits of Logic, February–May 2017. completed

I’m *Greg Restall*, and this is my personal website. I teach philosophy and logic as Professor of Philosophy at the University of Melbourne. ¶ 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.

- School of Historical and Philosophical Studies, The University of Melbourne, Parkville 3010, Australia.
- greg@consequently.org
- keybase.io/consequently, to sign or encrypt a message to send to me privately.
- @consequently on Twitter.
- @consequently on Instagram.

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.