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