consequently.org/news

About

I'm Greg Restall, and this is my website. I work in Philosophy at the University of Melbourne. [Email: greg at consequently.org; Skype: greg_restall; Post: Department of Philosophy, University of Melbourne, Parkville 3010, Australia.]

Writing

These are the three last modified entries on my writing page.

“Truthmakers, Entailment and Necessity 2008,” an addendum to “Truthmakers, Entailment and Necessity,” to appear in Truth and Truth-making, edited by E. J. Lowe and A. Rami, Acumen, 2008. →
[with Rebecca Kukla and Mark Lance] Appendix to Rebecca Kukla and Mark Lance ‘Yo!’ and ‘Lo!’: the pragmatic topography of the space of reasons, Harvard University Press, to appear. →
“Curry’s Revenge: the costs of non-classical solutions to the paradoxes of self-reference,” in The Revenge of the Liar, ed. JC Beall, Oxford University Press, pages 262–271, 2008. →
“Anti-Realist Classical Logic and Realist Mathematics,” under revision. →
“Proof Theory and Meaning: on second order logic,” to appear in the Logica 2007 Yearbook, Filosofia. →

Classes

In Semester 2, which starts on July 31, I’ll be teaching an honours seminar 161-438 Logic and Philosophy, in which we cover proof theory and its applications to semantics.

Events

AAL2007: the annual conference of the Australasian Association for Logic, University of Melbourne November 9 to 11, 2007.

Recent Past

University of Melbourne Philosophy Undergraduate Workshop, University of Melbourne September 21 to 23, 2007.

Logic Colloquium 2007, Wrocław, Poland, July 14-19, 2007.

1st GPMR Workshop on Logic & Semantics on Medieval Logic and Modern Applied Logic, Rheinische Friedrich-Wilhelms-Universität Bonn, Germany, on June 28-30, 2007.

Logica 2007, Hejnice Monastery, Czech Republic, 18-22 June 2007.

Heart of Philosophy Café talk and discussion on “What Marx, Freud and Nietzsche have taught me about belief in God”. Tuesday May 8, 7--9pm in the Merrick's General Store.

Key Ideas in the theory of proofs #1: The Duality of Proofs and Counterexamples

Now that my undergraduate teaching is done for the semester, I can devote more time to research. I’m going to use this place to post some material from my proof theory project. My goal is to present some key ideas in an accessible way.

Today’s idea is the duality between proofs and counterexamples.

Proofs: You can think of a valid argument as underwritten by a proof. A proof leads from the premises to the conclusions, and shows how the conclusions follow from the premises. An invalid argument from premises P to conclusions C is one for which there is no proof leading from P to C.

Different theories of proofs will characterise these in different ways (natural deduction, Hilbert-style axiom systems, Gentzen-style sequent systems, tableaux, etc.) but at heart, a proof is a formal structure that bears witness to a valid argument.

Counterexamples: You can think of an invalid argument as witnessed by a counterexample. A counterexample is a way of making the premises true and the conclusions untrue, and it shows how the conclusions say something more than what is present in the premises. A valid argument from premises P to conclusions C is one for which there is no counterexample rendering P true and C not.

Different theories of counterexamples (call them models or interpretations if you like) characterise them in different ways: truth tables, many-valued algebras, models with domains of quantification or “worlds” models for intensional logics, but at its heart, a counterexample bears witness to an invalid argument.

Notice the duality: Proofs witness validity and counterexamples witness invalidity. A proof gives you a validity fact. Only an absence of proofs tells you about invalidity. Conversely, a counterexample gives you an invalidity fact. Only an absence of counterexamples tells you about validity. These two different ways of characterising logical consequence have very very different properties.

Many key results in 20th Century logic, such as Gödel’s completeness theorem, pair together these two notions. A soundness result (for a proof system, given some set of counterexamples) tells you that a proof system provides a proof from P to C only when the argument from P to C has no counterexample. A completeness proof (for a proof system, given some set of counterexamples) tells us that a proof system provides a proof from P to C whenever the argument from P to C has no counterexample.

If you have a well-matched pair of a system of proofs and a system of counterexamples — for a notion of logical consequence — then you have two different ways to look at the one relation between premises and conclusions. These different tools are useful for different purposes. If you use just one of them, you might be selling yourself short.

[Aside: This was my critical point in my essay “One Way to Face Facts”: I found Stephen Neale’s excellent little book on slingshot arguments Facing Facts) helpful, but one-sided. In the book, we find detailed analysis of different slingshot proofs. Neale charts which principles combine together to produce unwanted results. What makes the work one-sided is that he never walks on the other side of the street to look at counterexamples. (He never looks at models to show that particular combinations of premises cannot produce the unwarranted conclusions on their own, as you can easily do if you produce counterexamples.) It is as if he is charting a boundary between territories by making occasional forays from this side of the boundary, never realising that you can jump the fence to see it from the other side as well. End of the aside.]

Now, if we have two different sorts of tools for characterising valid argument, a philosopher is constitutionally bound to ask a question: Is one of these tools more fundamental than the other? Many would say yes. My colleague Graham Priest takes counterexamples to be primary, and proofs to only be a means for enumerating the notion of logical consequence given by means of the counterexamples. (See, for example, his paper “Validity” in Varzi’s volume The Nature of Logic.) Others, like Dummett’s semantic anti-realist or Brandom’s inferentialist, would seem to take proof as primary, as you explain the meanings of a concept by articulating its role in proof.

But do we have to choose? Why think that one way of characterising logical consequence is any “deeper” than the other? To put things in an more cryptic manner: why think that there is just one direction of “depth” or “priority”?

What do you think?

Posted 11:05 AM on June 13, 2006

Comments

Excellent! The discussion of which one is the primary thing resembles the discussion in modal logic about choosing the primitive operator between □ and ◊. The arguments in favour of either one of them sound a lot like the arguments you quote about those in favour of proofs or of counterexampless.

Tony Marmo , June 13, 2006 04:33 PM

A related duality arises when considering the notion of informational content. E.g., the Inverse Relationship Principle clearly favours the counterexample-side: the content of A is individuated as the set of cases excluded by A.

On the other hand, an inferential approach is on the proof-side: the content of A is individuated as the set of wffs which can be inferred from A.

Interestingly there is still an asymmetry in their treatment, those who favour a model-theoretical approach (broadly realist positions about information) can play on both sides, while proof-theorists (semantic anti-realist positions about information) confine themselves to the second side only. The latter limitation seems totally unnecessary (even unwarranted?), and I think is also close to your present concerns.

p-trick , June 13, 2006 05:38 PM

Here’s what came to (my logically amateur) mind on reading this.

You don’t need a concept of negation to have proofs but it seems vital for counterexamples. For some really trivial logic where deduction was a fuction rather than a relation you’d still have proofs but counterexamples could only arise in a meta-language.

Daniel Slaney , June 13, 2006 06:13 PM

Yes, p-trick, that’s not only close to my present concerns, I think it is one of my concerns! Perhaps we can talk about it at Nancy. I think that a semantic anti-realist (one who wants to tell some story starting with proofs) can avail her/himself of models, and in fact some of the most interesting work in constructive logic (Beth/Kripke models, realizability interpretations, etc.) do just that.

Greg Restall , June 13, 2006 06:14 PM

Hi Daniel:

I think there’s something interesting about the language/metalanguage distinction here, and that proofs and counterexamples are, traditionally thought of as metalinguistic.

On negation and counterexamples: it seems to me that you don’t need negation in the language to construct counterexamples. Think of the classical logic of conjunction and disjunction. (Distributive lattice logic.) You can think of a counterexample in a row of a truth table as an interpretation in which the premises are true and the conclusions fail to be true. You don’t need negation in the object language to do that.

You do need negation in the language for talking about counterexamples of course. But you need it in the language of proofs if you want to talk about invalidity: there is no proof from P to C, so the argument is invalid…

Greg Restall , June 13, 2006 07:17 PM

This is a good way to put a lot of things that I remember John MacFarlane discussing in his lectures this past semester that I was TAing for. Interestingly, Tarski seems to consider the counterexamples more fundamental. At least, he gives an argument that his model-theoretic semantics captures the ordinary notion of consequence, and then uses the soundness and completeness theorems to show that proof-theoretic notions are also correct. Towards the end of his book objecting to this, Etchemendy points to a related, but more symmetrical, argument by Kreisel arguing for the correctness of the standard account. Basically, we can see pretty directly that existence of a proof guarantees validity, and that existence of a counterexample guarantees invalidity. Because of the soundness and completeness theorems, these conditions are mutually exclusive and exhaustive, so their implied extensions for validity coincide, and thus must both be correct.

Kenny Easwaran , June 13, 2006 10:54 PM

The Kriesel argument is really interesting: using my terminology, both proofs and models agree with intuitive validity where they provide positive evidence. (If you have a proof from P to C the argument is valid; if you have a counterexample for the argument from P to C, the argument is invalid.) And then soundness/completeness tells you that both accounts get validity correct when it comes to negative evidence as well. (The absence of a proof, or the absence of a model.)

Where the Kreisel argument is interesting is the application to theories with intended “models” that are not delivered by the completeness argument (a proper class “model” of set theory, for example), but that’s another story…

Greg Restall , June 14, 2006 09:27 AM

This account of proofs and counterexamples works well, it seems accessible. One small suggestion, the section that reads:

A completeness proof (for a proof system, given some set of counterexamples) tells us that a proof system provides a proof from P to C whenever the argument from P to C has no counterexample.

Would suggest to my unsophisticated mind that a proof system automatically offers up the proof from P to C (this suggestion comes from the use of provides). That in some sense it is the proof system that is doing the work and just following the steps will get one from P to C without any creative input required from the person constructing the proof. If this is not the intended meaning, perhaps can provide would work instead?

Duncan Watson , June 22, 2006 02:46 AM

Hmm… I didn’t mean to say that the proof of a valid argument was easy to find, but I did mean to suggest that if the argument was valid by the lights of model theory, then the proof system does have a proof for that argument somewhere. (I do want, however, to leave open the possiblility that the proof system might say “I have the proof here somewhere but I can’t seem to find it…” like those of us with messy offices.) So “can provide” is closer to the mark. Thanks!

Greg Restall , June 22, 2006 11:59 AM