Peter Smith's Blog, page 111

Introducing Homotopy Type Theory

Yes, Homotopy Type Theory is the latest, greatest, thing (we are told). Yes, a free book is available, following on from a major year-long program at the Institute for Advanced Study at Princeton in 2013-13, and this will tell you lots about the current state of play. And yes, you too started the book and found it pretty impenetrable. What on earth is going on?

Help is at hand.

Robert Harper at CMU ran a grad course last semester, ‘Introducing Homotopy Type Theory’. Notes written up by his students are online. So too are videos of his lectures (use the “stay on the web” option if visiting the site on an iPad). This all looks a pretty good way in if you are still curious about the HoTT phenomenon.

Introducing Homotopy Type Theory.

Yes, Homotopy Type Theory is the latest, greatest, thing (we are told). Yes, a free book is available, following on from a major year-long program at the Institute for Advanced Study at Princeton in 2013-13, and this will tell you lots about the current state of play. And yes, you too started the book and found it pretty impenetrable. What on earth is going on?

Help is at hand.

Robert Harper at CMU ran a grad course last semester, ‘Introducing Homotopy Type Theory’. Notes written up by his students are online. So too are videos of his lectures (use the “stay on the web” option if visiting the site on an iPad). This all looks a pretty good way in if you are still curious about the HoTT phenomenon.

Gödel Without (Too Many) Tears, 2014 version

I’ve made a start updating the notes Gödel Without Tears.

The previous version of the notes was downloaded nearly three thousand times in the last twelve months: so it certainly seems worth putting in the effort to produce a better version, and to get the notes to integrate better with the new edition of my Gödel book.

Some months ago, I rashly said I might try to run some kind of informal online course based on GWT. But unexpected pressures on my time have made that impossible. I’ll only be able to continue updating the notes at irregular intervals. However, you can leave comments on the GWT page to report typos or unclarities. And if you (or your students) post more substantive queries in a sensible form on math.stackexchange then almost certainly someone (quite possibly me!) will answer them.

Edmund de Waal at the Fitz

Image linked from Apollo Magazine’s article ‘Fragile Histories’ by Jon Sanders

There’s a wonderful small exhibition ‘On White: Porcelain Stories from the Fitzwilliam Museum’ by Edmund de Waal at the Fitz until Sunday 23 February 2014. There are three works by de Waal himself, and a series of cases in which he chooses some favourite pieces of porcelain, and comments illuminatingly on their significance and strangeness. A delight if you are in Cambridge and want to escape the madness of the town centre in the sales.

A Christmas card

Gentile Da Fabriano (c. 1370 – 1427), Navity, Uffizi

All good wishes for a happy and peaceful Christmas

Intro to Formal Logic: seventh time lucky?

My Introduction to Formal Logic was published in 2003, and CUP’s initial print run was rather large, so I didn’t get the chance to correct the inevitable typos and thinkos until a reprint in 2009. By that time, needless to say, there were quite a few little presentational things I wanted to change, so I slipped in a load of minor rewritings too. This revised version has been reprinted a number of times. (Oh yes, but of course, I’m making an absolute fortune …)

Along the way, Joseph Jedwab kindly sent me an embarrassingly long list of further errors in the revised printings (I have to put my hand up to having introduced quite a number of these in making the “improvements” in the second printing: thankfully, they were nearly all minor typos). Eventually I had the opportunity to make the needed further corrections, and I’ve just picked up the seventh printing from CUP bookshop. I hope this latest version is a heck of a lot cleaner than the previous ones. Fingers crossed.

A revised printing is not a new edition with a new ISBN, so I’m afraid you can’t put in a bookshop request for the seventh printing and be guaranteed to get one. But eventually the new version will propagate through the distribution system, and jolly good it is too. Or at any rate, reading through while making corrections and looking for any that Joseph Jedwab had missed (none, as far as I could find), I found I didn’t actually hate the book. Distance lends enchantment, eh?

TYL, #19: the Teach Yourself Guide reorganized and updated

Sooner than I was planning, there’s now yet another update for the Teach Yourself Logic Guide. So here is Version 9.4 of the Guide (pp. iii +  72).  

The main change — though it is a significant one, which is why it is worth propagating this new version ahead of schedule — is that the Guide has been reorganized to make it easier to navigate, and hopefully less daunting. Topics on the standard “mathematical logic” curriculum (of interest of mathematicians and philosophers alike) are now separated more sharply from topics likely to be more specialized interest to some philosophers. I’ve also added comments on books by Devlin, Hodel, Johnstone, and Sider.

As I’ve said before, do spread the word to anyone you think might have use for the Guide. As always, there’s a stable URL for the page which links to the latest version, http://logicmatters.net/students/tyl/. You can reliably use that link in reading lists, or on your website’s resources page  for graduate students, etc.

On Sider’s Logic for Philosophy — 2

Suppose that you have some background in classical first-order logic, and want to learn something about modal logic (including quantified modal logic) and, relatedly, about Kripke semantics for intuitionistic logic. Then the second half of Sider’s Logic for Philosophy certainly aims to cover the ground, and it will tell you about formal theories of counterfactuals too. How well does it succeed, especially if you skip the first half of the book and dive straight in, starting with Ch. 6?

These later chapters in fact seem to me to work fairly well (assuming a logic-competent reader). Compared with the early chapters with their inconsistent levels of coverage and sophistication, the discussion here develops more systematically and at a reasonably steady level of exposition. There is a lot of (acknowledged) straight borrowing from Hughes and Cresswell, and student readers would probably do best by supplementing Sider with a parallel reading of that approachable classic text. But if you want a pretty clear explanation of Kripke semantics together with an axiomatic presentation of some standard modal propositional systems, and want to learn e.g. how to search systematically for countermodels, Sider’s treatment could well work as a basis. And then the later treatments of quantified modal logic (and some of the conceptual issues they raise) are also lucid and tolerably approachable.

This is a game of two halves then. Before the interval, Logic for Philosophy is pretty scrappy and I wouldn’t recommend it. After the interval, when Sider plays through some standard modal logics, things look up. I wouldn’t have him at the top of the league for modality-for-philosophers (see the current version of the Guide for preferred recommendations); but Sider’s book-within-a-book turns in a respectable performance.

On Sider’s Logic for Philosophy — 1

It hasn’t been mentioned yet in the Teach Yourself Logic Guide, so I’ve predictably been asked a fair number of times: what do I think about Ted Sider’s Logic for Philosophy (OUP 2010)? Isn’t it a rather obvious candidate for being recommended in the Guide?

Well, I did see some online draft chapters of the book a while back but wasn’t enthused. Still, it is time to take a look at the published version. So here goes …

The book divides almost exactly into two halves. The first half (some 132 pages), after an initial chapter ‘What is logic?’, reviews classical propositional and predicate logic and some variants. The second half (just a couple of pages longer) is all about modal logics. I’ll look briefly at the first half of the book for this post, and leave the second half (which looks a lot more promising) to be dealt with a follow-up.

OK. I have to say that the first half of Sider’s book really seems to me to be rather ill-judged (showing neither the serious philosophical engagement you might hope for, or much mathematical appreciation).

Let’s start with a couple of preliminary points about discussions very early in the book.   (1) The intended audience for this book is advanced philosophy students, so presumably students who have read or will read their Frege. So just what, for example, will they make of being baldly told in §1.8, without defence or explanation, that relations are in fact objects (sets of ordered pairs), and that functions are objects too (more sets of ordered pairs)? There’s nothing here about why we should treat functions that have the same graph as the same, let alone anything about  why we should actually identify functions with their graphs. We are equally baldly told to think of binary functions  as one-place functions on ordered pairs (and the function that maps two things to their ordered pair …?). Puzzled philosophers might well want to square what they have learnt from Frege — and from the Tractatus —  with modern logical practice as they first encountered  it in their introductory logic courses: so you’d expect a second level book designed for such students would not just uncritically rehearse the standard identifications of relations and functions with sets without comment (when, ironically, good mathematics texts often present them more cautiously).

(2) We get a pretty skewed description of modern logic anyway, even from the very beginning, starting with the Ps and Qs. Sider seems stuck with thinking of the Ps and Qs as Mendelson does (the one book which he says in the introduction that he is drawing on for the treatment of propositional and predicate logic). But Mendelson’s Quinean approach is actually quite unusual among logicians, and certainly doesn’t represent the shared common view of ‘modern logic’. I won’t rehearse the case again now, as I’ve explained it at length here. But students need to know there isn’t a uniform single line to be taken here.

OK: the kind of carelessness shown here — and there’s more of the same — isn’t very encouraging, and is surprising given the intended readership. But that wouldn’t matter too much, perhaps, if the treatment of formal syntax and semantics is good. So let’s turn to the core of the early chapters: how well does Sider do in presenting formal details?

He starts with a system for propositional logic of sequent proofs in what is pretty much the style of Lemmon’s book. Which as anyone who spent their youth teaching a Lemmon-based course knows, students do not find user friendly. Why do things this way? And how are we to construe such a system? One natural way of officially understanding what is going on is that such a system is a formal meta-theory about what follows from what in a formalized object-language. But no: according to Sider sequent proofs aren’t metalogic proofs because they are proofs in a formal system. Really? (Has Sider not noticed that in his favourite text, Mendelson, the formal proofs are all metalogical?)

Anyway, the philosophy student is introduced to an unfriendly version of a sequent calculus for propositional logic, and then to an even more unfriendly Hilbertian axiomatic system. Good things to know about, but probably not when done like this, and certainly not as the main focus of a course for the non-mathematical moving on from baby logic. And it is odd too — in a book addressed to puzzled philosophers — not to give significantly more discussion of how this all hangs together with what the student is likely to already know about, i.e. natural deduction and/or a tableau system. Further, the decisions about what technical details to cover in some depth and what to skim over are pretty inexplicable. For example, why are there pages tediously proving the mathematically unexciting deduction theorem for axiomatic propositional logic, yet later just one paragraph on the deep compactness theorem for FOL, which a student might well need to know about and understand some applications of?

Predicate logic gets only an axiomatic deductive system (apparently because this approach will come in handy in the second half of the book — I’m beginning to suspect that the real raison d’être of the book is indeed the discussion of modal logic). Again, I can’t think this is the best way to equip philosophers who might have a perhaps shaky grip on formal ideas with a better understanding of how a deductive calculus for first-order logic might work, and how it relates to informal rigorous reasoning.  The explanation of the semantics of a first-order language isn’t bad, but not especially good either. So — by my lights — this certainly isn’t the go-to treatment for giving philosophers what they might need.

True, a potentially attractive additional feature of this part of Sider’s book is that it does contain discussions about e.g. some non-classical propositional logics, and about descriptions and free logic.  But e.g. the more philosophically important issue of  second-order logic is dealt with far too quickly to be useful. And at this stage too, the treatment of intuitionistic logic is also far too fast. So the breadth of Sider’s coverage here goes with superficiality.

I could go on. But the headline summary about the first part of Sider’s book is that I found it (whether wearing my mathematician’s or philosopher’s hat) irritatingly unsatisfactory. There are  better options available as outlined in the Guide (e.g. David Bostock’s Intermediate Logic gives similar coverage in a more philosopher-friendly way if you want something more discursive, and Ian Chiswell and Wilfrid Hodges’s Mathematical Logic despite its title is very accessible if you want something in a more mathematical style — read both!).

Comments from those who have used/taught/learnt from Sider’s book?

On Sider’s Logic for Philosophers — 1

It hasn’t been mentioned yet in the Teach Yourself Logic Guide, so I’ve predictably been asked a fair number of times: what do I think about Ted Sider’s Logic for Philosophy (OUP 2010)? Isn’t it a rather obvious candidate for being recommended in the Guide?

Well, I did see some online draft chapters of the book a while back but wasn’t enthused. Still, I am more than overdue to take a look at the published version. So here goes …

The book divides almost exactly into two halves. The first half (some 132 pages), after an initial chapter ‘What is logic?’, reviews classical propositional and predicate logic and some variants. The second half (just a couple of pages longer) is all about modal logics. I’ll look briefly at the first half of the book for this post, and leave the second half (which looks a lot more promising) to be dealt with a follow-up.

OK. I have to say that the first half of Sider’s book really seems to me to be ill-judged (showing neither the serious philosophical engagement you might hope for, or much mathematical appreciation).

Let’s start with a couple of preliminary points.   (1) The intended audience for this book is advanced philosophy students, so presumably students who have read or will read their Frege. So just what, for example, will they make of being baldly told in §1.8, without defence or explanation, that relations are in fact objects (sets of ordered pairs), and that functions are objects too (more sets of ordered pairs)? There’s nothing here about why we should identify functions that have the same graph, let alone anything about  why we should actually identify functions with their graphs. We are equally baldly told to think of binary functions  as one-place functions on ordered pairs (and the function that maps two things to their ordered pair …?). Puzzled philosophers might well want to square what they have learnt from Frege — and from the Tractatus —  with modern logical practice as they first encountered  it in their introductory logic courses: so you’d expect a second level book designed for such students would not just uncritically rehearse the standard identifications without comment (when, ironically, good logic texts often present them more cautiously).

(2) We get a pretty skewed description of modern logic anyway, even from the very beginning, starting with the Ps and Qs. Sider seems stuck with thinking of the Ps and Qs as Mendelson does (the one book which he says in the introduction that he is drawing on for the treatment of propositional and predicate logic). But Mendelson’s Quinean approach is actually quite unusual among logicians, and certainly doesn’t represent the shared common view of ‘modern logic’. I won’t rehearse the case again now, as I’ve explained it at length here. But students need to know there isn’t a uniform single line to be taken here.

The kind of carelessness shown here isn’t very encouraging (and there’s more of the same). But what about when Sider turns to looking at formal details? He starts with a system for propositional logic of sequent proofs in what is pretty much the style of Lemmon’s book. Which as anyone who spent their youth teaching a Lemmon-based course knows, students do not find user friendly. Why do things this way? And how are we to construe such a system? One natural way of understanding what is going on is that the system is as a formalized meta-theory about what follows from what in a formal object-language. But no: according to Sider sequent proofs aren’t metalogic proofs because they are proofs in a formal system. Really? (Has Sider not noticed that in his favourite text, Mendelson, the formal proofs are all metalogical?)

So the philosophy student is introduced to an unfriendly version of a sequent calculus for propositional logic, and then to an even more unfriendly Hilbertian axiomatic system. Good things to know about, but not when done like this, and certainly not as the focus of a course for the non-mathematical. And it is odd — in a book addressed to puzzled philosophers — not to give significantly more discussion of how this all hangs together with what the student is likely to already know about, i.e. natural deduction and/or a tableau system. (And we might have expected, too, more discussion of the way the conception of logic changed between e.g. Principia and Gentzen, from being seen as regimenting a body of special truths to being seen as regimenting inferential practice.) Further, the decisions about what technical details to cover in some depth and what to skim over are pretty inexplicable. For example, why are there pages tediously proving the mathematically unexciting deduction theorem for axiomatic propositional logic, yet later just one paragraph on the deep compactness theorem for FOL, which students might really need to know about and understand some applications of?

Predicate logic is dealt with by an axiomatic system only (apparently because this approach will come in handy in the second half of the book — I’m beginning to suspect that the real raison d’être of the book is indeed the discussion of modal logic). Again, I can’t think this is the best way to equip philosophers who have a perhaps shaky grip on formal ideas with a better understanding of how a deductive calculus for first-order logic might work. The explanation of the semantics of a first-order language isn’t bad, but not especially good either. So — by my lights — this certainly isn’t the go-to treatment for giving philosophers what they might need.

True, a potentially attractive additional feature of this part of Sider’s book is that it does contain discussions about e.g. some non-classical propositional logics, and about descriptions and free logic.  But e.g. the more philosophically serious (and mathematically interesting) issue of  second-order logic is dealt with far too quickly to be useful. And at this stage too, the treatment of intuitionistic logic is far too fast. So the breadth of Sider’s coverage here goes with superficiality.

I could go on. But the headline summary about the first part of Sider’s book is that I found it (whether wearing my mathematician’s or philosopher’s hat) irritatingly unsatisfactory. David Bostock’s Intermediate Logic similar coverage is much better.

Comments from those who have used/taught/learnt from Sider’s book?