In the first two chapters on propositional natural deduction for my revised logic text — coming quite a way into the book — I start with a system for conjunction, disjunction and negation. There are the usual pairs of introduction/elimination rules for conjunction and disjunction. There are three rules for negation, (RAA) — a subproof from A to ★ proves not-A; (Abs) — from A and not-A derive ★; and (DN), the usual double negation rule. ‘★’ is an absurdity marker not a falsum wff. (EFQ) — from absurdity, anything — is a derived rule, but not one of the three basic rules. We note that (RAA) and (Abs) can be thought of as another harmonious pair of introduction/elimination rules, leaving (DN) an odd one out. (Rules for the conditional are introduced in the third chapter.)
The first chapter on natural deduction motivates/introduces the rules by talking through some worked examples. The second chapter looks at some issues, about explosion, the best disjunction elimination rule, vacuous discharge, etc, and takes with another look at the negation rules. First, we note equivalents to (DN), including (EM), excluded middle. Then — at the very end of the chapter — I briefly touch on the status of (DN)/(EM).
I want to say something about this last issue. But equally, in the context of an introductory book I can’t say much. Here below is a draft of the relevant page-and-a-half. I’d very much welcome comments (perhaps not so much about philosophical doctrine, as about the expositional clarity given the intended audience! — can I put things better?).
In §21.4, we noted that the negation rules (RAA) and (Abs) make a nicely harmonious introduction/elimination pair. Which leaves the remaining negation rule (DN) and its equivalents out on a limb. As we asked before: what, if anything, is the significance of this? The issues here quickly become complex and contentious; but here are a few introductory remarks.
- We ordinarily distinguish being true from being warrantedly assertible. The naive thought is that whether a proposition is true depends on how the world is — and how the world is may be beyond our ken, even in some cases beyond our capacity to find out. Hence, we suppose, a proposition can be true without there being any available warrant or grounds for justifiably asserting it.
- But on reflection, for some classes of propositions, perhaps there is after all no more to being true than being warrantedly assertible. So-called ‘intuitionists’ and other constructivists hold that mathematics is a case in point. Mathematical truth, they say, does not consist in correspondence with facts about objects laid out in some Platonic heaven (what kind of objects could these be? how could we possibly know about them?). Rather, being mathematically true is a matter of being warrantedly assertible on the basis of a proof.
- We can’t discuss here whether an intuitionist view of mathematics is actually right. But we can ask: what should be our principles of correct informal reasoning if we accept such a view? For the intuitionist, correct inferences in mathematics are those inferences that preserve warrant-to-assert-on-the-basis-of-proof. Which inferences involving the connectives are these?
If you have a warrant for A and have a warrant for B, then you surely have a warrant for their conjunction, A and B. Likewise, having a warrant for A (or equally, a warrant for B) is enough to give you a warrant for A or B, when the ‘or’ is inclusive. And if you can show that supposing A leads to absurdity, that is enough to put you in a position to justifiably reject A, i.e. to give you a warrant for not–A.
So even if we are thinking of good inference as a matter of preservation of warranted assertibility, versions of the now familiar introduction rules for the three connectives — with (RAA) as negation-introduction — will still apply. And since the harmonious elimination rules simply allow us to extract again from a wff what the introduction rule for its main connective required us to put in, the elimination rules will continue to apply too. - What, however, will be intuitionist’s attitude to the rule that we can cancel double negations or to equivalent rules? Take the law of excluded middle. The intuitionist won’t endorse this as a generally applicable principle. Suppose that A is a mathematical open conjecture, not yet actually proved or disproved. Must it all the same be provable or disprovable? There is no obvious reason why so. Hence, according to the intuitionist (who holds that all there is to truth in mathematics is provability), we have no warrant to suppose that mathematically things are one way or the other with respect to A, so no warrant for A or not-A.
- Now going formal again, imagine you are an intuitionist who wants to encapsulate the inference rules you accept into a variant of our natural deduction system. Then you will adopt all the same rules as our PL system minus (DN) (since that’s equivalent to the unwanted excluded middle). Such a system, at least once we add the rules for the conditional too, is said to define intuitionistic propositional logic. And arguably, this intuitionistic logic is the right formal logic for arguing with the connectives when dealing with any domain where truth is warranted assertability/provability.
- Imagine alternatively that you conceive of truth in a more naively ‘realist’ way for some domain. So you think of the truth-values of (non-vague) propositions of the relevant kind as being determined one way or another by the world, independently of whether we can warrantedly judge whether they are true or false. You will then think of negation here in the classical way, as simply swapping the value of a proposition, taking you from a determinately true proposition to a false one and vice versa; and every proposition of the relevant kind determinately has one value or the other, ensuring that excluded middle always holds. Going formal, you will therefore adopt (EM) or equivalently (DN) as one of your rules for the connectives. The classical logic of our PL system reflects that classically realist view of truth.
So, at any rate, goes one often-told story. But it goes without saying that there is a great deal to wrestle with here. Does the apparently attractive logic of PL, with its immediately appealing rules, really presuppose a particular realist conception of truth? Are there really areas of enquiry where the appropriate notion of truth is non-realist, more akin to an idea like ‘warranted assertability’ or ‘provability’. If there are, is intuitionist logic really the right logic for such domains? Does it then make sense to think of different logics as being appropriate to different domains? Or should we rather think of the law of excluded middle — if it doesn’t apply to reasoning in general — as not part of core logic at all? Should we perhaps think of excluded middle, when it applies, as really more like a very general metaphysical claim about the determinacy of some parts of the world?
It also goes without saying that we can’t begin to tackle such intriguing but baffling issues in this book!
And there the chapter will end, apart from the usual end-of-chapter summary and exercises. As I said, all comments (or rather, all comments which bear in mind the intended introductory role of these remarks) will be very gratefully received!
Given Julien’s reminder, perhaps one might interpret your star as the empty set of formulae. And since we routinely abuse a conceptual distinction by replacing singleton formula sets by their unique elements, one might likewise create an ideal ’empty formula’ as surrogate for the empty set of formulae….So long as this is done as a mathematical or expository convenience and not as a metaphysical wedge.
I am rather wary of the treatment of the star. If, in earlier chapters, the book has already introduced truth-functional readings of the more familiar connectives for classical logic, then the most elegant reading of the star is simply as one of the two zero-ary truth-functional connectives. This, when followed by nothing, also doubles as the formula known as the falsum. But you don’t want to do that, and I guess that the underlying reasons are partly expository and partly substantive.
On the expository side, you may perhaps wish leave as much as possible of the earlier discussion of inference open, with minimal change, for an alternative intuitionistic reading. But that consideration does not seem to have much force. In so far as one has already given truth-functional readings of the arrow and disjunction, one is already be obliged not only to change those readings but also to cut down on what is derivable from what, when turning to intuitionistic logic. So, you might as well do the same with the falsum.
On the substantive side, I suspect that, like many other authors, you wish to hang on, by hook or by crook, to the dream that every connective in classical logic has both an introduction and an elimination rule that are in harmony with each other.
The first part of this is demonstrably false in the context of a consequence relation in set/formula format (as contrasted with a set/set format, where all truth-functional connectives do indeed have both introduction and elimination rules). In the set/formula format, the falsum, negation, nand, neither-nor, and exclusive disjunction are all contrarian (i.e. come out false in the top row of its truth-table), and it is easy to show that no contrarian connective of classical logic has any introduction rules at all, unless one fudges unashamedly with the notion of what counts as such a rule. Even intuitionistic falsum and negation lack any introduction rule unless one fudges with the definition, as has also been shown.
The second part of the dream is worse. Despite half a century of proposals, there is no clear and consensual formal account of what exactly “harmony” is supposed to mean in the set/formula format and, in any case, for that format it is very odd to talk of harmony between introduction and elimination rules for a connective that has none of the former but at least one of the latter (or conversely, as is the case for sub-contrarian connectives). I would add that too much of the literature on the notion of harmony carries a rather strange tone of ineffable mystification.
But so much the worse for the dream (I am trying not to say dogma): it was not supported by anything other than a hope of symmetry that loses its appeal when one realizes that the passage from set/set consequence relations to set/formula ones introduces mathematical imbalances that ruin some of the deep symmetries of the former. As humans, we have to work in practice with the set/formula format, but we also have to put up with its blemishes.
I agree with everything David says, on the assumption, however, that the consequence relation is SET-FMLA. If it is SET-Emptyset-or-formula, then IPL is harmonious, and CPL can be seen as harmonious, too.
Thanks, David!
On harmony: I now realize that my post above rather misrepresents what actually happens earlier in the book, as it makes it sound as if harmony features significantly as an issue there.
Well, I give some usual intro/elim rules; I say arm-wavingly that they seem to fit nicely together in that the elimination rules allow you to extract again what was put in by the intro rules (in some intuitive sense). But although I use the word “harmony” for this fitting together, I certainly don’t go into any serious discussion. Really the word is just left hanging as a hook someone teaching a course might (or might not) want to latch onto. Maybe I should even avoid this!
Certainly, I now see that, as things stand, I make it sound as if two issues — (i) whether (DN) has a special status in the pattern of intro/elim rules, and (ii) whether (DN) is tied to a specifically realist conception of truth (or something like that) — are definitely entangled, which is more than I really meant to do. In the light of your very helpful remarks, some rewriting (if only to make my actual text more clearly non-committal!) is certainly needed.
On interpretations of the absurdity sign — marker (akin to the marker we use to close off branches on truth-trees) or wff (zero-place connective)? I’m not sure how deep my preference for the first goes! It’s reasons of elegant economy, as much as anything. Which is why I’m not sure why you say “the most elegant reading of the star” is the second one. Though I also say in a section where I briefly note that different readings are possible, that (at an elementary level, anyway) not much hangs on this.
I find 4 confusing, and when I apply what I (by now somewhat vaguely) remember of intuitionist logic, I still find it confusing. It looks like you may be relying on a distinction between denying excluded middle and simply not accepting it, which may be fair enough, but I leave 4 with an uneasy feeling that I don’t quite understand what the intuitionists have decided.
Also, when I read “according to the intuitionist who holds that all there is to truth in mathematics is provability”, I have a moment of wondering why the qualification is there. Are there intuitionists who don’t hold that all there is to truth in mathematics is provability?
Finally, 4 says “Suppose that A is a mathematical claim that is neither provable nor refutable.” That looks very strong. What happens with a mathematical claim that merely hasn’t yet been proved or refuted? How would an intuitionist know that a claim was neither provable nor refutable? Especially since their idea of “know” would presumably be about proof.
Many thanks for this!
Taking your points in turn, it was indeed misleading to talk about “not denying” excluded middle. (I’ll relegate it to an exercise to show that the intuitionist can’t say not-(A or not-A).)
Second, that was mispunctuated — I didn’t mean a qualification picking out only some intuitionists!
Third, you are right — what I wrote indeed can’t be what I meant!! So I will rephrase.
Thanks again!