Natural deduction for quantifier logic

It’s very late in the day, as I hope to get IFL2 finally off to the Press within the next fortnight or so. But since the natural deduction chapters are new to the second edition it is understandable (I hope!) that I am still worrying away at them, tinkering here and there. Here then is the latest version of the three main chapters on QL proofs. Any last minute corrections and/or helpful comments (other than, perhaps, “use a different proof system”) will still be most welcome …

There is no real novelty here except perhaps by mistake: though one feature of the handling of QL proofs is the sharp distinction made between dummy names (parameters) and fixed-interpretation proper names, as I think this makes for conceptual clarity.

Some context for these chapters: As background, the reader will already be familiar with a Fitch-style system for propositional logic (pretty similar to The Logic Book‘s system, but with an absurdity constant and EFQ). The reader will also have done a lot of prior work on the language of QL, at least in an initial way,  hopefully coming to these chapters with a decent understanding of the quantifier/variable notation, and a lot of practice at translations. They won’t, however have met yet the identity predicate, and QL= proofs will come later.

14 thoughts on “Natural deduction for quantifier logic”

1. Hi Dr. Smith,

This may have come up in an earlier post, but how do you feel about replacing “wff” with “formula”? I get the impression that this is the direction that newer logic books have been moving in (e.g. Chiswell & Hodges and Leary & Kristiansen), and it has the benefit (in my opinion) of sounding more natural.

On a completely unrelated note: I’ve been trying to learn some classical results in proof theory (specifically, Gentzen’s consistency proof of PA and basic ordinal analysis), but there don’t seem to be many accessible introductions to these topics. The most approachable source I could find is Takeuti’s book, and that’s almost 50 years old. Even the recommendations in your “Teach Yourself Logic” guide tend to come with many qualifications. So if you ever consider writing something like “An Gentle Introduction to Gentzen’s Theorems”, I think it would be a very welcome addition to the literature!

1. A gentle introduction to Gentzen would be great.

In the meantime, one thing I’ve found is a book by Anna Horská called Where is the Gödel-point hiding: Gentzen’s Consistency Proof of 1936 and His Representation of Constructive Ordinals (SpringerBriefs in Philosophy)

It’s ridiculously expensive for an 88 page paperback (£49.99), but you can “look inside” on Amazon UK to see if it looks like what you want, and it should be possible to get a library copy somehow.

2. I indeed once had it mind to write a Gentle Introduction to Gentzen’s Theorems and made a serious start on it. But I fell out of love with the project for quite external reasons of academic politics. I do occasionally wonder about having another bash at it …

As to “wffs”: it’s a matter of brevity.

Simply changing “wff” to “formula” at this stage adds half a page to too many chapters. Why? There’s a lot of text-squeezing already going on in IFL2, with many paragraphs worded to end near the end of a line, with chapters eventually ending at the foot of a page. So any global search-and-replace adds much more to the length of the book than you might expect. CUP are already being very patient with a longer-than-promised book. Of course there is the option of changing “wff” to “formula” AND doing enough rewriting to keep the pagination: but the considerable effort needed to do this without any loss of clarity doesn’t really seem worth it to me. Of all the possible stumbling blocks for the student reader, the use of “wff” seems about the least of my worries!

So “wff” it will have to remain. (Though yes, were I starting rewriting from scratch, with length no issue, I might be tempted to move to “formula”.)

1. I can see a case for ‘formula’. For instance, when talking about programming languages — where the syntactic details matter as much as they do for logic — we don’t go around saying “well-formed expression” or “well-formed statement” all the time. OTOH, you do sometimes have to say a statement, expression, etc is not well-formed / syntactically valid, and I’ve just read the following sentence in the 3 main QL proof chapters:

Let’s remark again, the variable ? can’t already appear quantified in ?(?) or else ∃? ?(?) won’t be a wff.

You’d have to say something about it not being well-formed there.

‘wff’ also has the following nice properties

* It’s short.
* It says what it means and means what it says.
* It reminds us of just what sort of sticklers logicians are.
* No one is going to come along and say the correct plural is ‘wffae’.

So, on the whole, I think ‘wff’ is at least ok, and — given that changing to ‘formula’ now would require looking at many, many pages in the book to check that the change hadn’t messed anything up — I’m inclined to say ‘keep it’.

2. On Ch 31:

General comment, first. This is a masterful exposition of the material, second to none in my reading. That is not flattery; I say it having struggled to teach these points myself to high-school students, and having searched through a fair many baby logic books for help. You are a true teacher, sir!

Three very slight worries, however–purely expositional/pedagogical, not logical:

First, I felt that the expositional tone hit a very mild bump each time you used the phrase ‘suitably inclusive domain’. Perhaps you’ve explained this phrase patiently enough in prior sections that struggling students won’t feel that you’re letting go of their hands for a moment here, in which case all is well. But if not, I wonder if language like ‘a domain that includes Socrates’ would help any strugglers.

Second, on p 295 you have, ‘Rather, to repeat, it is just to consider an individual from the domain while not relying on anything distinctive about it’–and of course similar statements elsewhere. I wonder if a few more students will come to see the light here if you were to add (somewhere) a bit more specifically that you are not relying on anything distinctive about the individual either in selecting it for consideration or in the conclusions you are willing to draw about it. Does that drive the nail right home?

Third, and (slightly) related: In your development of EG-elim, you helpfully note, ‘We can still argue as if by cases by arguing from a representative case, using an arbitrary instance of our existential premiss’, and then again in the statement of the principle, ‘we can infer the claim C from an arbitrary instance of that existential generalization (where C is independent of the particular choice of instance)’.

But in your first example, you explain the process of Alex-introduction in these terms: First, ‘Pick an arbitrary person and dub them ‘Alex’’, and then after some reasoning steps, ‘But our premiss (1) tells us that there is someone who is like Alex in being, as supposed, a pizza-lover’.

There is a very slight disconnect here, which I think might confuse the weaker student. The first-cited formulations suggest that you picked Alex because he/she is a pizza-lover, and that you knew you could find some such Alex to pick because of the already established EG. But then when you work through the example, it seems that you chose Alex arbitrarily–similar language to what you used in UG-intro examples–and then subsequently talk about Alex being known to love pizza because of the EG. Would it not all flow much more cleanly if when you wanted to grab Alex you just said, We know there is one or more pizza-lover, so we pick one of them arbitrarily and temporarily dub them ‘Alex’…?

Finally, I’ll throw in my two bits concerning ‘wff’: First, I do think the distinction between a formula and a well-formed formula is important to keep before the mind’s eye, and ‘wff’ is DEFINITELY preferable to lots of usages of ‘well-formed formula’. Second, as a long-time computer programmer, I would suggest there is another though rather subtle pedagogical plus to using ‘wff’. I.e., if you’re going to work happily in the programming world, you’d better get used to abbreviations lacking vowels which are used so much that most people pronounce them (cf. ‘std’ in C++). AND (back to commenting as a teacher), it can be fun to have pointless little matters of personal preference to have good-natured wars over in the classroom, as between the proponents of ‘wiff’, ‘woof’, and ‘double-you ef ef’ (cf. ‘stood’, ‘ess tee dee’, ‘standard’ in C++). I found as a teacher that such little light touches could brighten the students’ days and ease their drudgery.

1. Many thanks for the initial kind words (at this stage in proceedings, all encouragement to keep going for the final yards of the marathon are very welcome!)

First worry: I’ve slightly rephrased, and put an explicit back reference to §30.3 which talks about choosing sufficiently inclusive domains.

Second worry: I like those additional words and have borrowed them!

Third worry: This was bugging me too (when I realized the disconnect in the current version). I’ve now significantly improved things, I hope!

And I’m going to stick to “wff”s happily enough, for various reasons, including your first.

3. p 298: “So there is some Welsh speaker who isn’t loved by Angharad.”

Would “So there is some Welsh speaker Angharad doesn’t love.” be better?

p 300 (b) could be a bit confusing. Was the m, n, … / middle-of-the-alphabet idea introduced earlier? If so, why isn’t it given in the grey box? And if it’s new, introduced here on p 300, why isn’t it in that grey box or another one nearby?

Also, what sort of thing was the italic ‘n’ used in the grey box on p 298?

p 302: Is (Fn∧Gn) not an instance of (∃zFz∧Gn) just because of the parentheses?

p. 303, C’: Argument C was: “No horses are green. All frogs are green. So no horses are frogs.” Before it’s conclusion, C’ does not seem to be using the ‘obvious glossary’ in which ‘F’ is frog, ‘G’ is green, and ‘H’ is horse. Instead, it seems to be saying Fs aren’t green and Hs are.

p 312, argument K, line (3): should the rule be ∧E rather than ∀E?

p 313-314: unfortunate page break

(I’ll try to look at Chapter 33 later.)

(I haven’t checked any of the section references.)

(I also think I need to look at earlier parts of the book to see how “instance” was defined, and then check the uses in Chs 31 – 33.)

1. About m, n and of the use middle-of-the-alphabet letters for proper names. This is indeed introduced earlier; but I’ve added some backreferences to help keep things clear.

The grey box on p. 298 has been rewritten to eliminate the use of informal italic schematic letters: on reflection adding another layer of symbols here was potentially confusing so your query “what is the italic ‘n’ doing” was a useful prompt!

Re p. 303 Yes, I’d stupidly not chosen the obvious formalization, ‘F’ for frog, etc.

Re p. 312 Yes, silly typo/thinko.

Thanks once again!

4. P.S. on ch 31: Your regimentation scheme for informal quantified sentences is wonderful. Just the right amount of regimentation, and with a light touch.

A few comments on the rest, which I had to skim rather than read properly (and my apologies, but I have entirely skipped the exercises for now):

p 301: ‘although we do have to make a policy choice here about the handling of parameters’. Quibble: Wasn’t the choice about which symbols to use as parameters, rather than how to handle them?

Same page: I’m delighted with how clearly you distinguish syntax and semantics–and help the student understand what those are and which is which and what is which. So I felt a very slight unease when you defined ‘instance’ of a quantified sentence.

Granted, the context is syntactical, or meta-syntactical, which the reader should notice. But I wonder again, for those weaker students, if a few of them might get tripped up here reading semantics into ‘instance’. I.e., Fm is an instance in your terminology of (exists x)Fx, but (exists x)Fx might be true and Fm false–perhaps Fn is true instead. That is, if I’m understanding the passage correctly, your notion of instance is a purely syntactical one, and is in fact in some cases distinct from a semantic notion that one might accidentally label with the word ‘instance’.

What I’m trying to get at: Would it help head off unfortunate confusions, and further strengthen the student’s grasp on the syntax-semantics distinction, to say a little something about this?

p 305: “We are given that something or other is F. Pick an arbitrary representative
a from the domain and suppose that a is F.” Here we have another instance (hmmm) of the slight worry I raised in ch 31. At this point you are sounding more like a mathematician (not meant as a pedagogical compliment), and I see weaker students (in philosophy presumably) getting restive. “Look, if I know there are some black socks in the drawer, and I need a black sock, why wouldn’t I just rummage around and pull out a random black sock? Instead, I’m apparently meant to pull out a random sock, and then NOT look at it to see if it’s black, but just suppose it’s black! There’s something underhanded (-footed?) going on here.”

I would guess that you might be sounding like a mathematician in the very precise way you’re putting this owing to worries about AC and the like–i.e., how these methods scale up to non-denumerable domains and so on. Maybe I’m wrong about that. In any case, if there is some advanced reason for this way of putting things, perhaps you should explain that, just a bit. If not, why not just put this in terms of grabbing a random black sock?

‘Strictly speaking, we could allow occurrences of in earlier, but now completed,
subproofs. However, our ‘always use a new dummy name’ condition (i) is memorable and is the simplest way of ensuring that features in no prior assumptions
(nor in the relevant earlier w↵ 9⇠↵(⇠)).’ Hear, hear! And bravo! I am really liking the way you combine technical rigor with common sense in cases like this, and let the student know what you’re doing. IMO, this is the right way to handle this kind of dilemma in an intro text.

p 327, ‘Pre-Fregean logic had serious difficulties coping with arguments that involve both connectives and quantifiers, or which involve propositions with
multiple quantifiers. We saw how modern quantificational logic can cope
smoothly and naturally with such arguments.’

Just another word of appreciation, prompted by this passage: Thank you for explaining so precisely (in this summary and in the details presented earlier) wherein modern QL advanced over traditional logic, and for not overstating the case in the triumphalistic manner of some. I appreciate the way the passages I’ve read clearly (and helpfully) build up to QL from the syllogistic, using the syllogistic as a useful step up to QL. That is historically much more accurate than the “just ignore traditional logic; we don’t need it” mentality, and psychologically/pedagogically much more sensible.

It is also much more likely to persuade those who have been exposed to the strange opinion that Aristotle’s syllogistic, as polished up by the Schoolmen, is The One True and Universal Logic. I interact a fair bit with various Thomists, neo-Thomists, semi-Thomists, and the like, many of whom make extravagant claims for the syllogistic that are just ignorant of modern logic, and your presentation in this chapter will be useful to me in trying to open their eyes to the logical riches of recent history (one of my weirder hobbies, I suppose).

Thanks for the opportunity to comment on these chapters!

“Wasn’t the choice about which symbols to use as parameters, rather than how to handle them?” Well, the policy choice of whether to use variables again, names again, or a separate kind of symbol is not, so to speak, a mere choice of symbolism (like alternative choices of symbols for the conjunction connective). Hence the “handling”

On “instance”: a good point which has prompted me to add a phrase or two.

On the way the EE rule is glossed (“Pick an arbitrary representative …”): I’ve changed that in line with the prompted changes in the previous chapter. Thanks particularly for nudging me on this.

On the cartoon history, Frege vs traditional logic, I wouldn’t want to say that it is more than a cartoon — but cartoon sketches can be helpful for preliminary orientation.

5. This follows on from my comments above on Chs 31 and 32

1. “Instance”

(1.1) What made me want to check the uses of “instance” was § 32.4 (a), p 304 calling conjuncts and disjuncts “instances”, and (having looked) this seems to be the only place where “instance” is used in this way. It’s only a “think of”, and “instance” seems to be in ‘scare quotes’, so I don’t think there’s a danger of it being seriously misleading; and the idea being expressed here — the similarity between (∧E) and (∀E), and (∨I) and (∃I) — is an important one.

Still, the way the first two paragraphs of (a) shift between different meanings of “instance” has the potential to be slightly confusing. Or do they shift? Perhaps par 2 is still using “instance” in the same scare-quoted sense as par 1. Anyway, the paragraphs are easy enough to understand if you already understand them, but if you don’t?

I think some slight rewording would help, though I’m not sure what the best slight rewording would be. Perhaps, as a fairly minimal change, have the first sentence of the 2nd par say

Now a universal quantification is like a big conjunction (see §28.9), and the (∀E) elimination rule says that, from a universally quantified wff, we can infer any instance of the conjunction it expresses / of the corresponding conjunction.

Perhaps with “big conjunction” in place of plain “conjunction”.

(1.2) Re p 296, (ii): We can still argue as if by cases by arguing from a representative case, using an arbitrary instance of our existential premiss. So suppose Alex is an arbitrary pizza-lover.

It can sound slightly as if Alex, rather than ‘Alex likes pizza’, is the instance. Something such as

So suppose Alex is an arbitrary pizza-lover, and take ‘Alex likes pizza’ as the instance.

would be clearer.

2. Chapter 33

(I haven’t looked at most of the formal proofs in detail.)

p 321 “so why introduce it?” — for the reasons you just gave, and because it’s a more natural expression of the informal argument. [I’m not suggesting you change this; I just don’t quite agree with it.]

p 322, argument D — see my e-mailed comments (from a while back) re Ch 4, though the ambiguity has been resolved.

p 324. I suppose you have to illustrate changing the domain to make a formal derivation easier, but I can’t say I like that tactic when the domain is restricted so much. (You could get much, at least, of the proof simplification by restricting the domain to people, having ‘F’ mean ‘ ① is in the class and can answer every question’ — compare “① is a tail belonging to ②” — and keeping ‘P’ as-is.)

[Again, I’m not suggesting you change this.]

p 328, exercise (d*)(ii): “Γ include” should be “Γ includes”; “then Γ themselves are” is awkward.

6. Thanks again.

Re “instance”, I agree best dropped.

Re “Alex” example, when I look I find it already been rephrased since the last public version in way that avoids the concern.

Re “Why introduce it?” — fair point, so replace with “Let’s keep things simple” or some such.

Re domain restriction example, fair point but judgement call.

Scroll to Top