Well, it’s not back to square one, but it is time to radically re-think plans for the shape of the book (and what will go into it, and what will survive as online supplements). Let me explain the practical problem — as all thoughts and comments will be gratefully received. Being retired has all kinds of upsides, but I can no longer buttonhole colleagues or long-suffering grad students over coffee. So, dear readers, it is your help and advice I seek!
Background info. The first edition of my Intro to Formal Logic has a little under 350 text pages between the prelims and the end matter. Of those, about 270 pages gently cover “core” material that will survive in rewritten/improved form into the second edition (introductory chapters on the very idea of validity; PL languages and truth-table testing for tautological validity; extending this to deal with the conditional; explaining how QL languages work; defining validity for quantificational arguments; adding the identity predicate and functions to formal languages; a bit of philosophical commentary along the way). The other 80 pages cover propositional and quantificational trees.
So the only proof system in IFL1 is a tree system. Tree systems are very elegant and students find them easy to play with. And ease of use is not to be scoffed at (after all, exploring strategies for completing natural deduction proofs might be fun for the mathematically minded teacher, not so much for the more symbol-phobic beginning philosophy student!). Still, many/most teachers think that beginners ought to know something about natural deduction. Indeed I think that too! — but IFL1 started life as my handouts for a first year course given to students who were also going to do a compulsory second year logic course where they would hear about natural deduction, so I then just didn’t need to cover ND in my notes. Still, for a more standalone text, of wider use, very arguably I should cover ND. People certainly complained about the omission from IFL1, and said that that was why they weren’t adopting it as a course text.
Now, I initially believed that in revising IFL I could cut down various parts of the core material, speed up the treatment of trees (in part by repurposing some material as online Appendices) and “buy” myself some thirty pages that way. CUP said they would also allow me an extra 30 pages (maximum, to keep the overall length of the book under 400 pages). So I thought that would give me 60 pages for chapters on natural deduction.
It doesn’t seem to be panning out quite like that ….! In various ways, I hadn’t thought things through properly.
(A) For a start, in reworking the “core” material in the first part of the book — up to the introduction of quantifiers — I seem to have added to the page length here. Yes, the result is clearer, more readable, more accurate … but not shorter. OK, I have been able to speed up the treatment of propositional trees while improving that too. But it balances out, and the first part of the book is more or less just as long as it was. So I’m not hopeful now of being able to save too many core pages and/or cut down the treatment of trees by much. On the other hand, the material on natural deduction for propositional and predicate logic looks as if it will run to about 80 pages, if I aim for a comparable level of clarity, accessibility and user-friendliness.
So instead of adding 30 pages, I’m in danger of adding something like 70 pages to the book, if I cover both trees and natural deduction — and there is probably no way that CUP will wear that.
(B) But in any case, I’m beginning to think that a full-scale treatment of both trees and ND — length apart — is just too weighty for an avowedly introductory book, too daunting. A beginning student shouldn’t come away from a first logic text feeling overwhelmed! Better to have mastered one way of doing things, while having been told that isn’t the end of the story.
So even if I could find and apply Alice’s magical “Shrink me” potion, and could cram everything in, I now not sure that would be a wise way to go. Which leaves me with two options:
- Keep the text as a tree-based text, of much the same size as present, while adding ND chapters as an optional extra available online. (Perhaps using just some of those permitted extra printed pages as an arm-waving introduction to what is spelt out in the online chapters.)
- Make the text a ND-based one, of much the same size as present, while offering tree-based chapters as an optional extra available online. (Perhaps using just some of those permitted extra pages as an arm-waving introduction to what is spelt out in the online chapters.)
Keeping to (1) would, yes, give the world an improved version of IFL, but one still subject to the shortcomings that many perceived, namely that the book wouldn’t have a “real” proof-system.
Moving to (2) is therefore tempting, as I think I can present an intuitively-attractive Fitch-style system in a very user-friendly way.
But yes, I do still think that trees make for a very student-friendly way into a first formal system. But then, I do think natural deduction is more, well, natural — regimenting modes of reasoning we use all the time, so surely something beginners should know about early in their logical studies. And arguably (as now some commenters note below) a grasp of ND is something that students need to be able to carry forward into later studies.
So which way should I jump? Choices, choices …! I’m still mulling this over, and all thought-provoking comments that might help me decide will be most gratefully received.
[As well as comments below, there is a thought-provoking Twitter thread from Greg Restall, @consequently, with others responding.]
20 thoughts on “IFL2, back to the drawing board …”
“Make the text a ND-based one, of much the same size as present, while offering tree-based chapters as an optional extra available online [if you really must!].”
Natural deduction has the advantage of being concerned with deduction, and of being natural.
Trees are great. But they are not especially concerned with everyday deductive reasoning. In my experience, this confuses students. With natural deduction, it is clearer what the aim is: to precisely regiment a key portion of everyday (correct) reasoning.
I would also make a plea for a Gentzen-style system. Natural deduction in the wild is largely Gentzen-style, as others have pointed out. And, if one cares about being precise (e.g. making the use of structural rules explicit), Fitch-style natural deduction is absolutely terrible. Gentzen-style natural deduction paves the way for Gentzen-style natural deduction in sequent style, and to sequent calculi.
I’ll soon be teaching intro logic here in Salzburg: two semesters, loads of natural deduction, Gentzen-style. I’ll write my own handouts.
If the revised version of your book adopts Gentzen-style natural deduction, I’ll definitely make it our official textbook starting from next year.
You’ll be rich!
I can’t agree that natural deduction in the wild is largely Gentzen-style, if “in the wild” means what I think it normally would mean: the reasoning people do in natural language. That is much more like Fitch-style ND. I would also say the reasoning that’s normally seen in maths texts (which is partly in natural language) is more like Fitch ND.
However, re “as others have pointed out”, the two posts above (from the same person) that used “in the wild” were clearly (?) not about arguments in the world outwith logic texts and the like, for they were about “Gentzen-style layout” and “helping the student be competent in reading and writing proofs in that style”.
If that is the “wild” we’re talking about, I would like to see the prevalence of Gentzen-style layout reduced, not increased by another book using it. I find such proofs almost unreadable.
If the choice is between Gentzen-style ND and trees, I pick trees.
If it’s between Fitch-style ND and trees, I’d greatly prefer ND.
Much as though I love Gentzen-style ND — unlike Rowsety Moid! — I do tend to agree that it should be Fitch-style for beginners. I’ll put my thoughts in order and post about this …
Yes, but what do you love Gentzen-style ND for?
I thought Josh P‘s post above was very good on which system was best for different purposes, but it didn’t say much about Gentzen vs Fitch ND.
Oh, and as Smullyan’s books show trees (signed trees) are great for elegant meta-theory.
I’m obviously an extreme minority in leaning toward trees. (Not only that, but I agree with almost all the comments!). So here’s why my lean:
1. I taught mostly non-majors, so that’s the audience I have in mind. Note that it is a much larger audience than majors.
2. I viewed a major goal of the course as teaching the students regimentation into the language of first-order logic with identity.
With my students (exceptions, of course) I couldn’t achieve 2. if I used ND. Trees were easy to motivate (as a search procedure).
Obviously, I wouldn’t have written the first edition as I did if I didn’t share your view about the considerable pedagogic attractions of trees! So if I do plump for ND-in-the-text and trees-as-online-supplement it will be with real regrets … Sigh!
FWIW, I’m a fifth-year bachelor in philosophy writing a thesis on non-classical DEL, so I’m somewhere between “still learning my way around logic” and “mathematically mature.” But, I can definitely share my very recent experience with logic courses pitched at both the undergrad and grad level.
In each of my undergraduate logic courses, I’ve had a different proof-system serve as the centerpiece of the course, and each has left me with greatly different impressions. For introductory (PL, QL) logic, we used Fitch ND, for metalogic (completeness, incompleteness, SOL), we used Fitch and Hilbert, following Enderton (which I have my own opinions about, but I digress). For my first-pass at modal logics, we used a more Gentzen-style ND, a sequent system, and some various calculi. In non-classical, we used primarily tableaux, following Priest. I’m glad I’ve been exposed to all of these, and while the Fitch and Hilbert proofs were certainly frustrating for a time, I’m very glad I have that as my solid foundation to fall back on.
My two-cents would be that moving from ND to tableaux was extremely easy, if not trivial. I can imagine moving the other direction would be more challenging for a time. I suppose one should ask what the ultimate objective of your text is. As a (relatively recent) learner, I found that I made a really quick and clear connection between what’s going on in tableaux proofs and both Kripke and sphere semantics. That connection was completely absent in ND, and I think that it is much easier to reason about modal logics and multi-value logics (e.g. R, B, FDE) with tableaux. I can say the complete opposite about intuitionistic logic (regardless of its status as a modal logic). The constructivist program is much clearer following ND (naturally) and often I found tableaux for IL to feel extremely artificial and non-intuitive, no pun intended. The proof of soundness for PL and FOL are really cool and enlightening in ND, and I think that for students interested in “philosophical logic,” the ND interpretation of conditionals is much closer to the way they turn up in other philosophy classes. The tableaux-sequent connection wasn’t clear to me until I was much more mathematically mature, and while that *is* an extremely exciting connection, it’s more exciting in say, a proof-theory or philosophy of mathematics class, and not intro to symbolic logic. Also, getting to work on programming a tableaux proof-checker was a cool exercise, but again, maybe not something which is very enlightening in a true introductory course.
So, I guess my suggestion would be, definitely include ND and perhaps save tableaux for comparisons, extensions, or for later logics.
Thanks for this long and thoughtful response! Which chimes with the way I’m currently thinking about things …
I also vote for natural deduction, with some nice-looking Fitch-style presentation.
No doubt you already have your own ideas on how it should look, but I do think that at least in the earlier diagrams, when students are still getting the hang of what they represent, there is a large role for tricks of layout – different fonts as you step further to the right to make assumptions, perhaps boxes around chunks at a given distance to the right that start with assumptions and then get somewhere from them (or lightly shaded backgrounds to those chunks), and so on. That sort of thing, plus an explanation along the lines of “Sometimes, in order to make progress, we step to one side and make an assumption to see where it could take us”, could help.
I agree with Leandro. Trees are somewhat easier if you’re nervous about symbols, but natural deduction has proved far more useful elsewhere in philosophy. I would rather put the somewhat greater effort into learning that from the start. Especially if it can be done in a user-friendly way. As you’ve said, the world may not be short on logic books, but I do think there’s space for an intuitively attractive presentation of natural deduction.
Option 2. There are already loads of the tree based book out there, if anyone wants one. And many of us who bought the original book would be willing to fork out for a new version that was based around natural deduction to compliment it. I’d prefer the internal unity and flow of the two separate versions, as opposed to grubbing about online for supplements.
For what the opinion of a simpleton and mathematically rather deficient philosophy student is worth, even though I do find trees easier to understand, natural deduction has proven to be of much greater help to anything logic-related I’ve attempted to study after going through “baby-logic”.
I think this is a very common pattern!
I think one of the benefits of an intro logic course should be to help people to understand and evaluate ‘real-world’ arguments (and also the ones in maths texts), and to make such arguments themselves. I think natural deduction (especially Fitch-style) does that better than trees.
I concur entirely with the suggestion just above from Rowsety Moid. Given your intended audience it seems to me that the Number Two (as of 3 September, that is) approach will provide the more useful background for students regardless of their future need for formal logic. And my personal preference here would be for a Fitch-style presentation.
Any treatment of tableaux that you choose to provide online would provide a nice compare-and-contrast basis for the more curious reader, without detracting from the utility of an earlier version of IFL. And those really enthusiastic about trees could be encouraged to pick up a copy of Smullyan’s First Order Logic.
Well, I’m biased toward 2 [now 1]. But I see why 3 [now 2] tempts, including the desire to value the effort to produce the ND section. Oops, puppy calls, so I’ll expound on my bias later.
I vote for #3 [now #2!]. Started out with Rich Thomason’s Symbolic Logic as the text for my first formal logic course and loved the Fitch-style presentation, missing it terribly as my studies progressed with materials that used mainly Hilbert-style systems. But as most ND in the wild that I run into uses Gentzen-style layout, I wonder if it would be better to use that instead, or at least provide material to help the student read and write fluently in either layout, along the lines of the comparative discussion in your 2010 “Types of Proof System” note.
My first formal logic course 40 years ago used Rich Thomason’s Symbolic Logic, which featured a Fitch-style presentation that I enjoyed very much, and missed as I proceeded further in my studies, which from that point on used texts with Hilbert-style presentations. So I’d vote for 3. But given that most ND proofs in the wild use Gentzen-style layout, I’d want to see some material helping the student be competent in reading and writing proofs in that style as well. Given your size constraints I’m not sure you would find that doable, but you do have of some of that material already in your “Types of proof systems” paper from October 2010. Another possibility would be to simply use Gentzen-style
As far as propositional logic goes, the most potent “shrink me” potion I know requires passing from trees to cacti of the sort I derived from Peirce’s logical graphs. Once the efficiencies of that system are well in hand, one begins to see quantificational logic in a more general light as the logic of higher order propositions.