Peter Smith's Blog, page 26

Super-infinite

Not, then, a maths post on the infinite, but rather a brief but very warm recommendation for Katherine Rundell’s biography of John Donne.

Having no young children around, we have a good rule which helps to keep Christmas relaxed — no exchanges of presents (I can really recommend that too!). But we might wander down to the bookshops a day or two before, and get ourselves a couple of new books we might particularly enjoy reading over the holidays. I went to Heffer’s planning to buy Irene Vallejo’s much praised Papyrus. However, browsing around, I found myself gripped by the first few pages of Super-Infinite: The Transformations of John Donne. So that’s what we bought. And I have now read it with great enjoyment over the last few days. I can certainly see why the book won the Baillie Gifford Prize for Non-Fiction.

Her pieces in the London Review of Books in recent years show that Katherine Rundell can write wonderful prose, of great zest and imaginative power. And she has been a prize-winning author of books for children. She brings her immense gifts for story-telling and her stylistic panache to her academic work as an English scholar, here recounting Donne’s quite extraordinary life and so illuminating his poetry.

Rundell’s title Super-infinite comes from one of Donne’s own new formations, and the paradox is impatient with the limitations of language and what it can be used to describe. The book stages an often thrilling meeting between Donne and Rundell, and its basis is this supple, flexible wordplay in which sentences jump between registers and tones, between this world and the next, between everything and something more. On a portrait of the young Donne, soulful and seductive: ‘He wore a hat big enough to sail a cat in, a big lace collar, an exquisite moustache.’ On his despairs and griefs, and the deaths of his family members and too many of his young children: ‘He was a man who walked so often in darkness that it became for him a daily commute.’ On the violence of his style: ‘He wanted to wear his wit like a knife in his shoe.’ Phrases such as these do the work which literary critics are sometimes afraid to do. They attest to love, and perform that love, and in so doing Rundell returns us to a Donne who is new yet old, nicely paradoxical, his own man and everyone’s.

I can’t put it better than that, from from Daniel Swift’s review in the Spectator. I couldn’t put Super-Infinite down and was even left wanting more.

So now, having devoured the book so quickly, I suppose I will need to wander now down to Heffer’s again, to pick up a copy of Papyrus.

The post Super-infinite appeared first on Logic Matters.

A Christmas card

Another year, another Christmas card. Like last year, this is a picture to be found down the road at the Fitzwilliam Museum, a Nativity long attributed to Bastiano Mainardi, a member of Domenico Ghirlandaio’s workshop and his brother-in-law. But latterly, the Fitz has claimed to see in it the hand of the master himself. Though I do wonder!

Ghirlandaio has been in my mind recently, in part prompted by reading Paola Tinagli’s Women in Renaissance Art (which, among much else, has interesting things to say about the iconography of the great frescos in Santa Maria Novella). And I was prompted to read that book by the references that Maggie O’Farrell gives at the end of her wonderful novel The Marriage Portrait.

The portrait is of the young Lucrezia de’ Medici. Here she is:

Lucrezia is taking her seat at the long dining table, which is polished to a watery gleam and spread with dishes, inverted cups, a woven circlet of fir. Her husband is sitting down, not in his customary place at the opposite end but next to her, close enough that she could rest her head on his shoulder, should she wish; he is unfolding his napkin and straightening a knife and moving the candle towards them both when it comes to her with a peculiar clarity, as if some coloured glass has been put in front of her eyes, or perhaps removed from them, that he intends to kill her. She is sixteen years old, not quite a year into her marriage.

How can you not read on? By some way, my favourite novel of this last year.

Distracting fictions of one kind or another have been necessary more than ever, no? As Eliot says, “Humankind cannot bear very much reality.” To mention just one reality befalling the world, who would have predicted, twelve months ago, that we would be three hundred days into a simmering land war in Europe? Grim times.

But just for a few days let’s try not to dwell too much on that! May you and yours indeed have a very happy Christmas, and I earnestly hope your New Year is a peaceful one.

The post A Christmas card appeared first on Logic Matters.

Why is it so difficult to introduce type theory to the rest of us?

One episode in the Beginning Mathematical Logic Study Guide which I must radically revise in the next edition is the final section on type theories, which was tacked on almost as an afterthought. But it will, indeed, take quite a bit of work to organize a better overview of what is a messy area, and devotees of varieties of type theory are not always the clearest of advocates to help us along.

Egbert Rijke has an Introduction to Homotopy Type Theory coming out soon with CUP. This is a textbook aimed at quite a wide readership; “it introduces the reader to Martin-Löf’s dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. … The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.” Which sounds promising. And a late pre-print can now be downloaded: here’s the link. This may very well be very useful to some readers of this blog, depending on your background. And all credit to Rijke for making his text freely available on the arXiv.

The first part of the book is, as announced, on Martin-Löf’s version of type theory. I’ve dived into this 98 page introduction hopefully. But I can’t, to be honest, say that I have wildly enjoyed the experience — Rijke makes it no easier than others for a conservatively-minded logician to happily find their way in. He acknowledges “Type theory [or at least, type theory of this stripe] can be confusing for people who are new to the subject,” but this means that many of us could do with rather more explanatory chat than we get here. For a small but not insignificant example, right at the outset we are told without further ado that “The expression 𝑎 : 𝐴 is … not considered to be a proposition, i.e., something which one can assert about an arbitrary element and an arbitrary type, but it is considered to be a judgment, i.e., an assessment that is part of the construction of the element 𝑎 : 𝐴.” Is the distinction between a proposition and a judgement transparently clear to you? No. Me neither. (Amusingly, I asked ChatGPT to give a simple explanation of the difference between propositions and judgements in Martin-Löf, and it was a lot clearer. On its first attempt. Though it lost the plot a bit when the question was re-asked.)

Well, meaning is use and all that, and eventually the mists clear somewhat as the notions of proposition and judgement get used later in Rijke. More generally, if you have in fact already encountered a bit of type theory, his explanations will probably serve well for revision and consolidation. But we still await (OK, I still await) a really introductory text on dependent-type-theory-for-old-fashioned-logicians.

The post Why is it so difficult to introduce type theory to the rest of us? appeared first on Logic Matters.

Off to Boston Spa

A small package of hardback copies of Gödel Without (Too Many) Tears has just arrived. One copy I’ll give to the Moore Library here (the university’s main library for the mathematical sciences); another will go to my long-ago college (once a Trinity mathmo, always a Trinity mathmo). A third will be sent off to Boston Spa, because you are legally required to deliver a copy of any book you publish to the British Library.

I suppose it quite likely that this third copy will disappear into the “Additional Storage Building” there, soon never to be seen again. In his strangely rambling but sporadically gripping Bibliophobia, Brian Cummings sets the scene:

From high in the roof, the book robot swings down in an arc in a vertical plane, 10 m or more in a single movement, between stacks ranking 20 m high. It pauses, chooses a stack, then hovers, humming all the time, hunting for the book that it is programmed to find. The scale of the building is difficult for a human to take in. The void is 24 m high by 24 m wide by 64 m long. In any case, the room is not designed for humans. Oxygen levels are kept at 14–15 per cent, which is similar to trying to breathe at the top of a Himalayan mountain. Visitors watch from a special cage, advised to leave after fifteen minutes for their own safety. This library is not a human environment, for it is designed for habitation by books and robots alone.

This is a library for the twenty-first century. … Since space at the main site [of the British Library] at St Pancras in London is at a premium, it is proposed to house books 262 km away and transport them between the Reading Rooms in both locations. Eventually, it is planned that seven million items will be held at the Additional Storage Building in Boston Spa. All of this makes logical sense …

The robotic crane adds a volume to a pile that it is assorting in a plastic bucket. In time, it delivers this to an airlock at the end of the room. There are 140,000 bar-coded containers. It is only at this moment that human intervention takes over, as staff retrieve items from the airlock to send to Reading Rooms, a maximum of 48 hours from ordering to arrival at a London desk. Yet if a human librarian wanted to enter the vault to retrieve a book, using either gigantic ladders or high-wire trapeze artists, it would not be feasible. The books are no longer on fixed shelves ear-marked for their location. Only the crane knows where the books are. It never puts a book back as it found it, absorbing the used item back into the system in the order in which it comes, then remembering where it was. The books are engaged in an eternal game of musical buckets, finding new neighbours, and slotting in accordingly. Only humans need shelf marks any longer: the shelves have gone. The retrieval system is fully automated …

Logical, but the stuff of Borgesian nightmare, squirrelling away everything in a limitless library, including the unread and the unreadable, published in their tens of thousands a year. Libraries, you feel (well, I feel), should be places of more homely comfort — whether in a private room or two with friendly familiars on the walls, or in a congenial public space for browsing along the shelves and reading and working with others similarly occupied.

I’m sure no one would notice if GWT2 never arrived at Boston Spa. But duty calls.

The post Off to Boston Spa appeared first on Logic Matters.

Logicisms and Gödel’s Theorem

Russell famously announced “All mathematics deals exclusively with concepts definable in terms of a very small number of logical concepts and … all its propositions are decidable from a very small number of fundamental logical principles.” That wildly ambitious version of logicism is evidently sabotaged by Gödel’s Theorem which shows that, fix on a small number of logical principles and definitions as you will, you won’t even be able to derive from them all arithmetical truths let alone the rest of mathematics. But how do things stand with latter-day, perhaps less ambitious, forms of neo-logicism?

Second-order logic plus Hume’s Principle gives us second-order Peano arithmetic, and True Arithmetic is a semantic consequence. Buy, for the sake of argument, that Hume’s Principle is in some sense as-good-as-analytic. But how does that help with the epistemological ambitions of a logicism once we see that Gödel’s Theorem shows that second-order semantic consequence is not axiomatizable? Fabian Pregel at Oxford has a very nice piece ‘Neo-Logicism and Gödelian Incompleteness’ coming out shortly in Mind, arguing first that the earlier Wright/Hale canonical writings on their neo-logicism unhappily vacillate, and then that Wright’s more extended discussion of the issue in his 2020 ‘Replies’ (in the volume of essays on his work edited by Alexander Miller) is also unsatisfactory.

I’ll leave Pregel to speak for himself, and just recommend you read his piece when you can. But I was prompted  to look again at Neil Tennant’s recent discussion of his deviant form of neo-logicism (which isn’t Pregel’s concern). Right at the outset of his The Logic of Number (OUP, 2022), Tennant is emphatic that (a) respecting what he calls the Gödel phenomena must be absolutely central in any sort of foundationalist story. But he still wants (b) to defend a version of logicism about the natural numbers (using introduction and elimination rules in a first-order context). So how does he square his ambition (b) with his vivid recognition that (a)?

Tennant  writes:

Logicism maintains that Logic (in some suitably general and powerful sense that will have to be defined) is capable of furnishing definitions of the primitive concepts of this main branch of mathematics. These definitions allow one to derive the mathematician’s ‘first principles’ of number theory as results within logic itself. The logicist is therefore purporting to uncover a deeper source of justification for these ‘first principles’ than just that they seem obvious or self-evident to mathematicians working in the branch of mathematics in question, … [p. 5]

So he is out to defend what Wright 2020 calls the “Core logicist thesis” that at least we can get to the mathematician’s familiar Peano Axioms starting from logic-plus-definitions.  And the methods of his version of logicism, Tennant says,

can be used to determine to what extent the truths in a particular branch of mathematics might be logical in their provenance. So it is more nuanced and discerning than logicism in its original and ambitious form, even when confined to number theory. [pp 5–6]

the formulation of mathematical theories in terms of introduction and elimination rules for the main logico-mathematical operators furnishe[s] a principled basis for drawing an analytic/synthetic distinction within those mathematical theories. [p. 13]

So Tennant is quite happy with an analytic/synthetic distinction being applied within the class of first-order arithmetical truths. In fact, that was already his view back in 1987, when his version of logicism in Anti-Realism and Logic dropped more or less stone-dead from the press (Neil has a terrible habit of trying to take on too much at once, as I’d say he does in his latest book — so that earlier book had something to annoy everyone, and I doubt that very many got to the final chapters!)

Whether Tennant should be happy about the idea of non-logical arithmetical truths concerning logical objects is another question, of course, but that’s the line.

OK: so the criterion of success, for Tennant, is that the logicist

accounts for what kind of things the natural numbers are, and thereby also enables one rigorously (and constructively, and relevantly) to derive as theorems the postulates of ‘pure’ Dedekind–Peano arithmetic, which the pure mathematician takes as first principles for the pure theory of the natural numbers. [p. 51]

NB ‘derive’ — it is syntactic provability as against semantic consequence more generally that is in question.

To be sure, we share Frege’s logicist aspiration to establish at least the natural numbers as logical objects, and to derive the Dedekind–Peano postulates that govern them from a deeper, purely logical foundation. Moreover, we claim to have succeeded where Frege himself had failed, for want of a consistent foundational logical theory. The natural numbers, though sui generis, are logical objects. They are recognizable and identifiable as such because of the role they play in our thoughts about objects that fall under sortal concepts. Our logico-genetic path to the natural numbers has proved to be fully logicist. And it does not take Hume’s Principle as its point of departure. [pp 54–55]

And a bit later — and here we interestingly link up with some remarks of Pregel’s which also touch on what has come to be called “Isaacson’s Thesis” — Tennant writes

Note that it will suffice, for the natural logicist to be able to claim substantial success in this project, to recover the axioms of Dedekind–Peano arithmetic. Indeed, if the natural logicist manages to succeed only on Dedekind–Peano arithmetic, this might offer the explanation sought by Isaacson [1987] of why it is that the axioms of Dedekind–Peano arithmetic are so very ‘natural’. As Isaacson puts it,

… Peano Arithmetic occupies an intrinsic, conceptually well-defined region of arithmetical truth. … it consists of those truths which can be perceived directly from the purely arithmetical content of a categorical conceptual analysis of the notion of natural number.

We have already acknowledged Gödelian incompleteness in arithmetic, and we fully recognize the logical and epistemological challenge posed by it. [p. 69]

So, for Tennant it is an open question how far logicist methods will take us into arithmetic. But that doesn’t impugn, he thinks, its success in giving us the mathematician’s ‘first principles’ for arithmetic. And indeed it might be conceptually important that the logicist method takes us just so far into arithmetic and no further, in the spirit of something like Isaacson’s ideas.

Pregel very reasonably asks the Wright-style neo-logicist

In particular, what account is the Neo-Logicist to offer of the analyticity status of the semantic consequences of HP that are not deductive consequences? Are they analytic as well, though for a different reason? Or synthetic? And how do we account for the fact that different possible choices of second-order deductive systems mean different formulas get categorised as ‘core’?

Tennant would bite the bullet for his version of logicism — they’re synthetic. And his logical framework is first order, so he doesn’t hit the second problem.

OK, that’s all mostly tangential to Pregel’s concerns with the canonical version of neo-logicism. But the point at which they both touch on Isaacson is interesting and suggestive — though since Tennant isn’t tangling with second-order logic, he avoids some of the worries Pregel rightly raise about whether we can deploy something like  Isaacson’s Thesis in the canonical second order framework.

Now, I hasten to add, all this isn’t to say that I outright endorse Tennant’s version of logicism. But do I find myself suspecting that his way with Gödel by limiting the ambitions of a logicism is a “best buy” for someone who wants to rescue something of substantive interest out of a latter-day version of logicism.

And now I’m kicking myself — I have just remembered that I meant to change a footnote about neo-logicism in Gödel Without (Too Many) Tears having read Neil when his book came out, and I forgot to do so before publishing the second edition last month. Bother!

The post Logicisms and Gödel’s Theorem appeared first on Logic Matters.

Avigad MLC — 5: More on FOL

Following on from the interesting Chapter 6 on cut-elimination, there’s one further chapter on FOL, Chapter 7 on “Properties of First-Order Logic”. There are sections on Herbrand’s Theorem, on the Disjunction Property for intuitionistic logic, on the Interpolation Lemma, on Indefinite Descriptions and on Skolemization. I’m not going to dwell on this chapter, though, which I think most readers will find hard going. Hard going in part because, apart from perhaps the interpolation lemma, it won’t this time be obvious from the off what the point of various theorems are.

Take for example the section on Skolemization. This goes at pace. And the only comment we get about why this might all matter is at the end of the section, where we read:

The reduction of classical first-order logic to quantifier-free logic with Skolem functions is also mathematically and philosophically interesting. Hilbert viewed such functions (more precisely, epsilon terms, which are closely related) as representing the ideal elements that are added to finitistic reasoning to allow reasoning over infinite domains.

So that’s just one sentence expounding on the interest  — which is hardly likely to be transparent to most readers!

Avigad’s sections in this chapter are of course technically just fine and crisply done, and can certainly be used as a good source to consolidate and develop your grip on their cluster of topics if you already have met the key ideas. But to be honest I wouldn’t recommend starting here.

OK: The chapters to this point take us some 190 pages into MLC — they form, if you like, a book within the book, on core FOL topics but with an unusually and distinctively proof-theoretic flavour. But to repeat what I’ve said more than once before, I suspect that a reader who is going to happily navigate and appreciate the treatments of topics here will typically need rather more background in logic than Avigad implies. (So when I get round to revising the Beginning Mathematical Logic Study Guide, these opening chapters will find their place in the suggested more advanced supplementary readings.)

Next up: a group of chapters on primitive recursion, on PRA, and on first-order arithmetics more generally. At a first glance, these look perhaps more accessible. But watch this space!

The post Avigad MLC — 5: More on FOL appeared first on Logic Matters.

Meeting Leibniz on the white road.

The non-fiction, non-logic, book which I have most enjoyed this year is the one I have just finished, Edmund de Waal’s remarkable The White Road (from 2105). I was enticed by the jacket description — the author “sets out on a quest – a journey that begins in the dusty city of Jingdezhen in China and travels on to Venice, Versailles, Dublin, Dresden, the Appalachian Mountains of South Carolina and the hills of Cornwall to tell the history of porcelain. Along the way, he meets the witnesses to its creation; those who were inspired, made rich or heartsick by it, and the many whose livelihoods, minds and bodies were broken by this obsession. It spans a thousand years and reaches into some of the most tragic moments of recent times.” It is indeed a quite remarkable read, intriguing and then — when it touches on some of the human disasters of the last century — distressing and moving. As you would expect from The Hare with Amber Eyes or Letter to Camondo, it is quite wonderfully well written — de Waal’s often short, beautifully crafted, paragraphs as carefully arranged as those white porcelain pots of his in their vitrines. Which makes the later pages all the more telling.

I hadn’t expected to bump into Leibniz on the road that takes us to seventeenth century Chinese porcelain and the attempts of the Jesuit missionaries to discern its secrets. But then I didn’t know that one of the few books Leibniz published in his lifetime was the Novissima Sinica — the very latest news from China! Unlike a Descartes who thinks that what is most fundamental is common to us all and is available through rational reflection, Leibniz is committed to the idea that the growth of knowledge will come from bringing together different perspectives, different ways of thinking, about our shared universe. So he has an extensive correspondence with the Jesuit mission, and (to quote de Waal) writes that

all this activity around China … is ‘un commerce de lumière’; enlightenment stretching both ways. This is a tremendous idea and a beautiful image, one of an equality of concerns, a correspondence of civilisations, of light.

As Leibniz writes to his friend Sophie, the wife of the elector of Hanover:

I will thus have a sign placed at my door with these words: bureau of address for China, because everyone knows that one only has to address me in order to learn some news. And if you wish to know about the great philosopher Confucius … or the drink of immortality which is the philosopher’s stone of that country, or some things which are a little more certain, you only have to order it.

He is one of the gatekeepers. If you want to know about Chinese mathematics, the I Ching as a coding of chance events, Chinese characters and their relationship to hieroglyphs, you go to him. Leibniz has been to visit Father Francesco Grimaldi in Rome, just back from the emperor Kangxi’s court, and written up copious notes on fireworks, glass and metal. I realise to my surprise that my hero, the father of rationalism, is anxious to keep ahead in this new, congested field of China Studies.

So Leibniz knows about the problem of porcelain. Later, he corresponds with the mathematician Ehrenfried Walter von Tschirnhaus, who has a sideline experimenting on how to create porcelain here in Europe. And the extraordinary story continues, that was all new to me, as I followed The White Road. 

The post Meeting Leibniz on the white road. appeared first on Logic Matters.

Mastodon, maybe: Twitter, not so much

Twitter could be pretty informative and entertaining, and I’d occasionally tweet posts myself. But the Elon Musk takeover seems to be Bad News on a number of fronts. So, like many, I’m backing off for the time being, though I’ve not deleted my account yet — the Musk era might or might not last. Hence I’ve removed the Twitter feed from the footer that shows on Logic Matters pages (when using a computer or tablet browser).

Instead, I’ll post occasional tweet-sized music-related snippets in the same place — about new CDs, old CDs I’ve been re-listening to, YouTube video links, etc.

Again like many, I’ve joined a Mastodon server, and there’s now a link in the footer to @PeterSmith@mathstodon.xyz. I’m seeing more mathsy stuff and fewer cats and otters. Still exploring who to follow in the wider fediverse. But so far, I’m enjoying the atmosphere and the occasional distractions.

The post Mastodon, maybe: Twitter, not so much appeared first on Logic Matters.

Avigad MLC — 4: Sequent calculi vs tableaux?

Jeremy Avigad’s book is turning out to be not quite what I was expecting. The pace and (often) compression can make for rather surprisingly tough going. And there are few pauses for broader reflection on what’s going on. Take for example the section on Skolemization (which I’ll get to in the next post). This goes at pace, and is probably fairly testing if you’ve never seen this idea before. And the only comment we get about why this might all matter is at the end of the section, where we read:

The reduction of classical first-order logic to quantifier-free logic with Skolem functions is also mathematically and philosophically interesting. Hilbert viewed such functions (more precisely, epsilon terms, which are closely related) as representing the ideal elements that are added to finitistic reasoning to allow reasoning over infinite domains.

So that’s just one sentence expounding on the interest  — which is hardly likely to be transparent to most readers!

Still, I’m cheerfully pressing on through the book, with enjoyment. As I put it before, I’m polishing off some rust — and indeed acquiring bits of new knowledge at other points. So, largely as an aide memoire for when I get round to updating the Beginning Mathematical Logic Guide next year, I’ll keep on jotting down a few notes, and I will keep posting them here in case anyone else is interested.

MLC continues, then, with Chapter 6 on Cut Elimination. And the order of explanation is, I think, interestingly and attractively novel.

Yes, things begin in a familiar way. §6.1 introduces a standard sequent calculus for (minimal and) intuitionistic FOL logic without identity. §6.2 then, again in the usual way, gives us a sequent calculus for classical logic by adopting Gentzen’s device of allowing more than one wff to the right of the sequent sign. But then A notes that we can trade in two-sided sequents, which allow sets of wffs on both sides, for one-sided sequents where everything originally on the left gets pushed to the right of sequent side (being negated as it goes). These one-sided sequents (if that’s really the best label for them) are, as far as I can recall, not treated at all in Negri and von Plato’s lovely book on structural proof theory; and they are mentioned as something of an afterthought at the end of the relevant chapter on Gentzen systems in Troelstra and Schwichtenberg. But here in MLC they are promoted to centre stage.

So in §6.2 we are introduced to a calculus for classical FOL using such one-sided, disjunctively-read, sequents (we can drop the sequent sign as now redundant) — and it is taken that we are dealing with wffs in ‘negation normal form’, i.e. with conditionals eliminated and negation signs pushed as far as possible inside the scope of other logical operators so that they attach only to atomic wffs. This gives us a very lean calculus. There’s the rule that any with atomic counts as an axiom. There’s just one rule each for , , , . There also is a cut rule, which tells us that from and we can infer [image error] (here is notation for the result of putting the negation of in negation normal form).

And Avidgad  now proves twice over that this cut rule is eliminable. So first in §6.3 we get a semantics-based proof that the calculus without cut is already sound and complete. Then in §6.4 we get a proof-theoretic argument that cuts can be eliminated one at a time, starting with cuts on the most complex formulas, with a perhaps exponential increase in the depth of the proof at each stage — you know the kind of thing! Two comments:

The details of the semantic proof will strike many readers as familiar — closely related to the sounds and completeness proofs for a Smullyan-style tableaux system for FOL. And indeed, it’s an old idea that Gentzen-style proofs and certain kind of tableaux can be thought of as essentially the same, though conventionally written in opposite up-down directions (see Ch XI of Smullyan’s 1968 classic First-Order Logic). In the present case, Avigad’s one-sided sequent calculus without cut is in effect a block tableau system for negation normal formulas where every wff is signed . Given that those readers whose background comes from logic courses  for philosophers will probably be familiar with tableaux (truth-trees), and indeed given the elegance of Smullyan systems, I think it is perhaps a pity that A misses the opportunity to spend a little time on the connections.A’s sparse one-sided calculus does make for a nicely minimal context in which to run a bare-bones proof-theoretic argument for the eliminability of the cut rule, where we have to look at a very small number of different cases in developing the proof instead of having to hack through the usual clutter. That’s a very nice device! I have to report though that, to my mind, A’s mode of presentation doesn’t really make the proof any more accessible than usual. In fact, once again  the compression makes for quite hard going (even though I came to it knowing in principle what was supposed to be going on, I often had to re-read). Even just a few more examples along the way of cuts being moved would surely have helped.

To continue (and I’ll be briefer) §6.5 looks at proof-theoretic treatments of cut elimination for intuitionistic logic, and §6.6 adds axioms for identity into the sequent calculi and proves cut elimination again. §6.7 is called ‘Variations on Cut Elimination’ with a first look at what can happen with theories other than the theory of identity when presented in sequent form. Finally §6.8 returns to intuitionistic logic and (compare §6.5) this time gives a nice semantic argument for the eliminability of cut, going via a generalization of Kripke models.

All good stuff. But I hope it doesn’t sound too ungrateful to say that a student new to sequent calculi and cut-elimination proofs would still do best, I think, to read a few chapters of Negri and von Plato (for example) first, in order to later be able get a lively appreciation of §6.4 and the following sections of MLC.

The post Avigad MLC — 4: Sequent calculi vs tableaux? appeared first on Logic Matters.

The Pavel Haas Quartet, at Wigmore Hall, online

It makes for a striking stage presence, Veronika Jarůšková with her mass of golden hair and a golden yellow dress catching the stage lights,  the rest of the quartet in the most subdued of subfusc. And there’s a lot of drama in the performances too. But in one respect, the way the quartet play couldn’t be further from what is visually suggested — the balance, the closeness of the ensemble, the intense way they listen to each other, is as ever remarkable. So here they are, from a Wigmore Hall concert last week, playing Haydn’s Op. 76 No. 1, Prokofiev’s second String Quartet No. 2, and then Pavel Haas’s String Quartet No. 2 (that’s the one with percussion in the final movement). On this occasion, I thought, the Prokofiev was especially fine: it is difficult to imagine the deeply affecting Adagio being played better.

Veronika Jarůšková founded the Pavel Haas Quartet in 2002, and she is the only remaining member from the original four — though she was soon able to swap cellists with the Skampa quartet, so was joined by her husband Peter Jarusek in 2004. There were then some changes of second violin until the quite excellent Marek Zwiebel joined in 2012. It seemed then that the Quartet was happily settled in a steady state. It must have been a great blow to them when their founder violist Pavel Nikl felt he had to leave the Quartet in 2016 because of family illness. Since then there have been — for whatever reasons, the internal dynamics of a quartet must always be complicated — more changes in the viola seat than they could possibly have wanted. But for a few months now, it has been occupied by another Czech, Karel Untermüller — who looks on stage such a stolid figure, but whose playing strikes me as wonderfully good. His ability to have fitted into the Quartet’s style so seamlessly, so quickly, is rather extraordinary. Let’s hope it now works for the four of them in the long term.

The unsettled recent state of the Quartet must mean that recording plans are on hold for now. But Veronika Jarůšková, Peter Jarusek and Boris Giltburg are going into the studio this month (I think) to record Dvořák trios together. The Czech concerts where they have performed these have had rave reviews. So another terrific CD to look forward to in 2023!

The post The Pavel Haas Quartet, at Wigmore Hall, online appeared first on Logic Matters.