Thesis Topics

This document is going to undergo some radical revision in the coming months. The chief reason for this is the alleged consistency proof for NF. Do I believe the allegations? I don't disbelieve them. Like Galileo, I have been shown the instruments. This much I will say: even if the proof doesn't work in its current state, a new seam has been opened up, and either way there is plenty of work for a Ph.D. student to do.

Most of these subjects arise from my interest in NF but are not neccessarily inextricably entwined with it.

One of my current preoccupations is the question of synonymy between weak systems of set theory with a universal set and weak systems of arithmetic. We know quite a bit about synonymy between weak arithmetics and weak set theories with foundation, and set theories with a universal set are a natural extension.
I have recently been moved to look again at Sharvy's Lucy and Benjamin puzzle. I am increasingly thinking that this is a problem worthy of a Ph.D. It raises both epistemic and logical issues. The link is to my Studia Logica article rather than the original article...but there is remarkably little literature on this topic and the link is as good a place to start as any.
What happens to the entities postulated by obsolete scientific theories? There is an extensive literature on this question in the philosophy of science community. Curiously, people who interest themselves in philosophy of mathematics take very little interest in the status of the entities postulated by dysfunctional or obsolete mathematics. It may be that they have too much respect for mathematics to wish to say anything that even sounds like a suggestion that there might be such a thing as obsolete or dysfunctional mathematics. Nevertheless, mathematics is a branch of the sciences, and, like other sciences, has its false starts---its phlogiston theories---too.
Much of mathematics (like much of science in general, for that matter) arises from projects to find the correct way to think of a particular phenomenon. Or, sometimes, the right way to apply a particular insight or technique. Boolean algebra is the way to think of (classical) propositional logic algebraically. Tarski, reflecting on this, felt that there should be an algebraic way of thinking of first-order logic (predicate calculus, whatever you want to call it). His response was to develop what he called cylindric algebras. Various people (one thinks of Donald Monk) did good work on these things, but in the second half of the twentienth century they fell out of favour, and the historical record makes it clear why. New approaches became available with the spread of category theory, and almost anyone who is both (i) interested in the question and (ii) familiar with category theory will say that the correct way to algebrize first-order logic is by means of the device of classifying topoi.
So what is the status of cylindric algebras? The same as phlogiston? Or are they perfectly kosher objects?
There is a nice theorem about Rieger-Bernays permutation models, which I made a small contribution to proving: a formula is equivalent to a stratified formula iff the class of its models is closed under the Rieger-Bernays construction. [The Rieger-Bernays construction you will have seen in rudimentary form in the standard proof of independence of the axiom of foundation from the other axioms of ZFC.] That's a nice fact. A slightly less striking fact is that in theories where one can quantify over the permutations that give rise to the models one has a natural interpretation of modal syntax: □p will mean that p holds in all permutation models. In NF this gives rise to a particularly degenerate modal logic: S5 + Barcan + converse Barcan + Fine's principle H. Not very interesting. It may be that by restricting the permutations one considers one gets more interesting modal logics.

Another thing that needs to be looked at is whether the topologies on the symmetric group on the carrier set have anything to tell us about the family of permutation models. Is the set of models containing Quine atoms dense, for example? The collection of permutation models admits a Stone topology beco's it's a collection of first-order structures. Do these two topologies interact with each other at all? As far as i know this has never been investigated: incredible tho' it may seem, it may be that the sum total of knowledge on this subject is in my Oxford Logic Guides book. One circumstance that I am sure is significant but whose significance is obscure to me is the fact that although composition of permutations has some meaning in terms of the model theory and modal logic, inversion seems to have no meaning at all: the fact that the family of permutations is a group seems to do nothing over and above it being a semigroup. Is this anything to do with the fact that we should really be dealing with setlike permutations rather than permutations that are sets, and the inverse of a setlike permutation might not be a set? The matter cries out for investigation. Seeking Structure for the Collection of Rieger-Bernays Permutation models is the current draught of a paper I started writing with Olivier Esser (it has to be admitted that this project is stalled at the moment: it really needs a Ph.D. student!).

There is a deep connection between permutation models and unstratified assertions about virtual entities (such as cardinals) which arise from congruence relations on sets. Cardinal arithmetic is that part of set theory for which equipollence is a congruence relation. All assertions---even unstratified assertions---of cardinal arithmetic are invariant. There seems to be a tendency for the unstratified assertions to be equivalent to assertions of the form □ or ◇ prefixed to a purely combinatorial assertion about sets. (□ and ◇ are as in the modal logic of Rieger-Bernays permutation models, as above.) For example the axiom of counting is equivalent to the assertion ``◇(the von Neumann ω is a set)''. It would be nice to know whether this happens generally and if so why. Holmes and I are working on a paper on this topic, but there is plenty of work still to be done.
NF and proof theory. We all know that we haven't really got the right concept of proof-as-mathematical-object---yet! Theoretical computer scientists are at work on it even as I write. Proof theory of set theory is a problem because the axiom of extensionality is a wel-known proof-theoretic nightmare. [Think about extensionality in lambda-calculus: reflect on Rice's theorem...] If we drop extensionality from NF the resulting theory has a sequent presentation for which one can prove cut-elimination. This important result is due to Crabbé. Anyway, it would be good if some member of the tribe of theoretical computer scientists who work on proof theory were to have a look at the possible ramifications of their work for NF studies. Constructive theories generally have nicer proof theory than their classical counterparts, and in the particular case of NF there are extra reasons (namely the breakdown of the double-negation interpretation) to support my long-standing conjecture that the obvious constructive version of NF (weaken the logic but keep the same axioms) is consistent and weak. There are good reasons to expect this, and I suspect the proof will be quite easy. It has been very elusive so far. It is only fair to say that Holmes doesn't believe that constructive NF (INF to its friends) is any weaker than NF. Might there be a clever way of coding constructive NF inside the theory of recursive functions.....? At all events, I am going to keep publicly available my notes on constructive NF
Students of NF will know the T function, that takes the cardinal of a set x and returns the cardinal of the set of singletons of members of x. The assertion that T is the identity on the natural numbers (aka The axiom of counting) is known to be strong: it proves Con(NF). What about the assertion that T is merely nondecreasing on the naturals? Does that prove Con(NF)? Does this assertion also imply that T is nondecreasing on the countable ordinals?
This probably sounds like a fiddly NF question but it's actually a fairly mainstream question about nonstandard models of arithmetic and of the theory of countable ordinals.
That said, my student Zachiri seems to have made some progress in driving a wedge between these two assertions.
The theory KF of my joint paper with Richard Kaye in the JSL 1990 is quite interesting. (End-extensions preserving power set. Journal of Symbolic Logic 56 pp 323-328). There is a vast sequel to that paper which has never been turned into anything publishable. Some of the material is alluded to and explained in Mathias' magisterial recent survey article on Weak Set theories: Notes on MacLane Set Theory, Annals of Pure and Applied Logic, 110 (2001) 107--234. One very interesting question about KF is whether or not it is consistent with the assertion that there is a set that contains wellorderings of all lengths. This question is interesting because it is related to the question of how far it is possible to separate the paradoxes. The paradoxes can all be seen off in one of two ways: either (i) the problematic collection turns out not to be a a set (which of course is the ZF response) or (ii) it remains a set, but one can't manipulate it as freely as one would wish. With some paradoxes one has no choice: for example the nonexistence of the Russell class is a theorem of first-order logic, so there is no live option (even for NF-like theories) to make it a set. However, the nonexistence of the set of all ordinals, or of all cardinals, and many others, rely on set-theoretic axioms and we have some freedom of manoeuvre.

It is natural to wonder to what extent decisions one takes about how to knock one of the paradoxes on the head affects one's decisions about the others.

So, for each paradoxical object not aleady ruled out by first-order logic, we have to choose between (i) and (ii).

Q: How free are we to make these choices independently?

Possibly freer than many people think. It is a little-known fact that it is consistent with Zermelo set theory that one can implement cardinality in such a way that the collection of all cardinals is a set! And it's a well-established fact that the universe can be a set. If the collection of all ordinals is a set (and we know it can be) must the universe be a set too? Or at least, does the sethood of the collection of all ordinals smoothly give rise to a model of a set theory with a universal set? The boldface question above seems a natural and fundamental question to ask, but it doesn't seem to have attracted much attention.

It is a curious fact that if --- in the usual axiomatisation of NF --- one replaces `∈' by `∉' throughout one obtains another axiomatisation of NF. Let φ* be the result of doing this replacement to a set theoretic formula φ. Obviously φ* is a theorem of NF iff φ is. What about sentences of the form: φ ↔ φ*? One does not expect these formulae to be theorems of NF; the situation is very like the original typical ambiguity setting (except that there the * operation is not an involution). I have been able to show that not all of these formulae are theorems of NF, but are they all individually consistent? And can they all be consistently added simultaneously? There is no obvious reason why not. It follows from work of Specker that any finite conjunction of expressions of this form is equivalent to another expression of this form, so it will be enough just to show that each biconditional is individually consistent relative to NF. The obvious weapon to use is Ehrenfeucht games, but I have not been able to make any significant progress using them.
NF0 is NF with quantifier-free comprehension only. There are the following conjectures:

Every ∀*∃* sentence refutable in NF is refutable already in NF0;
NF0 decides all stratified ∀*∃* sentences;
Any term model for NF and any model for NF in which all sets are symmetric satisfies every ∀*∃* sentence consistent with NF0;
All unstratified ∀*∃* sentences are either decided by NF or can be proved consistent by permutations.

What does NF prove about wellfounded sets? (The point is not made often enough that as far as we know NF proves no theorems about wellfounded sets that contradict any deeply-and-sincerely-held beliefs of the ZF-istes). Is the theory of wellfounded sets of NF invariant under Rieger-Bernays permutations? Probably not. Is the stratified part of it invariant? Perhaps more natural questions concern the content of that theory rather than the metatheorems once can prove about it. All we know at present is that it contains the theory KF alluded to above. (Not obvious that it satisfies either infinity or transitive containment, for example). If that is the best one can do, then every wellfounded model of KF is the wellfounded part of a model of NF. There are probably quite a number of theorems like that that one can prove, and a fairly straightforward example (every wellfounded model of ZF is the wellfounded part of a model of NFO) is one that can be found in my Church festschrift paper. It would be nice to have converses: ``The theory of wellfounded sets in NF is precisely KF'' would be nice. Of course one can't prove that without proving con(NF) but no-one has even proved the conditional ``Con(NF) → KF is the theory of wellfounded sets in NF''. My guess is that every wellfounded model of KF is the wellfounded part of a model of NF. To prove this outright one would of course have to show Con(NF), but in principle one might be able to show that if NF has any models at all then every wellfounded model of KF is the wellfounded part of a model of NF. I suspect it's true (and probably quite easy to prove) that every model of KF has an end-extension that is a model of NFU.
In the ZF world there is a family of inner models of Hereditarily symmetric sets. They are genuine inner models: they are transitive and extensional and wellfounded and you can take them anywhere. But unstratified separation fails in them and they violate AC. They are now under investigation by my group at Cambridge, and both Zachiri McKenzie and Vu Dang have worked on them. and Vu's Ph.D.thesis has a chapter on them.
We are also investigating a version of Gödel's L constructed by stratified rudimentary functions in which AC fails. (This, too, was first revealed to the world in the symmetric sets paper above). One thing that we would like to get from this project is a model of KF where Hartogs' theorem fails, so that there is a set containing wellorderings of all lengths. That would be a first step to a consistency proof for NF.
Weak choice principles in NF.
It is true that choice can be refuted in NF, but some quite strong and natural versions of choice are still running around free for the moment. There are global choice principles still unrefuted - the prime ideal theorem for example. As I keep saying, there is no reason to suppose that the wellfounded sets cannot form a model of ZFC. In this connection we note that Holmes has shown that if DC and the axiom of counting hold, then there is a forcing model in which the continuum can be wellordered.
(TZT is simply type set theory with types indexed by Z not by the naturals).
Very striking that:

(i) NF refutes AC,
(ii) No ω-model of TZT satisfes AC, and
(iii) No model of TZT in which all sets are symmetric can satisfy AC

---and these three proofs are completely different!
To this day no-one has ever found an ω-model of TZT. Nor has anyone ever found a model of TZT which is symmetric. We know TZT is consistent because of a compactness argument, and the only models we have are models that arise from that insight.

This last topic is a favourite of André Pétry's---or was. Develop model theory for Stratified formulae. I alluded above to a completeness theorem for stratified formulae that he and I put the finishing touches to: a formula is equivalent to a stratified formula iff the class of its models is closed under the Rieger-Bernays permutation construction. Theorems about cut-elimination and stratification have been proved by Marcel Crabbé. It does seem that it should be easier to prove cut-elimination for stratified formulae but the situation is clearly complex: every provable stratified formula has a cut-free proof, and will also have a stratified proof---but there is no guarantee of a proof that is both. The issue is subtle. The assertion

(∀x ∈ y)¬(∀z)(z ∈ x)  →  ¬ (∀w)(w ∈ y)

has both a stratified proof and a cut-free proof. However, if you eliminate the cuts from the stratified proof the result is not stratified. It seems that it has no proof that is both stratified and cut-free. (Notice that we are seeing all this subtlety just in first-order logic simpliciter: we need no rules for ∈ to do this.) The proposition comes in distinct classical and constructive versions. (The version displayed above is the one with a constructive proof). The existence of this proof means that if we have a principle of stratified parameter-free ∈-induction (that is to say, ∈-induction for stratified formulae without parameters) we can deduce the non-existence of a universal set. For the life of me I have not been able to deduce anything else from this induction principle. Can we perhaps show that stratified parameter-free ∈-induction follows from the nonexistence of a universal set? Can anyone find a model of KF exhibiting a failure of stratified parameter-free ∈-induction...?
The situation cries out for the attentions of a Ph.D. student!

Recently Randall Holmes has been in correspondence with a man who thought thhat the key to understanding in set theory was not stratification but the parallel notion of the variables forming an acyclic graph. Put an edge between two variables iff there is an atomic subformula containing occurences of them. On the face of it this is a restriction much more severe than stratification but, astonishingly, this turns out to give NF. This warrants investigation.
I don't promote questions about NFU here: if you want to study NFU you should go to Boise and work under Randall Holmes. (In fact if you come to work on NF with me you will be sent off to Boise to study with Holmes at some point or other). I do have one question about NFU tho': can there be a model of NFU in which the set of atoms forms a set of indiscernibles? Holmes thought for a long time that they are always indiscernible, but recently has shown that in the usual ZFJ models the atoms are all discernible. I think that the existence of a model of NFU in which the atoms are indiscernible is a strong assumption possibly equivalent to the consistency of NF. That would be worth proving.

Now here are some topics of a less hard-core set-theoretic nature.

There is a Ph.D. thesis to be written on the nature of the unconscious strong typing of mathematics, and how it developed in theoretical computer science and how it still fertilises mathematics. It's incompatible with foundationalism, which makes it a contrarian topic, albeit a very interesting one. It's also one i am trying to write a book on, but something tells me i'll never get it done.

The first-order logic with the quantifiers ``for all but finitely many x'' and its dual ``there are infinitely many x such that..'' is an interesting byway. There are some surprisingly elementary questions about it that remain open. Is it decidable, for example?

The differences between evaluation strategies (lazy vs strict, and versions in between) matter enormously to people in λ-calculus but elsewhere in Logic have not attracted the attention their potential expanatory power merits. I am sure an analysis in terms of lazy evaluation will have lot to say about the rôle of actually infinite mathematical objects in human thought...about how it is possible for finite beings to dream infinite thoughts. I would love to supervise a thesis on this subject