Exactly what you choose to put into a first formal logic course for philosophers, and the level of coverage you try to achieve, will be constrained by so many considerations which vary from university to university that there can’t possibly be a one-size-fits-all way of doing things. Have the kids already had an “informal logic/critical reasoning” module? How many lecturing hours have you got? Is there a system of frequent small-group tutorial classes backing up the lectures to go through exercises (and how much extra teaching can be done by TAs in that way)? Is this the only formal logic course offered in the first couple of years or is there a follow-up course in the second year (so it isn’t so much a question of *what* to teach as *when* to teach it)? What proportion of the class can be expected to have the equivalent of a top grade in A-level (high school) maths? What proportion are likely to be rather symbol-phobic humanities students? And so it goes …

I suppose, though, that we can agree — can we? — that *part* of what we’ll want to cover at some level in first course consists in topics such as these (put very roughly, so as not to prejudge too many choices on details of approach):

- Basic ideas about deductive validity (and related notions like logical consistency and logical necessity) and the contrast between deductive and good-but-not-deductively valid inference. Ideas about the way deductively valid arguments can fall into patterns sharing the same form, etc.
- The initial case of arguments relying on the connectives and/or/not; the ideas of a tautology and of tautological entailment; truth-table testing. You’ll want to connect this to important informal ideas like proof-by-cases, reductio-ad-absurdum, etc.
- Relatedly, we need to explain a tidy formal language for regimenting this propositional logic, getting over the idea of strict syntactic formation rules, and the idea of interpretations/valuations for the language.
- Along the way, we’ll have to say something about use and mention, quotation conventions and so on. And about the use of object-language variables vs schematic variables added to our English meta-language.
- Now add informal reflections on varieties of conditionals, and considerations about which inferences are intuitively valid or otherwise for different kinds of conditional (e.g. when can we contrapose?). Also informal thoughts about ‘only if’ and ‘if and only if’. Then consider prospects for adding a workable conditional to our truth-functional language, expanding the truth-table test etc.
- Now broadening our scope, we want to consider quantificational arguments. So we need to explain and motivate the usual sort of quantificational language QL (initially without identity and functions), again explaining the syntax very carefully and at least giving an informal understanding of the idea of an interpretation of the language (and hence of quantification validity as truth-preservation on any interpretations).
- We want students to be confident in handling the language QL when they meet it in use elsewhere, so we are going to need to spend quite some time getting them happy with translation/transcription/regimentation (whatever you want to call in) from English into the formal language and back again.
- Some informal discussion of examples of valid and invalid inferences of QL, and relation to vernacular arguments.
- Now add identity. Discussion of what we can now translate using identity. Russell’s theory of descriptions. Ideally something about functions too.

I should add (prompted by David Makinson’s congenial comment below) that we’ll also want students early on to get a smidgin of knowledge about set notation and basic ideas, and perhaps a few ideas about probability too. If you have to wrap these topics too into the first “logic” course (in my case, I didn’t have to do that, as there were separate mini-courses on them), then things are getting even more crowded.

Now note that, as yet, we’ve said *nothing* about a formal deductive system, whether natural deduction (Fitch-style, Lemmon-flavoured, Gentzen style), tableaux, or — perish the thought! — axiomatic. Yet we have *already* got a pretty substantial menu to get through. And if you are going to cover it properly and in an interesting way, keeping the majority of your class on board, then the material I’ve mentioned so far is necessarily going to take up a goodly amount of time. In fact, I guess this part of the menu used to occupy two-thirds of my lecturing time in a 24 lecture course. So the question “what formal system to use” became for me “what can we usefully do in maybe seven or eight lectures”

Now, I was ridiculously fortunate in my last years of logic teaching. I was in Cambridge, where we can do our very best to pick the brightest/most promising students, and where we can demand (and get) very intense levels of term-time work, and set vacation work too. The students got a lot of first year logic lectures, with back-up examples classes taught by enthusiastic grad students. Even so, and despite the fact that I intentionally aimed the lectures at the non-mathematical majority, and we didn’t go out of our way to set nasty tripos questions at the end of the year, it was clear that quite a few even of these students find even the stuff I’ve mentioned (before we tackle a formal system) surprisingly tough. Lots of course sail through, but I learnt that, even in Cambridge, it is only too easy to under-estimate how foreign all this kind of thing is to many students, however smart they are. So the question in fact became “what can I usefully do in maybe seven or eight lectures, with students many of whom find thinking formally quite tough, without entirely losing too many people?”

I have been following Peter’s discussion of the relative merits of different kinds of layout for natural deduction, and am also looking forward to the next instalment comparing their pedagogical merits with those of semantic decomposition trees (aka tableaux). His remarks so far correspond to my own experience.

But at the same time, I feel that these comparisons, important though they are, should not distract attention from a basic pedagogical question: what should an introductory course in formal logic, offered in a philosophy department, be doing? Is cultivating the skill of constructing natural deductions or decomposition trees sufficiently important to take a significant place in the limited time available?

It is my conviction that students of philosophy – indeed of any discipline where abstract reasoning plays a part – need to master a broad range of formal tools as they progress in their studies. Logic is just one of them; equally important tools are basic notions of sets, relations, functions, recursive definitions and inductive proofs – these not only over the natural numbers but also, and indeed especially, in their non-numerical or ‘structural’ forms. To this list one may add a bit about trees, as simple graphic devices in themselves. Elementary finite probability is also indispensable as a formal tool for any student of philosophy.

Moreover, there is a case for teaching all of these (other than probability) before getting seriously into logic, for two reasons.

One is that the routine verifications that one carries out for basic properties of sets, up to say the correspondence between equivalence relations and partitions, provide a great training ground for practice in non-numerical deduction, so that the students without much high-school mathematics can become used to doing it in a transparent context before being asked either to fully formalize it or to philosophize about it. They will already be carrying out for themselves, in disciplined English, conditional proofs, contrapositions, reductio ad absurdum, and proof by cases, and able to recognize their utility and spirit when later taught to reproduce them in unremittingly formal terms.

The other reason is that the nuts and bolts of basic set theory are needed for a proper articulation and understanding of any system of formal logic, as also for proving even simple things about it. For example, on the semantic level truth-value assignments to sentence letters are functions, which are extended to valuations by structural recursion, on which we can then piggy-back to make inductive proofs about truth-functional logic. On the syntactic level, the set of all well-formed formulae is also defined recursively. So is the set of all theorems of a formal axiom system, being the closure of the set of axioms under the relations specified by the derivation rules; inductive proof based on that recursive definition will play a part in almost anything that we show about the axiom system. Trees are useful in logical context other than semantic decomposition: even bracketing in a formula is rendered conceptually transparent by writing the formula itself as a syntactic tree of its sub-formulae; derivations can be displayed as trees as well as annotated sequences; and so on.

In brief, in my view, an introductory logic course for students of philosophy should not be just about logic, but about formal methods in general. It will profitably be alert to logical subtleties from the very beginning, but may well end, rather than begin, with a systematic treatment of the subject.

Of course, such an approach has its costs. In order to deal with all those topics in one year one must cut elsewhere, and the prime candidates for that are the time-intensive acquisition of skill in constructing fully formalized natural deductions or semantic decomposition trees (which can be tricky in the first-order context). Many instructors would be reluctant to make such cuts in a game that they enjoy playing. There are even some philosophers who would regard the approach as ‘ontologically incorrect’, feeling that we should not be corrupting the youth by bringing suspect entities, such as sets, into the picture until they have been given a clean bill of philosophical health in later courses. For them, introductory logic should be taught pure, without the assistance of any tools from beyond its own boundaries, even if that slows down the exposition and limits what can be said clearly and concisely. But such bootstrapping is, in my view, neither pedagogically helpful nor philosophically justified.

> Now note that, as yet, we’ve said nothing about a formal deductive system, whether natural deduction (Fitch-style, Lemmon-flavoured, Gentzen style), tableaux, or — perish the thought! — axiomatic.

I’m a computer science Ph.D. student in PL theory. As such, I’ve had to pick up a passing understanding of proof systems; however, I have not seen a succinct comparison of the terms you use. For example, I am constantly plagued by the question “Are the proof rules I see in papers ‘natural deduction’ or are they ‘sequent calculus’ or are they something else entirely?”

Would it be possibly for you to write a post with examples (of both rules and completed proofs) of the 5 systems you described, and mention how “sequent calculus” is related to all this?

Thank you!