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.