Peter Smith's Blog, page 60

April 1, 2020

Illusionists of logic

My friend Hugh Mellor sent this on to me, one of the pieces in J.B. Priestly’s Delights, a book of short essays from 1949, another difficult time, mostly about simple pleasures. Or in this case, something a bit more philosophical:



The post Illusionists of logic appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on April 01, 2020 02:45

March 30, 2020

Luca Incurvati’s Conceptions of Set, 1

I’m really pleased to see that Luca Incurvati’s long-awaited Conceptions of Set and the Foundations of Mathematics has now been published by CUP. It’s currently jolly expensive. So let’s hope for an early inexpensive paperback. Happily, though, you will be able now to read an e-version of the book for free if your library has appropriate access to the Cambridge Core platform. So I’m going to assume I’m not the only one with access to the book! — and will dive in and comment slowly, chapter by chapter, over the next few weeks. I’ll be very interested (of course) to hear other readers’ reactions.


The first chapter is titled ‘Concepts and conceptions’. Not that Luca wants to suggest a sharp distinction here between concept and conception. But roughly, to characterize the concept of set is to characterize what someone has to grasp if they are to count as understanding ‘set’ (in the right way). But that characterization will leave open a lot of fundmental questions about the nature of sets and about what sorts of sets there are, about how sets relate to their members, and so on. And our answers to such questions will typically be guided by a conception of sets, which tells us something about what it is to be a set (a story which “someone could agree or disagree with though without being reasonably deemed not to possess the concept” of set). Take for example the iterative conception of sets: you don’t have to have grasped that surprisingly late arrival on the scene to count as understanding ‘set’. (I suppose that we might wonder about the understanding of someone who couldn’t see that the iterative conception, once presented, was at least a candidate for an appropriate conception of the world of sets: but reasoned rejection of the now standard conception would surely not debar you from counting as talking about sets.)


OK, so what does belong to the core concept of set as opposed to a more elaborated conception? Luca suggests three key elements:



Unity: “A set is … a single object, over and above its members.”
Unique decomposition: “A set has a unique decomposition” into its members.
Extensionality: The familiar criterion of identity for sets — sets are identical if and only if they have the same members.

By the way, in talking about members here, it isn’t (I take it) being assumed that we we can call on a prior, fully articulated, notion of membership. The notions ‘set (of)’ and ‘member (of)’ have to be elucidated in tandem — just as e.g.  ‘fusion (of)’ and ‘part (of)’ have to be elucidated in tandem (and similarly for some other pairs).


These three aspects of the concept of set distinguish it from neighbouring ideas. (1) is needed to distinguish sets from mere pluralities — it distinguishes the set of Tom, Dick and Harry from those men. (2) is needed to distinguish sets from mereological fusions which can be carved into parts in arbitrarily many ways. (3) is needed to distinguish the relation between a set and its members, and the relation between an intensionally individuated property and the objects which have the property (different properties can have the same extension).


Let’s pause though over (1). We have two sets of Trollope’s Barchester Chronicles in the house. We can distinguish the two sets of six books, and count the sets — two sets, twelve individual books. One set is particularly beautifully produced, the other was a lucky find in an Oxfam bookshop. In a thin logical sense (if we can refer to Xs, count Xs, predicate properties of Xs, then Xs are objects in this thin sense) the sets can therefore be thought of as objects. But are the sets of books objects “over and above” the books themselves? Trying that thought out on Mrs Logic Matters, she firmly thought that talking of the set (singular) is just talking of the books (plural), and balked at the thought that the set was something over and above the matching books. Does that mean she doesn’t understand talk of a ‘set of books’?


The distinction we need here is the one made by Paul Finsler as early as 1926 in a lovely quote Luca gives:


It would surely be inconvenient if one always had to speak of many things in the plural; it is much more convenient to use the singular and speak of them as a class. […] A class of things is understood as being the things themselves, while the set which contains them as its elements is a single thing, in general distinct from the things comprising it. […] Thus a set is a genuine, individual entity. By contrast, a class is singular only by virtue of linguistic usage; in actuality, it almost always signifies a plurality.


In this sense, I’d say that (as with Mrs Logic Matters and the Trollopian sets) much ordinary set talk is surely class talk, is singular talk of pluralities. Luca cheerfully claims “if I say that the set of books on my table has two elements, you [as an English speaker] understand what I am saying”, I rather suspect that the non-mathematician, non-philosopher (i) is going to find the talk of ‘elements’ really rather peculiar, and (ii) is in any case not going to be thinking of the set as something over and above the two books, there on the table.


There’s little to be gained, however, in spending more time wondering how much set talk “as it occurs in everyday parlance” (as Luca puts it) really is set talk in Finsler’s sense, as characterized by Luca’s (1). I think it is probably less than Luca thinks. But be that as it may. Let’s move on to ask: what is the cash value of the claim that a set (the real thing, not a mere class) is a “genuine [bangs the table!] individual entity” [Finsler], is “a single object, over and above its members” [Luca]?


One key thought is surely that sets of objects are themselves objects in the sense that they too, the sets, can be collected together to form more sets. Suppose someone just hasn’t grasped that sets are the sorts of thing that themselves can straightforwardly be members of sets, would we say that they have fully cottoned on to the idea of sets (in the sense we want that contrasts with Finsler’s classes)?


Let’s take that thought more slowly. Suppose we for the moment take the idea of an object in the most colourless, all-embracing, way — just to mean a single item of some type or another. Then e.g. Fregean concepts are indeed items distinct from the objects that fall under them; fixing the world, there’s a unique answer to what falls under them; and they are individuated extensionally — same extension, same Fregean Begriff. This isn’t the place to assess Frege’s theory of concepts! The point, though, is that (1) talk of a single item distinct from the plurality it subsumes, plus (2) and (3), doesn’t distinguish sets from Fregean concepts. And similarly, I think, if we are to distinguish sets from (extensionally individuated) types in the sense of type theory.


But why should we distinguish Fregean concepts or types from sets? What, apart from some rhetoric and motivational chat is the real difference? Surely, one key difference is that Fregean concepts or types are, well, typed — only certain kinds of items are even candidates for falling under a given Fregean concept, or for inhabiting a given type. Sets are, by contrast, promiscuously formed. Take any assortment of objects, as different in type as you like — the number three, the set of complex fifth roots of one, the Eiffel Tower, Beethoven’s op.131 Quartet [whatever exactly that is!] — and then there is a set of just those things. At least, so the usual story goes.


Maybe that example is a step too whacky, and you could deny that there is such a set without being deemed not to know what sets are. But still, you’ll standardly want to countenance at least e.g. a set whose members are a basic set [either empty or with some urelement], a set with that set as it member, a set with those two sets as its members, etc. The set-forming operation does not discriminate the types of such things, but cheerfully bundles them together.


Isn’t the usual idea, in short, that a set of objects (objects apt for being collected into a set) is itself an object in the sense that it is, inter alia, apt to be collected into a set — indeed, collected alongside those very objects we started from? Whereas e.g. a Fregean concept has objects falling under it, but can’t be regarded as itself another item that could fall under a concept with those same objects — that offends against Frege’s type discipline.


I suppose — well, we’ll see when we come to his discussion of the iterative conception — that Luca could treat the idea of sets being (in a sense) type promiscuous as part of a certain conception of sets, something that elaborates rather than is part of our core concept. Given neither of us think there is a sharp concept/conception distinction to be drawn anyway, it certainly wouldn’t be worth getting into a fight about this. But my feeling remains that if we don’t say something more about how (1)’s understanding of sets as objects allows them to be themselves members of sets alongside other objects, then we won’t have done enough to distinguish the concept of set from the concept of more intrinsically typed items.


To be continued (with some comments on Chapter 1’s conception of ‘conceptions‘)


The post Luca Incurvati’s Conceptions of Set, 1 appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 30, 2020 05:31

Luca Incurvati’s Conceptions of Set — 1

I’m really pleased to see that Luca Incurvati’s long-awaited Conceptions of Set and the Foundations of Mathematics has now been published by CUP. It’s currently jolly expensive. So let’s hope for an early inexpensive paperback. Happily, though, you will be able now to read an e-version of the book for free if your library has appropriate access to the Cambridge Core platform. So I’m going to assume I’m not the only one with access to the book! — and will dive in and comment slowly, chapter by chapter, over the next few weeks. I’ll be very interested (of course) to hear other readers’ reactions.


The first chapter is titled ‘Concepts and conceptions’. Not that Luca wants to suggest a sharp distinction here between concept and conception. But roughly, to characterize the concept of set is to characterize what someone has to grasp if they are to count as understanding ‘set’ (in the right way). But that characterization will leave open a lot of fundmental questions about the nature of sets and about what sorts of sets there are, about how sets relate to their members, and so on. And our answers to such questions will typically be guided by a conception of sets, which tells us something about what it is to be a set (a story which “someone could agree or disagree with though without being reasonably deemed not to possess the concept” of set). Take for example the iterative conception of sets: you don’t have to have grasped that surprisingly late arrival on the scene to count as understanding ‘set’. (I suppose that we might wonder about the understanding of someone who couldn’t see that the iterative conception, once presented, was at least a candidate for an appropriate conception of the world of sets: but reasoned rejection of the now standard conception would surely not debar you from counting as talking about sets.)


OK, so what does belong to the core concept of set as opposed to a more elaborated conception? Luca suggests three key elements:



Unity: “A set is … a single object, over and above its members.”
Unique decomposition: “A set has a unique decomposition” into its members.
Extensionality: The familiar criterion of identity for sets — sets are identical if and only if they have the same members.

By the way, in talking about members here, it isn’t (I take it) being assumed that we we can call on a prior, fully articulated, notion of membership. The notions ‘set (of)’ and ‘member (of)’ have to be elucidated in tandem — just as e.g.  ‘fusion (of)’ and ‘part (of)’ have to be elucidated in tandem (and similarly for some other pairs).


These three aspects of the concept of set distinguish it from neighbouring ideas. (1) is needed to distinguish sets from mere pluralities — it distinguishes the set of Tom, Dick and Harry from those men. (2) is needed to distinguish sets from mereological fusions which can be carved into parts in arbitrarily many ways. (3) is needed to distinguish the relation between a set and its members, and the relation between an intensionally individuated property and the objects which have the property (different properties can have the same extension).


Let’s pause though over (1). We have two sets of Trollope’s Barchester Chronicles in the house. We can distinguish the two sets of six books, and count the sets — two sets, twelve individual books. One set is particularly beautifully produced, the other was a lucky find in an Oxfam bookshop. In a thin logical sense (if we can refer to Xs, count Xs, predicate properties of Xs, then Xs are objects in this thin sense) the sets can therefore be thought of as objects. But are the sets of books objects “over and above” the books themselves? Trying that thought out on Mrs Logic Matters, she firmly thought that talking of the set (singular) is just talking of the books (plural), and balked at the thought that the set was something over and above the matching books. Does that mean she doesn’t understand talk of a ‘set of books’?


The distinction we need here is the one made by Paul Finsler as early as 1926 in a lovely quote Luca gives:


It would surely be inconvenient if one always had to speak of many things in the plural; it is much more convenient to use the singular and speak of them as a class. […] A class of things is understood as being the things themselves, while the set which contains them as its elements is a single thing, in general distinct from the things comprising it. […] Thus a set is a genuine, individual entity. By contrast, a class is singular only by virtue of linguistic usage; in actuality, it almost always signifies a plurality.


In this sense, I’d say that (as with Mrs Logic Matters and the Trollopian sets) much ordinary set talk is surely class talk, is singular talk of pluralities. Luca cheerfully claims “if I say that the set of books on my table has two elements, you [as an English speaker] understand what I am saying”, I rather suspect that the non-mathematician, non-philosopher (i) is going to find the talk of ‘elements’ really rather peculiar, and (ii) is in any case not going to be thinking of the set as something over and above the two books, there on the table.


There’s little to be gained, however, in spending more time wondering how much set talk “as it occurs in everyday parlance” (as Luca puts it) really is set talk in Finsler’s sense, as characterized by Luca’s (1). I think it is probably less than Luca thinks. But be that as it may. Let’s move on to ask: what is the cash value of the claim that a set (the real thing, not a mere class) is a “genuine [bangs the table!] individual entity” [Finsler], is “a single object, over and above its members” [Luca]?


One key thought is surely that sets of objects are themselves objects in the sense that they too, the sets, can be collected together to form more sets. Suppose someone just hasn’t grasped that sets are the sorts of thing that themselves can straightforwardly be members of sets, would we say that they have fully cottoned on to the idea of sets (in the sense we want that contrasts with Finsler’s classes)?


Let’s take that thought more slowly. Suppose we for the moment take the idea of an object in the most colourless, all-embracing, way — just to mean a single item of some type or another. Then e.g. Fregean concepts are indeed items distinct from the objects that fall under them; fixing the world, there’s a unique answer to what falls under them; and they are individuated extensionally — same extension, same Fregean Begriff. This isn’t the place to assess Frege’s theory of concepts! The point, though, is that (1) talk of a single item distinct from the plurality it subsumes, plus (2) and (3), doesn’t distinguish sets from Fregean concepts. And similarly, I think, if we are to distinguish sets from (extensionally individuated) types in the sense of type theory.


But why should we distinguish Fregean concepts or types from sets? What, apart from some rhetoric and motivational chat is the real difference? Surely, one key difference is that Fregean concepts or types are, well, typed — only certain kinds of items are even candidates for falling under a given Fregean concept, or for inhabiting a given type. Sets are, by contrast, promiscuously formed. Take any assortment of objects, as different in type as you like — the number three, the set of complex fifth roots of one, the Eiffel Tower, Beethoven’s op.131 Quartet [whatever exactly that is!] — and then there is a set of just those things. At least, so the usual story goes.


Maybe that example is a step too whacky, and you could deny that there is such a set without being deemed not to know what sets are. But still, you’ll standardly want to countenance at least e.g. a set whose members are a basic set [either empty or with some urelement], a set with that set as it member, a set with those two sets as its members, etc. The set-forming operation does not discriminate the types of such things, but cheerfully bundles them together.


Isn’t the usual idea, in short, that a set of objects (objects apt for being collected into a set) is itself an object in the sense that it is, inter alia, apt to be collected into a set — indeed, collected alongside those very objects we started from? Whereas e.g. a Fregean concept has objects falling under it, but can’t be regarded as itself another item that could fall under a concept with those same objects — that offends against Frege’s type discipline.


I suppose — well, we’ll see when we come to his discussion of the iterative conception — that Luca could treat the idea of sets being (in a sense) type promiscuous as part of a certain conception of sets, something that elaborates rather than is part of our core concept. Given neither of us think there is a sharp concept/conception distinction to be drawn anyway, it certainly wouldn’t be worth getting into a fight about this. But my feeling remains that if we don’t say something more about how (1)’s understanding of sets as objects allows them to be themselves members of sets alongside other objects, then we won’t have done enough to distinguish the concept of set from the concept of more intrinsically typed items.


To be continued (with some comments on Chapter 1’s conception of ‘conceptions‘)


The post Luca Incurvati’s Conceptions of Set — 1 appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 30, 2020 05:31

March 25, 2020

Covered in blue …



So here’s the cover for IFL2 (click for a larger version).  The painting, my choice, is Kandinsky’s Blue Painting (Blaues Bild) from January 1924. It has been slightly cropped by CUP’s designers but I do think it still makes for a good-looking cover. I’m really very pleased with the result.


I’m working away putting answers to end-of-chapter exercises online (currently I’m having fun with quantifier natural deduction).  This is actually rather a good task to have on the go right now. It is distracting enough to keep my mind off other things during a long afternoon stuck at home; but it hardly demands prolonged concentration trying to get my head round Difficult Stuff.  I’m making some very slight improvements to the exercises as I go along which can be incorporated into the final final book version when CUP call for it in a week or two. And so  on we go.


I’d like, though, to get back to thinking about category theory. Here’s one question: category theorists, or some influential ones among them at any rate, seemingly work with a non-standard conception of sets: but what is it, exactly (when you try to cash out the ‘bag of dots’ metaphor that gets trotted out)? As a warm up exercise (although I don’t think he tackles this question) I’m going to be sitting down to read carefully Luca Incurvati’s recent Conceptions of Set and the Foundations of Mathematics. If your library subscribes to the Cambridge Core system, you should be able to get it online. I’ll start posting about this book, chapter by chapter, in the next few days.


 


The post Covered in blue … appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 25, 2020 10:02

March 24, 2020

From a small corner of Cambridge, 2

In the London Review of Books a couple of issues ago, there was a strangely timely review of a book on the plague in Florence in the early seventeenth century. The plague approached the city, only temporarily halted by the natural barrier of the Appenines



On the other side of the mountains, Florence braced itself. The officials of the Sanità, the city’s health board, wrote anxiously to their colleagues in Milan, Verona, Venice, in the hope that studying the patterns of contagion would help them protect their city. Reports came from Parma that its ‘inhabitants are reduced to such a state that they are jealous of those who are dead’. The Sanità learned that, in Bologna, officials had forbidden people to discuss the peste, as if they feared you could summon death with a word. Plague was thought to spread through corrupt air, on the breath of the sick or trapped in soft materials like cloth or wood, so in June 1630 the Sanità stopped the flow of commerce and implemented a cordon sanitaire across the mountain passes of the Apennines. But they soon discovered that the boundary was distressingly permeable. Peasants slipped past bored guards as they played cards. In the dog days of the summer, a chicken-seller fell ill and died in Trespiano, a village in the hills above Florence. The city teetered on the brink of calamity.


By August, Florentines were dying. The archbishop ordered the bells of all the churches in the city to be rung while men and women fell to their knees and prayed for divine intercession. In September, six hundred people were buried in pits outside the city walls. As panic mounted, rumours spread: about malicious ‘anointers’, swirling infection through holy water stoups, about a Sicilian doctor who poisoned his patients with rotten chickens. In October, the number of plague burials rose to more than a thousand. The Sanità opened lazaretti, quarantine centres for the sick and dying, commandeering dozens of monasteries and villas across the Florentine hills. In November, 2100 plague dead were buried. A general quarantine seemed the only answer. In January 1631, the Sanità ordered the majority of citizens to be locked in their homes for forty days under threat of fines and imprisonment.


And so it went (the review is gripping). And so, with some marked similarities though a thankfully much less virulent infection, it goes. The coronavirus lockdown has now reached Cambridge. Probably some days after it should have done, and probably it is still less stringent that it ought to be. The English, or far too many of them it seems, are still not conducting themselves particularly well. Some national myths are being unmade as we watch. Grim times.


The now official lockdown will, I suppose, make relatively little difference to us, at least for the moment. We’ve been ultra-cautious about going out and about in our small corner of the town for the past two weeks. We rather suspect that, like very many, we might in fact already have had the virus in a pretty mild way. Who knows? We’ll have to wait for when an antibody test becomes available, though it would be very good to know. When we feel a bit more lively, DV, time for some serious gardening (Mrs Logic Matters) and decorating.



We were much looking forward to a Wigmore Hall concert a couple of days ago with the countertenor Iestyn Davies and the lutenist Thomas Dunford. But that of course was cancelled like all London concerts. To see what we missed, there are some really nice videos of Iestyn Davies singing on his site here. And looking ahead we’ve had to cancel our usual spring stay in Cornwall, which is a sad (apart from other reasons, they are now rightly strongly asking visitors to stay away). With that missed trip I mind, I picked up again, and read from end to end, a book (not Cornish but at least West Country in theme) that we bought on one trip in the delightful indie bookshop in Falmouth — namely Alice Oswald’s Dart, that follows the river and its people from source to sea. This is a wonderfully ambitious  many-layered, many-voiced, poetic journey full of allusion and mythic echoes and observation of nature and more: no wonder it won the T.S. Eliot Prize. This week’s warm recommendation!



Just when, after lean years, independent booksellers like the Falmouth shop I mentioned seem to have been having doing rather better, they will be hit hard by the lockdown. So do support your favourite ones by giving them orders. There’s a website here listing indie shops offering an online service: book love in the time of coronavirus.

The post From a small corner of Cambridge, 2 appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 24, 2020 08:26

March 22, 2020

Groups and sets

Standard algebra texts define a group to be a set of objects together with a binary operation on those objects (obeying familiar conditions) — or indeed, they define a group to be an ordered pair of a set and a suitable binary function (where ordered pairs and functions are to be treated as sets too, in familiar ways).


But what work is the conventional set talk here actually doing? — is it really doing much more than the set talk back in the days of ‘new math’? Can these sets be treated as Quinean virtual classes? Can we in fact perfectly well think of a group as some objects (plural — or at least one) equipped with a group operation, and drop the set talk in favour of common-or-garden plural locutions?


There are a number of general philosophical issues here about the commitments of various grades of set talk, and about the commitments of plural talk too. But there’s an interesting technical question: how far can we get in group theory before we have to call on substantial ideas from set theory?


Let’s sharpen that question: what issues are there that can readily be understood by a relative beginner in group theory that depend for their answers on set-theoretic matters (e.g. whose answers can depending on the ambient set theoretical principles we countenance?). It is well known, for example, that Shelah showed in 1974 that the Whitehead problem is independent of ZFC. But the beginning student is surely not going to understand the significance of that (indeed picking up a couple of heavyweight standard texts, Dummit and Foote’s Abstract Algebra and Aluffi’s Algebra: Chapter 0, neither even mention the Whitehead problem). So put aside problems at that level. To repeat, then, what student-accessible problems have answers dependent on set theoretic ideas?


One suggestion might be


“Given objects X, is there always a group (X, e, *) with those objects, and some identity e and some group operation *?”


The answer is positive if and only if the Axiom of Choice is true. Though I suppose here we might now have a serious debate about whether the Axiom of Choice is at bottom an essentially set-theoretic principle at all (after all, some plural logics have versions of choice, and then there are type-theoretic versions).


Here’s a perhaps better example. The following


“Take a group G, its automorphism group Aut(G), the automorphism group of that, i.e. Aut(Aut(G)), the automorphism group of that, i.e. Aut(Aut(Aut(G))), etc. Does this automorphism tower terminate (count it as terminating when successive groups are isomorphic)?”


Joel Hamkins has shown that the answer is yes, but the very same group can lead to towers with wildly different heights in different set theoretic universes. (Why should this be, on reflection, no great surprise? — which is not to diminish Hamkins theorem one jot! Because, as he points out, there’s a sense in which going from a group to its automorphism group is ‘going up a level’; and we can play forcing tricks as we go up the levels.)


OK that’s a lovely example. But what others are there? I asked this on math.stackexchange here and the question got a surprising number of up-votes (suggesting I’m not alone in  finding the issue interesting).


And I didn’t get any more problems which are as immediately student-accessible as the automorphism towers problem, rather re-inforcing my guess that you can get a pretty substantial way into group theory without really tangling with set theory (especially if choice principles are assigned to the logic side of the ledger rather than the intrinsically set-theoretic side). But I did get two nice suggestions a notch or two up in sophistication, which you might be interested to see (if you know some algebra).


The post Groups and sets appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 22, 2020 10:49

March 19, 2020

Dale Jacquette’s biography of Frege, again

In a posting here almost a year ago, I was rather scathing about Dale Jacquette’s book  Frege: A Philosophical Biography (surprisingly, to my mind, published by CUP in 2019). But I frankly admitted to having read only a hundred pages or so before giving up on the book. Was I being unfair, then? Did I miss much by not reading on? Or did the book continue in the same hopelessly amateurish and confused way?


It seems the latter. Here’s a review by Wolfgang Kienzler (a shorter version appeared in History and Philosophy of Logic in January this year). Kienzler was evidently no more impressed than I was.


(A nice example of Gricean implicature, from this review: “The author seems to enjoy using as many German words and expressions as possible across his text, and it must be admitted that almost all of them are spelled correctly.” Ouch.)


The post Dale Jacquette’s biography of Frege, again appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 19, 2020 06:44

March 17, 2020

The Lean Theorem Prover

Something to do during your logical self-isolation: find out a little about The Lean Theorem Prover.


I confess I have previously never really “got” the supposed attractions of the likes of Coq. But I stumbled a week or two back over a piece by Thomas Hales on the pros and cons of using the much more recent Lean. There are a lot of cons, but still I was prompted to take a first quick look at the Lean documentation, and then stayed to read on quite far. As you might have predicted of something which Jeremy Avigad has a major hand in, this is really very well written. If you (like me) start with only a shaky grasp on why working in a version of dependent type theory might be a Good Thing, then this is interesting and genuinely illuminating –well worth looking at, even if you don’t find yourself playing with Lean itself for very long.


The post The Lean Theorem Prover appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 17, 2020 14:15

March 16, 2020

From a small corner of Cambridge, 1

Very strange, difficult, stressful times. For some, already the worst of times. So far, we’ve been lucky.


But our world contracts. People our age are now being asked to stay close to home, to reduce social contacts, and so on.  How stern is the injunction? It’s not entirely clear. Fortunately, we live very near the river and Midsummer Common; we can take walks out when the paths are quiet. But I can foresee that we will largely be confined for weeks to this small corner of Cambridge.


In fact, we have been more-or-less self-isolating for a week already, because that seems wisest for us, various things being considered. We’ve already stopped going to cafés, I’ve stopped going to the gym, University of the Third Age classes and walking groups have been suspended. We’re not meeting up with friends. Family are mostly elsewhere anyway. We are used to a very quiet life, so will no doubt cope better than many. But there is a difference between quietness and prolonged isolation. We’ll just have to find some time-consuming and enjoyable house-bound projects.  So, for a start, there’s the decoration of three or four rooms we’ve been meaning to do ever since the builders left. Already there has been an amount of comfort baking — we’ll need to do more home exercise too, to counteract that. And then this isn’t a house without books to read …


I’ll keep you posted about how things go as the weeks roll on.



Talking of books, when I put Emily Thomas’s The Meaning of Travel away alongside other travel books, I found a copy of Eric Newby’s Love and War in the Appenines. I couldn’t remember ever having read it before. Here’s one of the advantages of age; your bookshelves renew themselves!


Newby tells of his adventures as a prisoner of war and then afterwards, when he takes to the mountains, sheltered by courageous Italian peasants, in the process meeting Wanda who later becomes his wife. This perhaps isn’t one of the reflective, philosophically-coloured, travel books: but Newby’s story rattles along as he draws some memorable characters, and sketches both a landscape and a lost way of life. I rattled through it in a few days; a very enjoyable  distraction from these differently troubled times.


 


The post From a small corner of Cambridge, 1 appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 16, 2020 14:55

March 12, 2020

More natural deduction exercises

We are keeping our social distance, ducking out of meetings, avoiding cafés, having at least some food supplies delivered rather than going to the shops, and so on — all in all, erring on the side of caution, given age considerations. Keep calm and carry on. What else can you do?


So I’ve had a  bit more time than expected to plough on with getting answers to IFL2 exercises online (discovering along the way that one of the exercises asked students to prove a falsehood — I live and learn: fortunately I can still change the final final PDF for the book).


By my lights, the key thing for philosophy students is to understand the principles behind a natural deduction system (and ideally, to get some sense of what are the deep ideas, and what are matters of presentational choice). Doing a few exercises no doubt helps understanding. Getting expert at proof-discovery goes beyond what is really necessary. Still, I can’t resist: I have now provided very extensive worked answers — over forty pages — with a lot of hints and tips for proof discovery. You will find the exercises and answers here. I hope they will be of some interest even to those not using IFL2 (e.g. users of forall x).


Exercises for QL natural deduction next … is there no end to the fun?


The post More natural deduction exercises appeared first on Logic Matters.

 •  0 comments  •  flag
Share on Twitter
Published on March 12, 2020 13:37