Year: 2012

I was particularly looking forward to two of the talks scheduled for the last day of the Foundations conference, those by Steven Methven and Dan Isaacson. Sadly, for different reasons, neither happened. That left just three talks. Sam Sanders spoke about his research on the reverse mathematics for a certain system of non-standard analysis. You could get a few glimmers of what might be interesting in this area from his talk, but it was hopelessly ill-judged for the occasion: but visit Sam’s web-pages if you want to know more.

Alan Weir also gave far-too-rushed a tour, this time through some of the themes of his book Truth Through Proof which I’ve blogged about at length: I think it is fair to say there was nothing new here.

The remaining session, though, was a very nice review by Mary Leng of some points of difference between the sort of fictionalism that she favours and the kind of formalism that Alan defends. On the principle ‘the enemy of my Platonist enemy is my friend’, Mary found herself wanting to minimize some apparent big divergences between their positions. But the crunch disagreement, for her, comes over their respective views about logical consequence. The fictionalist talks of inferences within the fiction, the formalist of inferences within the formal game (putting it roughly). But what makes for ‘good’ patterns of inference in either case? Mary thinks she has to appeal to a primitive logical modality here. Alan eschews such modalities, but then — Mary argued — has nothing helpful to say about logical consequence (unless he smuggles a modality in the back door). Alan of course thinks otherwise. Like a Catholic bemused by warring factions of Protestants, I’ll leave them to battle that one out …. But I think Mary probably does jab her finger on a sore spot for the formalist.

I missed Mic Detlefsen’s talk, and arrived half-way through Steve Awodey’s “Homotopy type theory and univalent foundations”, which was a beautifully presented advertising pitch for the project you can read a lot more about here.

James Studd (a graduate student in Oxford) then gave a paper on a bi-modal axiomatization of the iterative conception of set. Why bimodal? Start with the familiar informal tensed chat where we talk of forming levels of the hierarchy successively. We want to say things like: the new sets formed at a level must have members already formed at past levels, and once formed must persist at future levels. So it is pretty natural to try regimenting such past-looking and future-looking talk with a pair of tense-like modalities. Except, as Studd himself emphasised, they aren’t really temporal modalities. But then, of course, the problem is to make non-metaphorical sense of them. And (as Robert Black pointed out in discussion) the trouble is that the natural ways of doing this presuppose an understanding of talk of levels in the iterative hierarchy, so the modalities thus explained can’t really serve as giving an independent handle on how to understand the iterative conception. If instead, as I think Studd wants, we ultimately take the modalities as new primitives, then it is pretty unclear whether anything has been gained at all over e.g. the Boolos axiomatization of stage theory.

Next up, Michael Potter talked about whether Replacement can be justified, developing worries already expressed in his Set Theory and its Philosophy. Replacement amounts to two claims: roughly, (a) every set is a subset of a level, and (b) there is a level for every set size. In a Scott-style axiomatization, (a) is built in. But what would justify adding (b), which is equivalent to a reflection principle?

‘External’, regressive, arguments — from the supposed need to assume (b) if we are to prove some desired mathematical results outside set theory — don’t work: full Replacement isn’t needed for (enough) “ordinary” mathematics. So we need to appeal to ‘internal’ considerations, flowing from our conception of the set universe. A limitation of size principle might support Replacement, but is itself difficult to motivate. Meanwhile — and this is the key point Michael wants to press — the iterative conception doesn’t deliver the goods.

This particularly nice talk was followed by Hannes Leitgeb on ‘A theory of propositions and truth’. The idea is to model a theory of propositional functions and ‘aboutness’ on a theory of sets and membership: so the aim is an untyped but paradox-free theory, on which is grafted an untyped theory of truth-for-propositions, and then a theory of syntax and a derived theory of truth-for-sentences. Hannes ends up in the Tractarian position of having to say that the axioms of his theory don’t express propositions, a conclusion he cheerfully embraced. But I, for one, am quite unclear what are the rules of the game for this kind of constructional exercise in defining formal gadgets, and hence quite unclear whether such insouciance is justifiable.

In the final talk of the day, Alex Paseau talked interestingly about the possibility and scope of non-deductive knowledge of mathematical propositions. He had two different sorts of cases. First, there’s what we might call ‘experimental’ evidence — as when we draw enough diagrams to convince ourselves that the perpendicular bisectors of a triangle intersect at a point. And then there is mathematical evidence such as probabilistic considerations, neighbouring theorems, etc. — as in our evidence for Goldbach’s Conjecture or the Riemann Hypothesis. These cases do seem very different to me, however, and I am rather inclined (without much by way of argument) to return a split verdict. That is to say, I find it happier to say I can get to know some propositions of Euclidean geometry by the experimental method than I am to say I could get to know Goldbach’s conjecture by totting up more evidence short of a proof. Perhaps that’s because of the nagging doubts engendered by the dim recollection that there are other number theoretic conjectures which have only immense, and immensely sparse, counter-examples: so, the thought remains that for all we currently know — even augmented with more of the same — we could still be in for a nasty surprise.

I am taking some time off from revising the Gödel book, going to (most of) a local conference, Foundations of Mathematics: What are they and what are they for? Yes, it really is all fun, fun, fun at Logic Matters.

The conference kicked off with Tim Gowers (that’s Sir Tim to you) talking about discovering proofs by breaking down proof-tasks into simpler and simpler ones. He talked through a couple of cases: for example, how would you tackle the question “Find the 2012th digit after the decimal point in the expansion of $latex (\sqrt 2 + \sqrt 3)^{4024}$”? As an exercise by a wonderful teacher leading an audience to see that there is a “natural” way of getting to an answer, just brilliant. As (part of) a gesture towards evidence for a general thesis Gowers likes, namely that the role of “flashes of intuition” in mathematical discovery is much exaggerated, interesting and suggestive. As a hopeful illustration of the kind of heuristics we could give a computer to discover the proof, not so convincing. And as far as the official theme of the conference goes, I suppose somewhat off-topic.

Brendan Larvor’s talk was about the so-called “Philosophy of Mathematical Practice” and the supposed rise and fall of a certain conception of the architectural organisation of mathematics as having/needing “foundations”. But this was at a level of arm-waving generality that I find entirely uncongenial.

Philip Welch talked about a General Reflection Principle in set theory — fine, as you would expect, on the technicalities, but this got bound up with some entirely unclear remarks about why it might help to move from talking about sets qua objects to talking about the concept of sets (which turned out to be talking about a structure). I was also unclear why he thought that talk about “parts” of the set-theoretic universe rather than of sub-classes of the universe was a gain.

The best talk of the day was by Patricia Blanchette, essentially on the Frege-Hilbert dispute about theories, independence proofs, etc. This was extremely clear and convincing, but she has written more than once before about this (see her terrific entry in the Stanford Encyclopedia), and I’m not really sure what was new.