Archive for the ‘Logic’ Category

Pohler’s Proof Theory

Saturday, February 7th, 2009

I’ve started struggling through Wolfram Pohler’s recent Proof Theory: The First Step Into Impredicativity. And it is, I’m afraid, a struggle — for a textbook exposition “pitched at undergraduate/graduate level”, it is really quite unnecessarily hard going. For example, I can’t imagine that anyone who hasn’t already encountered the idea would have much hope of cottoning on to what is going on with the Veblen hierarchy from the discussion in Sec. 3.4. And even if you are very familiar with completeness proofs for first-order logic, it’s made ridiculously hard work to see what’s going in the completeness proof in Sec. 4.4.

I’ll certainly keep ploughing on through, given the book’s coverage. But not with relish. Why on earth write like this, without the introductory informal motivating comments and explanations of concept definitions and proof ideas that you’d give in lectures? I’m quite baffled that anyone can think that this is the right way to write a book intended for a student readership.

Anonymous comments: I think this is the usual way of writing a math book. Most, if not all, math books are written this way.

I don’t think that’s entirely true. I’m sitting here surrounded my shelves of relatively recent maths books, both pure and applied maths (dating from when I was writing my chaos book ten years ago, or teaching the philosophy of space-time theories). They do illustrate a whole spectrum of modes of presentation from rather relaxed to take-no-prisoners relentless formality. To be sure, there are too many of the latter kind — but it is possible to do better!

Online logic texts resources

Friday, October 3rd, 2008

In case you missed this over at Richard Zach’s blog, here’s a link to an excellent page by Henri Galinon which in turn links to freely available logic texts and surveys of various kinds. Very well worth checking out. [Link updated!]

Mathematics and games

Friday, September 26th, 2008

Of course, the trouble with tackling Wittgenstein is you can bogged down so easily and distracted into various kinds of detective work (sometimes I wonder if half the attraction the sage has for some of his less critical fans is that he offers his readers the pleasure of puzzle-cracking as one tries to track down the sense of the more gnomic utterances). So, I’m still wrestling with Sec. 108 of the Big Typescript, the first section in the last third of the book which comprises remarks on the foundations of mathematics. But here, to be going on with, are my reconstructive efforts organizing and padding out the remarks of Sec. 108 into more continuous prose: commentary to follow. [For an updated link for the version with commentary, see posting for 1st Oct.]

Quine’s Mathematical Logic revisited

Wednesday, September 3rd, 2008

I recently unpacked a box of old books that I’d stored away in the garage, which included my missing copy of Quine’s Mathematical Logic. I’ve just found myself (re)reading the first part — that’s the initial hundred pages on propositional and quantificational logic. And it’s mostly still a great read — though I do wonder how on earth anyone got to think that Principia style dots were a great idea for bracketing?! The brief end-of-section historical notes are sometimes particularly interesting. So actually, I’d recommend any beginning graduate student brought up on natural deduction and/or trees to spend a morning zipping through these chapters, both for the historical perspective they bring, and also to prompt some thoughts about what’s gained and what’s lost by doing things the modern ways.

I rather wish I’d found my copy before I sent off the revised version of IFL to the press. I might well have stolen a sentence here and an example there! Oh well, next time …

Naturalism in the Philosophy of Mathematics

Saturday, August 30th, 2008

Alex Paseau has a new entry in the Stanford Encyclopedia on ‘Naturalism in the Philosophy of Mathematics‘. If I was being picky, I’d perhaps say that student readers will find that it dives in the deep end a bit quickly. But I found Alex’s useful distinction-making and rather sceptical reflections very helpful.

Smorynski on Hilbert’s Programme

Wednesday, July 23rd, 2008

As I mentioned before, Menzler-Trott’s biography of Gentzen has a number of appendices, including a fifty page essay “Hilbert’s Programme” by Craig Smorynski. (A better title might have been “The slow emergence of Hilbert’s Programme from Hilbert’s intermittent work on foundational questions up to 1930/31, and in particular from his disputes with Brouwer and Weyl.” But I can see why Smorynski stuck to his snappy title!)

I found this essay a terrific read, very helpful and illuminating, at least for someone who makes no pretence of knowing much about the history here. This should now go on any reading list for philosophy of maths students touching on Hilbert’s Programme. And so spread the word: it would be a great pity if Smorynski’s efforts went largely unread because buried at the back of a rather oddly written biography. (The rationale for having this piece appended to the biography is that it sets the scene for Gentzen’s work — but actually, as I noted, Menzler-Trott doesn’t engage very closely with that work, so he doesn’t really join up the dots. An opportunity missed.)

Parsons’s Mathematical Thought: Sec 13, Nominalism and second-order logic

Monday, July 21st, 2008

A general comment before proceeding. Parsons himself says that this book has been a very long time in the writing. And I suspect that what we are reading is in fact a multi-layered text with different passages added at different times, without the whole being finally reorganized and rewritten from beginning to end. This does make for a bumpy read, with the to-and-fro of argument not always ideally well signalled.

Anyway, Sec. 13 falls into two parts, both related to nominalist takes on second-order logic. First, Parsons offers some remarks on the Fieldian project of using mereology to do the work of second-order logic. The key thought is this. For mereology to do all the work Field wants, it needs an (impredicative) comprehension principle: “Given a predicate of individuals that is true of at least one individual, there is a sum of just the individuals of which the predicate is true, and moreover, the admissible predicates will be closed under quantification over all individuals, including those very sums.” (Cf. the principle “Cs” in Field’s “On Conservativeness and Incompleteness”.) But what entitles Field to such a strong comprehension principle? Well, Parsons notes that it’s not clear that Field can offer any direct a priori argument (but then, I wonder, would he want to?). The justification will be that “the comprehension principle is a hypothesis justified by its consequences in systematizing the geometrical basis of physics”. But then “Field’s view, on this reading, puts him in a position in which we have found other formulations of nominalism: making the justification of mathematics turn on some hypothesis about the physical world, which is more vulnerable to refutation than the mathematics.”

But how troubled will a Fieldian be by that complaint? Suppose we decide that our physical theory of the world doesn’t require such a strong comprehension principle (we can get away with recognizing a less wide-ranging plurality of regions). That’s not at all implausible, actually, given that (nearly) all the mathematics required for physics can be reconstructed in a weak second-order arithmetic like ACA_0 with only predicative comprehension. Then the Fieldian response will (surely?) be just to demote the full mathematical apparatus of the classical reals from its status in Science without Numbers as a supposedly justified tool for getting more nominalistically acceptable consequences out of our best physics. It is no longer so justified. In that sense, for the Fieldian, the “justification” of a bit of mathematics is wrapped up with our hypotheses about the physical world, and Parsons’s complaint will seem question-begging. [Or am I missing something here?]

The second part of Sec. 13 considers Boolos’s attempt to make second-order logic ontologically tame by giving a plural reading to the second-order quantifiers. The thought under scrutiny is that plural quantification is ontologically innocent because, in plurally quantifying over Fs, we are just committing ourselves to Fs (not to sets or to Fregean concepts). Parsons’s discussion [or again, am I missing something here?] initially advances familiar sorts of worries about this claim of innocence. But Parsons does make one point towards the end of the section that I find very congenial (i.e. I’ve argued similarly myself!).

Consider (say) the range of second-order arithmetics that Simpson discusses in SOSOA. As we advance through theories with stronger and stronger comprehension principles, then — on a standard platonist construal — we are countenancing more and more sets of numbers. If we reconstrue the second-order quantifiers plural-wise, then, as we go from theory to theory, we are countenancing more and more …. well, more what? It is tempting to say “pluralities”. And indeed it is convenient to give an informal gloss of the plural reading using talk of pluralities. But — if this isn’t to smuggle back reference to pluralities-as-single-entities, i.e. sets — this convenient way of talking needs to be eliminable (cf. Linnebo’s nice article on plural logic). So how do we eliminate it here? We might, I suppose, trade in talk of countenancing more and more pluralities for talk of allowing more and more different ways we can take numbers together: but this seems tantamount to re-instating Fregean concepts as the values of the second-order variables — which is fine by me, but then the supposed ontological gain of interpreting the second-order quantifiers via plurals is lost.

The question then is this: if we accept the pluralist’s contention that we can treat second-order numerical quantifiers as ontologically committing just us to numbers, period, then how are we to think of the surely varying commitments we take on with varying strengths of comprehension principle. As Parsons puts it, “If there is no enlargement of ontological commitment [my emphasis] as one passes to less restricted versions of the comprehension schema, then perhaps that speaks against the importance of the notion.”

Logic’s Lost Genius

Friday, July 18th, 2008

It has to be said that Eckart Menzler-Trott’s Logic’s Lost Genius: The Life of Gerhard Gentzen is a strange work.

For those who haven’t seen it, a word about the structure. The main part (pp. 1-283) of this large-format, small-print, book is notionally a biography of Gentzen, but as I’ll note in a moment there are very long digressions. Then there are four appendices. The first (pp. 285-292) is a note by Craig Smorynski (who is also the main translator from the original German version of the book) on an elementary but neat proof in geometry re-discovered by the school-boy Gentzen. Next (pp. 293-343) there is a long essay by Smorynski on Hilbert’s Programme. The final appendix (pp. 369-405) is another essay, almost as long, by Jan von Plato, called “From Hilbert’s Programme to Gentzen’s Programme”. Lastly, rather oddly sandwiched in between those last two essays, Menzler-Trott includes three lectures by Gentzen himself. These are

  1. The Concept of Infinity in Mathematics (item #6 in Szabo’s Collected Papers),
  2. The Concept of Infinity and the Consistency of Mathematics,
  3. The Current Situation in Research in the Foundations of Mathematics (item #7 in Szabo).

1 and 3 are newly retranslated. 2 is just over two sides long (and is little more than a summary of 1).

I’ll comment in later posts on the essays by Smorynski and von Plato. But what about the main biography?

Well, as I said, this really is rather strange. For a start, one very long chapter (pp. 141-232, ‘The Fight over “German Logic” from 1940 to 1945: A Battle between Amateurs’) concerns Nazi attitudes about the “decadence” of mathematics supposedly due to Hilbert. This tells us just a bit about how Gentzen’s work was viewed in some quarters. But most of the discussion is only distantly relevant (pages and pages go by without Gentzen being even mentioned). In fact, however interesting this all will be for those researching on the politicization of academic life under the Nazi regime, it tells us almost nothing about Gentzen’s intellectual development.

And the other chapters, which really are on Gentzen, are oddly written (and I’m not talking about the translation into an English replete with far too many sentences no native speaker would use). Rather the text too often reads like unprocessed working notes, stringing together remarks on intellectual events, or on unrelated family affairs, with excerpts from Gentzen’s letter and reviews. For a particularly staccato example, on p. 94 we read [and yes, these are consecutive mini-paragraphs]:

In December 1937 Gentzen informed at least Paul Bernays that he had carried out his consistency proof in a simpler and more thorough form.

Since December 1937, Gentzen’s sister, Waltraut, and her husband lived in Liegnitz/Niederschlesien (today: Lignice, Poland).

On 3 January 1938 Bernays wrote from Besenrain Str. 30 in Zürich that he had finished §11 of the foundations book for two weeks, but it was not yet typeset: “As soon as the copy is made, I will send it to you.”

In Zentralblatt für Mathematik 17 (1938), p. 242, there appeared: [and Menzler-Trott then reproduces Gentzen's review of Barkley Rosser's 1937 JSL paper 'Gödel theorems for non-constructive logics'.]

So no one can call this a gripping, well-structured, story!

But stylistic complaints (and the very long aside on Nazi attitudes) apart, is the biography at least illuminating? The answer, I’m afraid, is “not very”, at least not if you are looking for an account of Gentzen’s intellectual trajectory. And this is because — unlike Dawson on Gödel or the Fefermans on Tarski — Menzler-Trott doesn’t just engage enough with Gentzen’s logic. For example, if you don’t already know about his work on natural deduction and sequent calculi, you’ll hardly get any sense of what Gentzen was up to here and why it matters. (Ok, Gentzen’s work is going to be addressed more directly in the two long appendices by Smorinski and von Plato: but it does feel as if Menzler-Trott narrative has a large hole at the centre.)

Still, there is a lot of detail about Gentzen’s milieu, about whom he met when, about who influenced him, and whom he was corresponding with. And this scene-setting is interesting enough. Moreover, quite a few letters are quoted, which have some interest — though note that there is little by way of e.g. novel informal exposition here. Hence you won’t get a new understanding of Gentzen’s results from them. But you’ll at least come away with a better sense of the external shape of the context in which his papers were written. You’ll have to wait until the appendices, however, to learn more about the internal dynamic of the ideas there.

I should add, though, that the last main chapter, on Gentzen’s death in prison, contains moving accounts from fellow prisoners: do read this chapter even if you don’t read the rest of the book.

Parsons’s Mathematical Thought: Sec. 12, Nominalism

Wednesday, July 16th, 2008

This is a short and rather insubstantial section, which I’m just taking separately to get out of the way, because the next section is weighty (and one of the longest in the book).

Parsons understands ‘nominalism’ Harvard-style — no surprise there, then! — to mean the rejection of abstract entities and the eschewing of (ineliminable) modality. What hope, then, for giving a response to the potential-vacuity problem for eliminative structuralism about arithmetic (say) which meets nominalist constraints? We can’t, by hypothesis, go modal: so what to do?

Well, as the physical world actually is (or so we might well now believe), there are in fact enough physical things — e.g. space time points — and suitable physical orderings on them to give us physically realized ’simply infinite’ structures. But Parsons is unhappy with this way of meeting the vacuity worry, and for familiar reasons: “[S]hould it be taken as a presupposition of elementary mathematics that the real world instantiates a mathematical conception of the infinite? This would have the consequence that mathematics is hostage to the future possible development of physics.”

But (although I have no particular nominalist sympathies myself), I’m not sure how worried the nominalist eliminative structuralist should be about giving such hostages to fortune. As things are, given how we believe the world actually to be, he can reasonably continue to speak with the vulgar and treat arithmetical claims as true or false. Even if the worst happens, so we come to believe the world is ultimately grainy and finite in all respects, it’s not that ’school-room’ arithmetic is going to get undermined. At most, it is the idealizing rounding out of school-room arithmetic which insists on an infinitude of numbers. And if it should emerge that the rounding out, construed the eliminative-structuralist way, collapses in vacuity — well, formal arithmetic can still be played as an intriguingly entertaining game. It’s just that then, after all, the nominalist eliminative structuralist who is relying on physical realizations for structures can no longer readily construe idealized arithmetic’s claims as true or false, and so the nominalist has to sound a bit more revisionary. But, he’ll say, so what? (Parsons says “a great deal of the historically given mathematics would have to be jettisoned in this case” — but that’s too quick. Talk of ‘jettisoning’ covers over a slide. For no longer thinking of arithmetic as construable as literally true by the eliminative structuralist manoeuvre is not the same as throwing arithmetic into the trash-can, as any fictionalist will insist.)

What about the other line that offered to the nominalist at the end of Sec. 11? — i.e. sidestep the vacuity problem by going modal in an anodyne way (“interpret the theories in an if-thenist way, but deal with the problem of possibility by appealing to consistency, nominalistically interpreted”). Well, again Parsons sees trouble, this time arising from the fact that there might be physical limitations in how big a proof-token could be, and so a theory could count as (nominalistically) consistent — because no proof of an inconsistency could be tokened — even if we can show that there is a process which, given world enough and time, would produce an inconsistency. But again, I’m not sure that the obstreperous nominalist couldn’t swallow that too.

At the end of this section, Parsons revisits the question of how to frame an eliminative structuralism for arithmetic. He looked at a move from a set-theoretic formulation to a more ‘logical’, second-order formulation. But could we go first-order, in a way more congenial no doubt to those of nominalist inclinations? The trouble is, of course, that we won’t get categoricity (whatever we build into the axioms), so the eliminative structuralist who goes first-order runs up against the intuition that the natural numbers have a unique structure. But how secure, in fact, is that intuition? Parsons raises that excellent question (too often passed over in silence), but only to shelve it until Ch. 8. So we’ll have to return to that later.

Telling your epis from your monos.

Monday, July 14th, 2008

Ok, so how do you remember which are the epimorphisms, which are the monomorphisms, and which way around the funny arrows get used?

Since the textbooks don’t seem eager to offer helpful mnemonics, I offer a forgetful world the following.

It’s the LM/PR rule. L-for-left goes with M-for-mono, and P-almost-for-epi goes almost next to R-for-right. OK?

But what does that mean? Simple. A mono is of course a left-cancellable morphism, and you signal one using an arrow with an extra decoration (a tail) on the left. Dually, an epi is a right-cancellable morphism, and you signal one of those using an arrow with an extra decoration (another head) on the right.

Easy, huh? Well, it works for me — and these days, I’m grateful for all the props I can get … [As always, click on the image to get a full sized version.]