Peter Smith's Blog, page 20

Big Red Logic Books …

If you have downloaded a PDF copy of one of the Big Red Logic Books, found it useful, and have been thinking you might buy a printed paperback (or even a hardback), then now might be the moment to do so!

Amazon have announced that the printing costs of their KDP print-on-demand service will go up next month (for the first time in six years, apparently: whatever we think of Amazon, they haven’t been price-gouging on this service). Since I price the paperbacks more or less at cost to me, rounding up just a bit, it could well be that the price I have to charge will need to increase. So hurry, hurry, while the lower prices remain!

IngramSpark who print the hardbacks of IFL and GWT have already raised their printing prices (for the UK and EU in particular) to the point I have been losing money on each copy of IFL. So those prices have already had to go up by a little. But I note that — today at any rate — Amazon UK are still selling the hardback of IFL at the old price of £20 (as against £22.50). And they have an offer on the hardback of GWT, selling that for £9.75 (instead of £15), which is a bargain, though I say so myself!

I’ve reached the point where I can seriously think about another Big Red Logic Book, a paperback version of Category Theory I (it come in a bit over 200 pages, but I hope under £5). I’ll try to put it out in the world by the end of next month as a minimal-cost sort-of-beta-version, alongside the freely downloadable PDF, since a substantial number of people do find it much nicer to work from a printed copy. And indeed, if you have a properly designed PDF, it is almost no work to set up another KDP print-on-demand book. Hopefully making the draft available in hard copy will help increase the quantity of feedback/comments/corrections I get. When that paperback is sorted, I’ll then move on to having a serious bash at Category Theory II. Oh what fun!

But logical matters have been going much more slowly than I’d hoped since we got back from Perugia, with the after-effects of Covid taking a significant toll on Mrs Logic Matters and even more so on me. Things have thankfully improved quite a bit in recent days, however, and — fingers crossed — life is returning much more to ‘normal’. So, in particular, I hope I’ll be able to hit that self-imposed end-of-June deadline. We’ll see …

The post Big Red Logic Books … appeared first on Logic Matters.

Categories for the Working Philosopher: 15–18

I’ll be brief. I’m going to skip the fifteenth piece, ‘Application of Categories to Biology and Cognition’ by Andrée Ehresmann: this reader made absolutely nothing of it. The next piece by David Spivak on ‘Categories as mathematical models’ (downloadable here) is pretty empty of serious content, the notion of ‘model’ in play being hopelessly vague. This is followed by Hans Halvorson and Dimitris Tsementzis on ‘Categories of scientific theories’ (downloadable here) which proceeds at such a stratospheric level of abstraction as to cast no light at all on the sort of issues in the philosophy of science that back in the day used to interest me. The final paper is by our editor, Elaine Landry, ‘Structural realism and category mistakes’ is disappointing in a different way. Landry has written thought-provoking pieces about category theory elsewhere (e.g. here and here): but this present piece has the flavour of a narrower-interest journal article replying to particular target papers rather than the sort of more general-interest essay appropriate for this sort of collection.

Heavens! Haven’t I been curmudgeonly? But I confess I started pretty sceptical about claims about the wider significance of category theory (once we go beyond the world of pure mathematics/logic — and perhaps functional programming): and on the evidence of this book, I remain as sceptical. And happy enough to be so: there is some lovely maths in e.g. the Elephant as far as I understand it, and lovely maths is good enough for me!

If you want to read more judicious(?) responses to Categories for the Working Philosopher, you could try Neil Barton’s review or the review by Chris Kapulkin and Nicholas Teh. Obviously, those reviewers are nicer and more generous than I am! But life is short …

The post Categories for the Working Philosopher: 15–18 appeared first on Logic Matters.

In concert: Menahem Pressler plays Schubert

There can only be one choice of musician this week, Menahem Pressler who died on 6th May at the age of 99. He played with the wonderful Beaux Arts Trio for 53 years (leaving a stunning series of recordings of the core repertoire). And when they eventually disbanded, and Pressler was 84, he launched another career as a soloist.

We heard him a few years later at a very memorable concert in the intimate Peterhouse Theatre in Cambridge, when he played Beethoven’s A-flat major sonata, Op. 110, Debussy’s Estampes, and then Schubert’s last piano sonata D. 960. As I wrote at the time “He talked touchingly at the beginning of the evening, and this was evidently music that meant a great deal to him. Pressler’s … desire to communicate with his audience is undimmed. The Schubert in particular was very affecting: in the second movement, the poignancy of an old man now 87 playing the searing music of a young man facing early death was almost too much to take.”

The photo here is of him with Elisabeth Brauß, characteristic of them both. And Pressler was by all accounts a wonderful teacher and encourager of young players, and held in much affection.

What to choose of his to watch and listen to again? There is a wonderful too brief excerpt here of the Beaux Arts playing the slow movement of the Schubert B flat Trio — their CD recording is so fine. But perhaps for sheer joy, I have to pick this performance he gave with Quatuor Ébène at his 90th birthday celebration, of Schubert’s Trout Quintet. What a delight.

The post In concert: Menahem Pressler plays Schubert appeared first on Logic Matters.

Categories for the Working Philosopher: 11–14

In fact I am only going to really comment (and that only briefly) on one of these four papers. For two of them relate to quantum mechanics; and to my great regret I quite lost my grip on such matters many years back. Here, Samson Abransky writes on ‘Contextually: On the borders of paradox’; and Bob Coecke and Aleks Kissinger contribute ‘Categorical quantum mechanics I: causal quantum processes’. Both papers can be downloaded from the arXiv and you can chase them up. And if you want to know more about Bob Coecke and Aleks Kissinger’s take on quantum mechanics, they have a very large book Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning (CUP, 2017) whose opening chapters are pretty accessible.

Back in the Landry collection, another paper is an eight-page note by the late Joachim Lambek on a ‘Six-dimensional Lorentz category’ (again the piece is downloadable). This, however, seems quite out of place in this volume. And indeed the author himself concludes ‘The two extra dimensions of time had been introduced for the sake of mathematical elegance and I have not settled on their physical meaning. For a while I had hoped that they might help to incorporate the direction of the spin axis, but did not succeed to make this idea work’ — hardly a ringing endorsement of the project. Best forgotten as far as I can see.

Which leaves James Owen Weatherall’s ‘Category theory and the foundations of classical space-time theories’: again, a version of this paper is downloadable.

I don’t know quite what Elaine Landry asked of her contributors. In her preface, however, she writes that ‘this book aims to bring the concepts of category theory to philosophers working in [a variety of] areas …
Moreover, it aims to do this in a way that is accessible to a general audience.’ And Weatherall’s piece is indeed clear and engaging. But does he actually show categorial ideas doing essential work?

His topic is various classical field theories which have, in an intuitive sense, “excess content” (they are, as it is said, gauge theories), and the aim is to use categorial ideas to analyse this notion of excess content. Without going into details here, the discussion is interesting and persuasive about the differences between various gauge theories. He sums up:

I have reviewed several cases in which representing a scientific theory as a category of models is useful for understanding the structure associated with a theory. In the context of classical space–time structure, the category theoretic machinery merely recovers relationships that have long been appreciated by philosophers of physics; these cases are perhaps best understood as litmus tests for the notion of “structure” described here. In the other cases, the new machinery appears to do useful work. It helps crystalize the sense in which [versions of classical Newtonian gravity and of electromagnetic theory] have excess structure, in a way that clarifies an important distinction between these theories and other kinds of gauge theories, such as Yang–Mills theory and general relativity. It also clarifies the relationship between various formulations of physical theories that have been of interest to philosophers because of their alleged parsimony. These results seem to reflect real progress in our understanding of these theories — progress that apparently required the basic category theory used here.

But the last claim does seem to overshoot. The basic category theory in question is just the invocation of the notion of a functor as a map between different models and their automorphisms, plus the idea that different functors can preserve different amounts of information, a general idea which is entirely available to someone who has met no category theory at all. In fact, Weatherall himself admits as much at the beginning of his paper:

Although some of the results I describe in the body of the chapter are non-trivial, the category theory I use is elementary and, arguably, appears only superficially.

He does give a promissory note that there are cases in the same neck of the woods to the ones which he discusses ‘where category theory plays a much deeper role’. But as things stand in this paper itself, the category theory indeed seems inessential.

The post Categories for the Working Philosopher: 11–14 appeared first on Logic Matters.

Categories for the Working Philosopher: 7–10

In Vol. 12 of the Handbook of Philosophical Logic (Springer 2005), John L. Bell contributed a long piece on ‘The development of categorical logical’ (some 62 pages, plus a 10 page bibilography, with another 8 pages of background from category theory). Here’s an online version. That piece starts with a historical sketch, and then gets down to a rather hard-core, compressed, outline of some key ideas and results. I can’t imagine that anyone has found it an easy read: in fact, I’ve thought of it as not so much a source essay to start from but as a target summary, something to aim to get to eventually understand from other readings.

It is disappointing, then, to find that the main contribution on categorical logic in Landry’s collection is a 23 page piece ‘Categorical logic and model theory’ by Bell which is mostly just a series of excerpts from that old longer paper. It doesn’t range as widely, but I’m not sure that is much more readily accessible. Will a logic-minded philosopher who knows some category theory — has tackled, say, Emily Riehl’s Category Theory in Context — get much out of this as it stands? I doubt it. To my mind, then, this is an opportunity missed.

The next paper, the eighth, is again by Jean-Pierre Marquis, ‘Unfolding FOLDS: A foundational framework for abstract mathematical concepts’. The first dozen pages are mostly, as a section title has it, ‘some generalities about abstract mathematical concepts’, with arguments for the claim that traditional set theoretic foundations ‘do not encode abstract mathematical concepts properly’. Category theory, you won’t be surprised to hear, does better; and a theory embracing a hierarchy of 1-categories, 2-categories, 3-categories, …, does better still. And then, Marquis claims, Makkai’s system FOLDS — that’s first-order logic with dependent sorts — is what we need as a formal framework ‘to describe this hierarchy directly and properly’. So in the remaining dozen pages of this paper, Marquis outlines FOLDS.

The opening pages of generalities include a sample of the sort of claims made by some categorial enthusiasts which I hesitate to sign up to. For example, what are we to make of this? —

“Let G be an abstract group.” This is a common way of talking in contemporary mathematics, say in group theory. … Our mathematician certainly thinks that the abstract group G has an underlying abstract set. An abstract set is basically a set whose elements have no structure.

Really? Who, I wonder, goes in for this ‘common’ way of talking? You won’t find the phrase ‘abstract group’ anywhere in e.g. Lang’s Algebra. Nor in Aluffi’s Algebra: Chapter 0 (an interesting case, given the categorial flavouring that Aluffi likes to give to his exposition in that lovely book). You will find a few occurrences at the very beginning of Dummit and Foote’s Abstract Algebra, and they do talk on p. 13 of ‘the notion of an abstract group’. But that can be read equally as ‘the abstract notion of a group’ — the notion we get by abstracting from various cases of permutation groups, symmetry groups and the like. I don’t think they are committed to the idea that there is, as well as those more concrete groups there is another sort of thing, an abstract group made of items which (unlike permutations or symmetries) have no nature of their own. Here’s a quote from another book, a standard undergraduate text, Rotman’s First Course in Abstract Algebra: he has just moved on from talking about permutations to introducing the general notion of a group”

We are now at the precise point when algebra becomes abstract algebra. In contrast to the concrete group Sn consisting of all the permutations of the set X = {1, 2, . . ., n} under composition, we will be proving general results about groups without specifying either their elements or their operation. … It will be seen that this approach is quite fruitful, for theorems now apply to many different groups, and it is more efficient to prove theorems once for all instead of proving them anew for each group encountered. For example, the next proposition and three lemmas give properties that hold in every group G. In addition to this obvious economy, it is often simpler to work with the “abstract” viewpoint even when dealing with a particular concrete group. For example, we will see that certain properties of Sn are simpler to treat without recognizing that the elements in question are permutations.

So yes, our mathematician can often proceed abstracting from a group’s details: but that doesn’t mean that “our mathematician certainly thinks” that they are dealing with an abstract group, something built from elements which actually lack structure.

But maybe, on a more careful reading, that isn’t quite the view that Marquis really wants to attribute to the contemporary mathematician. He has a footnote on p. 141, quoting the French mathematician Maurice Fréchet

In modern times it has been recognized that it is possible to elaborate full mathematical theories dealing with elements of which the nature is not specified, that is with abstract elements. A collection of these elements will be called an abstract set. … It is necessary to keep in mind that these notions are not of a metaphysical nature; that when we speak of an abstract element we mean that the nature of this element is indifferent …

So it isn’t after all that the elements of an abstract group have no structure, but rather that for certain generalizing purposes we are ignoring it. As Marquis comments, approvingly I think, here we have ‘a quote by a mathematician that specifies that the property of being abstract is epistemological rather than ontological’.

But if that’s the line, is it so obvious that good old-fashioned set-theoretic reductionism does ‘not encode abstract mathematical concepts properly’? If talk ‘the’ Klein four group is not to be construed ontologically, as talk about some Dedekind abstraction, an entity over and above all the concretely realized Klein four groups, why can’t we say: a claim of the form ‘the (abstract!) Klein four group is F’ is to be cashed out along the lines of ‘any (set-theoretic?) instantion of a Klein four group is F*’ some some suitable derived F*?

Ok, I can’t pursue this further here. But I’m flagging up that Marquis’s opening discussion about ‘abstract mathematical concepts’, while hinting at interesting issues, to my mind goes too fast to be very satisfactory.

What about the more technical part of the paper, on FOLDS? I can only say that I didn’t find the exposition inviting or leaving me wanting to find out more …

Marquis’s paper may or may not be a success, but at least I can see why the editor thought it belonged in this volume. Not so for the next two papers. A sixty page heavy technical paper by Kohei Koshida on ‘Categories and modalities’ belongs in one of the specialist journals. Similarly for forty pages on ‘Proof theory and the cut rule’ by J. Cockett and R. Seely. Unless I am much mistaken, I imagine the number of readers who will be interested and comprehending will be the same as for most such technical articles. Tiny.

The post Categories for the Working Philosopher: 7–10 appeared first on Logic Matters.

In concert: Concerto Köln play Sammartini

Once upon a time, a full-price classical LPs cost almost £40 at today’s prices. No wonder cheaper labels flourished. And I remember some of those cheaper LPs with great fondness, including a Saga recording of pieces by Giovanni Battista Sammartini (c. 1700 – 15 January 1775). The first piece on the record was this short Symphony in A, played here — with engaging zest — by Concerto Köln.

Sammartini was prolific: if you want to hear another piece by him, this time in the performance on that Saga LP, then try this delightful Symphony In G For Trumpet And Strings. Or if you have time for the whole eighty odd minutes of the excellent concert by Concerto Köln, with pieces by Bach, Vivaldi, Locatelli and Dall’Abaco, then the complete video is here.

And since you asked, the cover of the LP is a self-portrait by Filippino Lippi, so only about three hundred years out of time with the music.

The post In concert: Concerto Köln play Sammartini appeared first on Logic Matters.

Categories for the Working Philosopher: 4–6

The next paper in Landry’s collection is a reprint of a short 2014 Phil. Math. paper by Steve Awodey, ‘Structuralism, invariance, and univalence’. You can download it here.

Awodey’s question concerns the content we can give to what he calls the Principle of Structuralism, that isomorphic objects are identical, when a naive reading makes that Principle simply false. And as the title suggests, Awodey wants to argue that Voevodsky’s Univalence Axiom is the way to make sense of the Principle. This does involve skating at great speed over some ideas from type theory, such as Propositions-as-Types. My sense is that the typical logic-and-phil-maths-minded philosopher is still pretty hazy when it comes to these type-theoretic ideas. However, Awodey’s vigorous advocacy here and elsewhere should perhaps prompt more of us to put in the effort to get up to speed (though sadly, as I’ve complained before, the literature isn’t exactly over-supplied with good introductions to type theory!). So: short but thought-provoking.

The fifth paper is ‘Category theory and foundations’ by Michael Ernst. This might rather naturally have been the first paper in the collection, as it is a lucid state-of-play assessment of debates – some long-running — about the foundational role that category theory may or may not have.

In a previous paper, Ernst himself proved a technical result which in fact changed the state-of-play: he showed that some plausible conditions on what could count as an unlimited all-encompassing category (which all categories belong to) can’t be jointly satisfied. This means that e.g. the complaint that ZFC (plus, for example, some large cardinal axioms) fails to cope with an all-encompassing category is no strike against standard set-theoretic foundations: no consistent theory meets that impossible goal. There is a nice short presentation of Ernst’s result here.

But equally, Adrian Matthias’s well-known arguments that categorial foundations in the shape of ETCS are inadequate for mathematical purposes fail to strike a fatal blow, given the fact that we can extend ETCS in categorially motivated ways to recover a theory which can do everything that can be done by ZFC (or indeed by ZFC plus some large cardinal axioms). Also see again McLarty’s piece in this collection and references there.

So, arguably, both a conventional set theoretic framework and a deviant categorial framework starting from ETCS can be developed into adequate technical foundations for mathematical practice (in some useful sense of ‘foundations’).

But what about the complaint that category theory is not really autonomous but makes use of notions of operation/morphism and collection/objects-combined-into-a-structure which need ultimately to be elucidated in set-theoretic terms? The potentially most interesting part of Ernst’s paper, his §5, discusses this autonomy issue: but to be frank I found the discussion a bit thin. E.g. he touches on Lawvere’s supposedly Cantorian “bag-of-dots” conception of sets which I have always found opaque: and I can’t say I was really helped here. However, that said, this piece is overall definitely worth reading, with useful pointers to relevant debates.

The sixth paper is on ‘Canonical maps’ by Jean-Pierre Marquis. The idea is that there is, out there in mathematical practice, a notion of canonical map which has a reasonably definite use and which can be illuminatingly analysed in categorial terms. There’s a great deal of initial arm-waving but nowhere near enough examples for me (or you?) to latch onto the supposed notion under examination. So I found this entirely unsatisfying. But you can download the paper here, and see if you can get more out of it.

The post Categories for the Working Philosopher: 4–6 appeared first on Logic Matters.

Categories for the Working Philosopher: 1–3

Categories for the Working Philosopher, edited by Elaine Landry (OUP), was first published in 2017, and I briefly noted this collection when it came out as seeming to be a very mixed bag. Since my mind is back on matters categorial, and the book has been recently paperbacked, I thought I’d take another look.

Landry describes the first eleven essays as concerning the “use of category theory for mathematical, foundational, and logical purposes”. The remaining seven pieces are on scattered applications of category theory (though there seems to be nothing on why it has come to be of such central concern to theoretical computer science). I’ll probably only comment here on the earlier essays, and I’ll take them in the published order, starting with the first three.

‘The roles of set theories in mathematics’ by Colin McLarty takes up what is by now a familiar theme — that ZFC radically overshoots as an account of what ‘ordinary mathematics’ requires by way of background assumptions about sets. McLarty in particular takes a look at the set-theoretic preliminaries expounded in two classic texts, by Munkres on topology and Lang on algebra, and comments on their relatively modest character. Now, neither Munkres or Lang gives a regimented summary of his set-theoretic assumptions in axiomatic form: but if we did so, what would it look like? Arguably like ETCS, the theory so neatly presented in Tom Leinster’s well-known ‘Rethinking set theory’ whose aim is, as he puts it, to show that “simply by writing down a few mundane, uncontroversial statements about sets and functions, we arrive at an axiomatization that reflects how sets are used in everyday mathematics.”

Now, ‘ETCS’ is of course short for the ‘Elementary Theory of the Category of Sets’ developed by Lawvere and its original idiom was categorial. But Leinster is at pains to point out that the axioms of this set theory, in his presentation, do not involve any essentially categorial notions — they just talk about sets and functions (without reducing the functions to sets, by the way). McLarty explores a little further in a helpful and interesting way, e.g. telling us more about how variant stronger set theories can be seen as expansions of ETCS.

But I can imagine some thinking that the interest here is primarily set-theoretic rather than in the (apparently dispensable?) categorial idiom. I doubt that McLarty sees it like that! — but then those readers would have probably liked to hear more from him here about quite how he does see ETCS to be more intertwined with category theory.

The next paper is, by my lights, pretentious arm-waving by David Corfield on ‘Reviving the philosophy of geometry’: you can give this a miss.

Next up, Michael Shulman writing about ‘Homotopy type theory: a synthetic approach to higher equalities’. Now, Shulman has elsewhere shown a considerable gift for what you might call the higher exposition — explaining, unifying, organising difficult material. His much-referenced paper ‘Set theory for category theory‘ is indispensable. But this present paper is pretty hard going — surely rather too compressed and allusive (would someone who had never before encountered Einstein’s hole argument get what is going on? more to the point, is the supposedly crucial distinction between the rules of a type theory and axioms of a set theory made transparently clear?). I’ll certainly not try to summarize, then. But despite its density, the piece is helpful enough to be worth struggling with, if you want to get some glimmer of what the programme of homotopy type theory/univalent foundations is.

However, as Shulman tells us at the outset, HoTT is a “surprising synthesis of constructive intensional type theory and abstract homotopy theory” and neither of those is essentially categorial from the off. Indeed, in the foundational text, Homotopy Type Theory: Univalent Foundations of Mathematics, category theory doesn’t get mentioned until p. 377! So we might wonder: interesting though HoTT’s programme is as “a new foundation for mathematics and logic” (in Landry’s words), in what sense exactly is this programme essentially categorial in nature?

The post Categories for the Working Philosopher: 1–3 appeared first on Logic Matters.

Not so fontastic

Another birthday gone. It is, as the t-shirt has it, weird being the same age as old people.

As a present for myself, I sent off weeks ago for the catalogue for the Rijksmuseum Vermeer exhibition, but only opened it on the day. And I’m very glad that I hadn’t instead dropped heavy hints to Mrs Logic Matters that I would really like a copy, because it would have been difficult to hide my initial disappointment.

Many catalogues of major exhibitions are wondrous art-objects in their own right. But this one so strangely isn’t.

Some complaining Amazon reviewers have put this down to the use of a matt paper, but actually I think that’s a mistake. Putting pages side by side with the reproductions in other books on Vermeer we have then — when not placed so as to catch reflections — you can in many cases hardly tell the matt and the slightly glossy pages apart. True, independently of the matt/gloss finish, in a number of cases the colours in this volume seem slightly dulled. But maybe these reproductions are in some sense truer to the paint surface; we have just become so used to seeing paintings rather artificially glowing in modern gallery lighting.

No, I don’t think it is principally the exact level of colour reproduction which makes this catalogue unsatisfactory as a visual object. Rather, there is a very odd choice of a dark, modern, sans serif font. So instead of the extensive blocks of text receding with quiet grace, as in the lovely catalogue for the Fitzwilliam’s Vermeer’s Women a few years ago, we get page after page visually shouting (and with the print overwhelming the inset — and oddly small — supplementary illustrations). If this was a catalogue for an exhibition by Kandinksy, say, it might have worked excellently. But for Vermeer of all artists? It simply looks off-puttingly uncomfortable.

As for the texts themselves — mostly essays on different groups of paintings, written by many hands — some are a bit banal, but mostly they are engaging and illuminating. Which makes it all the more a pity that the mode of typographical presentation is, to my eyes, so very misjudged. I’ve got a bit more used to the look of the book: but it’s not fontastic!

The post Not so fontastic appeared first on Logic Matters.

Avigad’s MLC — First order logic

Last year I wrote a number of posts on Jeremy Avigad’s major recent book for advanced students, Mathematical Logic and Computation (CUP, 2022). I was reading it with an eye to seeing what parts might be recommended in the next iteration of the Study Guide. This is a significantly shorter version combining the posts, now removed, on the first part of the book. A brisker post on the rest of the book will follow.

The first seven chapters of MLC, some 190 pages, form a book within the book, on core FOL topics but with an unusually and distinctively proof-theoretic flavour. This is well worth having. But a reader who is going to happily navigate and appreciate the treatments of topics here will typically need significantly more background in logic than Avigad implies. The exposition is often very brisk, and the amount of motivational chat is variable and sometimes minimal. So — to jump to the verdict — some parts of this book will indeed be recommended in the Guide, but as supplementary reading for those who have already tackled one of the standard FOL texts.

To get down to details …

Chapter 1 of MLC is on “Fundamentals”, aiming to “develop a foundation for reasoning about syntax”. So we get the usual kinds of definitions of inductively defined sets, structural recursion, definitions of trees, etc. and applications of the abstract machinery to defining the terms and formulas of FOL languages, proving unique parsing, etc., but all done in a quite hard-core way. But as JA notes, the reader can skim and skip and return to the details later on a need-to-know basis.

But there is one stand-out decision that is perhaps worth commenting on. Take the two expressions and The choice of bound variable is of course arbitrary. It seems we have two choices here:

Just live with the arbitrariness. Allow such expressions as distinct formulas, but prove that  formulas like these which are can be turned into each other by the renaming of bound variables (formulas which are -equivalent, as they say) are always interderivable, are logically equivalent too.Say that formulas proper are what we get by quotienting expressions by -equivalence, and lift our first-shot definitions of e.g. wellformedness for expressions of FOL to become definitions of wellformedness for the more abstract formulas proper of FOL.

Now, as JA says, there is in the end not much difference between these two options; but he plumps for the second option, and for a reason. The thought is this. If we work at expression level, we will need a story about allowable substitutions of terms for variables that blocks unwanted variable-capture. And JA suggests there are three ways of doing this, none of which is entirely free from trouble according to him.

Distinguish free from bound occurrences of variables, define what it is for a term to be free for a variable, and only allow a term to be substituted when it is free to be substituted. Trouble: “involves inserting qualifications everywhere and checking that they are maintained.”Modify the definition of substitution so that bound variables first get renamed as needed — so that the result of substituting for in is something like . Trouble: “Even though we can fix a recipe for executing the renaming, the choice is somewhat arbitrary. Moreover, because of the renamings, statements we make about substitutions will generally hold only up to -equivalence, cluttering up our statements.”Maintain separate stocks of free and bound variables, so that the problem never arises. Trouble: “Requires us to rename a variable whenever we wish to apply a binder.”

But the supposed trouble counting against the third option is, by my lights, no trouble at all. Why so?

JA is arguably quite misdescribing what is going on in that case.Taking the Gentzen line, we distinguish constants with their fixed interpretations, parameters or temporary names whose interpretation can vary, and bound variables which are undetachable parts of a quantifier-former we might represent ‘’. And when we quantify to get we are not “renaming a variable” (a trivial synactic change) but we are — in one go, so to speak replacing the parameter with a variable and prefixing a linked quantifier, and that complex makes a single semantic unit which has a quite different semantic role from a parameter. There’s a good Fregean principle, use different bits of syntax to mark different semantic roles: and that’s what is happening here when we replace the ‘’ by the ‘’ and at the same time bind with the quantifier ‘’.

So its seems to me that option 1c is in fact very markedly more attractive than JA has it (it handles issues about substitution nicely, and meshes with the elegant story about semantics which has true on an interpretation when is true however we extend that interpretation to give a referent to the temporary name ). The simplicity of 1c compared with option 2 in fact gets the deciding vote for me.

After the chapter of preliminaries, MLC has two chapters on propositional logic (substantial chapters too, some fifty-five large format pages between them, and they range much more widely than the usual sort of introductions to PL in math logic books).

JA’s general approach foregrounds syntax and proof theory. So these two chapters start with §2.1 quickly reviewing the syntax of the language of PL (with as basic — so negation has to be defined by treating as ). §2.2 presents a Hilbert-style axiomatic deductive system for minimal logic, which is augmented to give systems for intuitionist and classical PL. §2.3 says more about the provability relations for the three logics (initially defined in terms of the existence of a derivation in the relevant Hilbert-style system). §2.4 then introduces natural deduction systems for the same three logics, and outlines proofs that we can redefine the same provability relations as before in terms of the availability of natural deductions. §2.5 notes some validities in the three logics and §2.6 is on normal forms in classical logic. §2.7 then considers translations between logics, e.g. the Gödel-Gentzen double-negation translation between intuitionist and classical logic. Finally §2.8  takes a very brisk look at other sorts of deductive system, and issues about decision procedures.

As you’d expect, this is all technically just fine. But I strongly suspect an amount of prior knowledge will be pretty essential if you are really going get much out the discussions here. Yes, the point of the exercise isn’t to get the reader to be a whizz at knocking off complex Gentzen-style natural deduction proofs (for example); but are there quite enough worked examples for the genuine newbie to get a good feel for the claimed naturalness of such proofs? Is a single illustration of a Fitch-style alternative helpful? I’m very doubtful.

To continue, Chapter 3 is on semantics. We get the standard two-valued semantics for classical PL, along with soundness and completeness proofs, in §3.1. Then we get interpretations in Boolean algebras in §3.2. Next, §3.3 introduces Kripke semantics for intuitionistic (and minimal) logic — as I said, JA is indeed casting his net significantly more widely that usual in introducing PL. §3.4 gives algebraic and topological interpretations for intuitionistic logic. And the chapter ends with a pretty challenging §3.5, ‘Variations’, introducing what JA calls generalised Beth semantics. As you can see, a lot is going on here!

Still, I think that for someone coming to MLC who already does have enough logical background (perhaps a bit half-baked, perhaps rather fragmentary) and who is mathematically adept enough, these chapters — perhaps initially minus their last sections — should bring a range of technical material into a nicely organised story in a very helpful way, giving a good basis for pressing on through the book.

The next two chapters of MLC are on the syntax and proof systems for FOL — in three flavours again, minimal, intuitionstic, and classical — and then on semantics and a smidgin of model theory. Again, things proceed at considerable pace, and ideas come thick and fast.

So in a bit more detail, how do Chapters 4 and 5 proceed? Broadly following the pattern of the two chapters on PL, in §4.1 we find a brisk presentation of FOL syntax (in the standard form, with no syntactic distinction made between variables-as-bound-by-quantifiers and variables-standing-freely). Officially, recall, wffs that result from relabelling bound variables are identified. But this seems to make little difference: I’m not sure what the gain is, at least here in these chapters, in a first encounter with FOL.

§4.2 presents axiomatic and ND proof systems for the quantifiers, adding to the systems for PL in the standard ways. §4.3 deals with identity/equality and says something about the “equational fragment” of FOL. §4.4 says more than usual about equational and quantifier-free subsystems of FOL, noting some (un)decidability results. §4.5 briefly touches on prenex normal form. §4.6 picks up the topic (dealt with in much more detail than usual) of translations between minimal, intuitionist, and classical logic. §4.7 is titled “Definite Descriptions” but isn’t as you might expect about how to add a description operator, a Russellian iota, but rather about how — when we can prove — we can add a function symbol such that holds when , and all goes as we’d hope. Finally, §4.8 treats two topics: first, how to mock up sorted quantifiers in single-sorted FOL; and second, how to augment our logic to deal with partially defined terms. That last subsection is very brisk: if you are going to treat any varieties of free logic (and I’m all for that in a book at this level, with this breadth) there’s more worth saying.

Then, turning to semantics, §5.1 is the predictable story about full classical logic with identity,  with soundness and completeness theorems, all crisply done. §5.2 tells us more about equational and quantifier-free logics.  §5.3 extends Kripke semantics to deal with quantified intuitionistic logic. We then get algebraic semantics for classical and intuitionistic logic in §5.4 (so, as before, JA is casting his net more widely than usual — though the treatment of the intuitionistic case is indeed pretty compressed). The chapter finishes with a fast-moving 10 pages giving us two sections on model theory. §5.5 deals with some (un)definability results, and talks briefly about non-standard models of true arithmetic. §5.6 gives us the L-S theorems and some results about axiomatizability. So that’s a great deal packed into this chapter. And at a sophisticated level too — it is perhaps rather telling that JA’s note at the end of the chapter gives Peter Johnstone’s book on Stone Spaces as a “good reference” for one of the constructions!

The same judgement applies, I think, as to the chapters on PL: very good material for someone already on top of the basics, and wanting to consolidate and expand their knowledge, but not the place to start.

One minor comment: I note that JA does define a model for a FOL language in the standard way as having a set for quantifiers to range over,  but with a function (of the right arity) over that set as interpretation for each function symbol, and a relation (of the right arity) over that set as interpretation for each relation symbol. My attention might have flickered, but JA seems happy to treat functions and relations as they come, not explicitly trading them in for set-theoretic surrogates (sets of ordered tuples). But then it is interesting to ask — if we treat functions and relations as they come, without going in for a set-theoretic story, then why not treat the quantifiers as they come, as running over some objects plural? That way we can interpret e.g. the first-order language of set theory (whose quantifiers run over more than set-many objects) without wriggling. JA does in general seem to nicely downplay the unnecessary invocation of sets — though not quite consistently. I’d go for consistently avoiding unnecessary set talk from the off — thus making it much easier for the beginner at serious logic to see when set theory starts doing some real work for us. Three cheers for sets: but in their proper place!

MLC continues, then, with Chapter 6 on Cut Elimination. And the order of explanation here 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 JA 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, if I 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 JA 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 soundness 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 JA misses the opportunity to spend a little time on the connections.JA’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 do have to report though that, to my mind, JA’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.

This is all very good stuff, and I learnt from this. 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 to read the initial chapters of Negri and von Plato (for example) first, if they are later to be able get a lively appreciation of §6.4 and the following sections of MLC.

Following on from the very interesting Chapter 6 on cut-elimination, MLC has 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. This does nicely follow on from the previous chapter, as the proofs here mostly rely on the availability of cut-elimination. I’m not going to dwell on this chapter, though, which I think most readers will find pretty 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 wider interest  — which is hardly likely to be transparent to most readers! It would have been good to hear more.

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

In his Preface, Avigad writes ‘The material here should be accessible at an advanced undergraduate or introductory graduate level’ and implies that having had a prior introduction to logic might be helpful but isn’t necessary for tackling MLC. I rather suspect that teaching at Carnegie Mellon has given our author a distinctly rosy picture of what most advanced undergraduates/beginning graduates can readily cope with! But let’s forget the advertising pitch, and take the book for what it more turns out to be, an advanced text suitable for mathematically apt readers who have already have some background in logic and who want to consolidate/push on. Then there is, as indicated, a lot of interesting material here, presented in an often-compressed, though sometimes perhaps over-compressed, way. I definitely learnt from it. So a bumpy ride but (for the appropriately primed reader) one worth tackling.

The post Avigad’s MLC — First order logic appeared first on Logic Matters.