Thesis Topics
Most of these subjects arise from my interest in NF but are not
neccessarily inextricably entwined with it.
Someone ought to write a thesis analysing potential infinities in
terms of lazy evaluation. That is how finite beings can come to dream infinite thoughts. I would love to supervise it.
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. 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? Does that
topology interact in any useful way with the usual (Stone) topology
on the space of permutation models? 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
proof-theoretic nightmare. If we drop it 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.
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, or (ii) it remains a
set, but one can't manipulate it as freely as one would wish. 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 decision about
the others. If the collection of all ordinals is a set 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?
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 we have just started a wiki to record our
progress. (Outsiders can read it but not write to it.) 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.
Very striking that: (i) NF refutes AC,
(ii) No ω-model of
TNT satisfes AC, and
(iii) No model of TNT 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 TNT. (TNT is the theory of simple types with
types indexed by Z not by the naturals). Nor has anyone ever found a
model of TNT which is symmetric. We know TNT 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. Astonishingly this turns out to give NF. This needs investigating.
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.