Excluded middle, harmony, intuitionist logic for beginners

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 deny this (by the rules he accepts, not-(A or not-A) implies both not-A and not-not-A, and hence implies a contradiction). However, the intuitionist won’t endorse excluded middle as a generally applicable principle either. Suppose that A is a mathematical claim that is neither provable nor refutable. Then, 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!