nf.html

<TITLE> New Foundations Home Page </TITLE>

<H1> New Foundations home page </H1>

<strong>Note, added March 30, 2005</strong> After systematic neglect
for some years, I'm about to overhaul the page and update the
bibliography (again in 2020).  Any comments from NFistes would be useful at this
point...</strong><p>
  
  <strong>Note, added June 8, 2020</strong>:  After a further fifteen years of neglect, a great deal of dusting and rearranging needs
  to be done in this space before it is usable!  <strong>June 10</strong>:  I am done with preliminary administrative repair (links to resources and persons are as accurate as I can make them)
but there remains the more delicate task of reporting on changes in our view of the mathematical content.<p>

For new information about the mailing list, look in <A HREF = "#Links">the Mailing List
and Links to NF Fans section.</A><P>

<A NAME = "Contents"><H2> Contents </H2></A>
<UL>
<LI><A HREF = "#Introduction">Introduction</A>
<LI><A HREF = "#Links">Mailing List and Links to NF Fans</A>
<LI><A HREF = "#Definition">Definition</A>
<LI><A HREF = "#Paradoxes">The Paradoxes</A>
<LI><A HREF = "#Problem">The Big Problem</A>
<LI><A HREF = "#Consistent">Consistent Subsystems</A>
<LI><A HREF =
"Bibliography/setbiblio.html"> Thomas Forster's Exhaustive Bibliography (new version set up in HTML by Paul West)</A>
</UL>
<A NAME = Introduction><H2>Introduction</H2></A>

This page is (permanently) under construction by <A HREF =
https://Randall-Holmes.github.io> Randall Holmes</A>.  

<P>
The subject of the home page which is developing here is the set
theory "New Foundations", first introduced <A HREF =
"Bibliography/setbiblio.html#Quine">by W. V. O. Quine in 1937</A>.  This is a
refinement of the simple typed theory of sets (which is not really Russell's type theory, though for the rest of this document I will follow
  my own old incorrect usage and call it that) based on the observation that
the types in Russell's theory look the same, as far as one can
apparently prove.

<P>
To see Thomas Forster's master bibliography for the entire subject, as
updated and HTML'ed by Paul West, click <A HREF = "Bibliography/setbiblio.html">
here</A>.  References in this page also refer to the master
bibliography.  We are very grateful to <A HREF =
http://www.dpmms.cam.ac.uk/~tf>Thomas Forster</A>
for allowing us to use his bibliography.  An all purpose reference for
this field (best for NF) is <A HREF = "Bibliography/setbiblio.html#Forster"> Thomas
Forster's "Set theory with a universal set"</A>, second edition,
Oxford logic guides no. 31, 1995.  An old but still good treatment is
found in <A HREF = "Bibliography/setbiblio.html#Rosser"> Rosser's "Logic for
mathematicians"</A> (second edition, Chelsea, 1978); the main text
predates Specker's results about Choice and Infinity.  The entire
development in Rosser, including the treatment of Choice, can readily
be adapted to NFU (by providing a type-level ordered pair as a
primitive).  I have written something which appears to be an elementary
set theory textbook using NFU: for information look <A HREF =
"../nfsummary.html">here</A><p>

  A corrected text for my book Elementary Set Theory with a Universal
Set is now available online <A HREF = "head.pdf">here</A> (this
is a PDF file) by permission of the publisher: a real second
edition will appear online eventually in place of this ad hoc
corrected version.<p>

<P>
There is a theorem prover <A HREF = "Watson//proverpage.html">Watson</A>
whose higher order logic is an untyped lambda-calculus equivalent to
an extension of Jensen's NFU.  This is being developed by <A HREF =
"index.html">Randall Holmes</A>.  Source and documentation can be
downloaded from the link given.  In this connection, one should also
mention the work of Thomas Jech and Warren Wood in which they apply
the prover Otter to investigations of the system of untyped
combinatory logic TRC defined by Holmes (and shown to be equivalent to
NF).

<A HREF = "../Marcel/marcel.html">Here</A> find the page describing a sequent prover using NFU as its logic,
adapted from the sequent calculus for SF in Marcel's cut-elimination
paper.  

  <P>
<A HREF = "#Contents">Back to contents</A>

<A NAME = "Links"><H2> Mailing List and Links to NF fans </H2></A>

<H3> The Mailing List </H3>


There was until fairly recently a New Foundations mailing list, which I shall try to revive in some form 
    (writing in June 2020)<P>

<H3> Links to Fans</H3>

<A HREF = "http://www.wvquine.org">
W. van Orman Quine</A> originated NF.

<P>
<A HREF = "http://www.dpmms.cam.ac.uk/~tf"> Thomas
Forster</A> is the author of the currently definitive tome on the
subject (see above).

<P> 


Marcel Crabb&eacute (who is retired, and whose page now malfunctions) showed that subsystems of NF with predicativity restrictions are consistent and also showed that NFU (with no extensionality at all) enjoys cut-elimination.

<P>
<A HREF="mailto: ddz@skynet.be"> Daniel Dzierzgowski </A>'s 
home page is <A HREF = "http://users.skynet.be/ddz"> here </A>.

<P>
Aldo Antonelli, mentioned here before, has passed on.  May his memory be for a blessing.

<P>
<A HREF = "http://web.mat.bham.ac.uk/R.W.Kaye/"> Richard Kaye </A> has
worked on the theory KF which is a subtheory of both NF and standard
set theory and has worked on fragments of NF in which comprehension is
restricted to quantifier prefix classes.

<P>
<A HREF = "mailto: koerner@math.tu-berlin.de"> Friederike Koerner
</A> is engaged in interesting work on consistency and independence
results using permutation models of NF.  I am not verifying mailing addresses as I
  fix this in 2020:  I do not find a web page for Dr Koerner.<p>

<A HREF = https://Randall-Holmes.github.io"> Randall Holmes</A> is
the author of this page; all flames concerning its contents should be
addressed to him.  He was and one hopes will be again the manager of the NF mailing list.  
                                           His research is mostly on Jensen's NFU and extensions and on
development and application of <A HREF = ../proverpage.html>the Watson
theorem prover</A>, which uses a lambda-calculus equivalent to an
extension of NFU as its higher order logic.  This descrption of my program is outdated:  look at my main page.<P>

<A HREF = http://pobox.com/~flasheridn> Flash Sheridan</A> warns us
that his page is mostly his Newton programming stuff.

<P>
<A HREF = "http://www.math.psu.edu/jech/"> Thomas Jech </A> has worked on implementing the system of
combinatory logic TRC defined by <A HREF =
http://math.boisestate.edu/~holmes> Randall Holmes</A> in his
Ph. D. thesis and a subsequent paper under the <A HREF =
https://www.cs.unm.edu/~mccune/otter/> Otter theorem
prover</A>.



<P>
<A HREF = "mailto:pdub@accesscom.com"> Paul West </A> is an amateur
reader of set theory who has done a good deal of work on improving this page.
Look at his version of the exhaustive bibliography!  Again, I am not verifying email addresses as I update
in 2020.

<P>
<A HREF = "mailto: 73524.2215@CompuServe.COM">Isaac Malitz</A>, who
did his thesis on positive set theory, has an e-mail link here.  Again, not updated in 2020.

<P>


This is not an exhaustive list of current workers; it consists of
those for whom I have links.  In 2020, I think I should be soliciting information from a few new people. 
Workers are encouraged to send me their
e-mail addresses or home pages so I can link them in!  As of June 2020, I comment that I have checked these links and modified them in
certain cases.<p>

<P>
<A HREF = "#Contents">Back to contents</A>

<A NAME = "Definition"><H2> Definition </H2></A>

The axioms of New Foundations (hereinafter NF) are

<UL>

<LI> extensionality:  sets with the same elements are the same.

<LI> "stratified" comprehension: the set { x | P } exists when P is a
formula of first-order logic with equality and membership which can be
obtained from a well-formed formula of Russell's type theory by
ignoring the type indices (while ensuring that variables of different
types do not become identified).

<LI> Stratified comprehension is an axiom scheme, which can be
replaced with finitely many of its instances (<A HREF =
"Bibliography/setbiblio.html#Hailperin">a result of Hailperin</A>).  Using the finite
axiomatization removes the necessity of referring to types at all in
the definition of this theory.

</UL>

<P>
<A HREF = "#Contents">Back to contents</A>

<A NAME = "Paradoxes"><H2> The Paradoxes </H2></A>

These don't seem to trouble NF, though the fact that it disproves AC
(see below) is disturbing!

<UL>

<LI> Russell's paradox: "x is not an element of x" is not a stratified
predicate.  But the universe, V = { x | x = x }, does exist in NF and its
subsystems known to be consistent (see below).

<LI> The Burali-Forti paradox of the largest ordinal: Ordinals are
defined in NF as equivalence classes of well-orderings.  There is a
set of all ordinals, and it has the usual natural order, and this
order has an order type.  So far, so good.  But the order type of the
set of ordinals less than an ordinal a does not need to be equal to a
(this is proved in the usual set theory by transfinite induction on an
unstratified condition!); the order type Omega of all the ordinals is
an ordinal, but it is less than the largest ordinals.  The order type
Omega_2 of the ordinals less than Omega is less than Omega.  There is
an apparent descending sequence of ordinals Omega_i suggested here,
but it is not a set because (you guessed it) its definition is not
stratified (fortunately!).

<LI> Cantor's paradox of the largest cardinal: Cardinal numbers are
defined in NF as equivalence classes of sets of the same size.  The
form of Cantor's theorem which can be proven in Russell's type theory
asserts that the cardinality of the set of one-element subsets of A is
less than the cardinality of the power set of A.  Note that the usual
form (|A| &lt; |P(A)|) doesn't even make sense in type theory.  It makes
sense in NF, but it isn't true in all cases: for example, it wouldn't
do to have |V| &lt; |P(V)|, and indeed this is not the case, though the
set 1 of all one-element subsets of V is smaller than V (the obvious
bijection x |-&gt; {x} has an unstratified definition!).

<LI> Sets with the property that the set P1(A) of one-element subsets
of A is the same size as A are called "Cantorian" sets; sets with the
stronger property that the restriction to A of the singleton "map" x
|-&gt; {x} exists are called "strongly Cantorian" sets.  Cantorian and
strongly Cantorian sets clearly satisfy Cantor's theorem in its usual
unstratified form (|A| = |P1(A)| &lt; |P(A)|).  Strongly Cantorian (and
to a lesser extent Cantorian) sets have properties more like those of
the sets of the usual set theory than the general sets of NF (the same
remarks apply in the subsystems); for example, the relative type of a
variable restricted to a strongly Cantorian set can be freely raised
and lowered, allowing limited subversion of stratification
restrictions.  The strongly Cantorian sets can be thought of as being
"small enough" to act like the sets of ZFC.  The set of natural
numbers is provably Cantorian; the assumption that it is strongly
Cantorian, known as Rosser's Axiom of Counting, is known to strengthen
NF (if it is consistent -- one of the few independence results not
obtained by permutation methods) and known to be consistent with NFU.

<LI> Though NF is not known to be consistent, these solutions to the
paradoxes are known to work: they work exactly the same way in NFU
(New Foundations with urelements) which has well-understood models.

</UL>

<P>
<A HREF = "#Contents">Back to contents</A>

<A NAME = "Problem"><H2> The Big Problem </H2></A>

NF is not known to be consistent.  The following results are known:

<UL>

<LI>  NF disproves the Axiom of Choice
 (<A HREF = "Bibliography/setbiblio.html#Specker">Specker, 1953</A>).

<LI>  NF proves Infinity (corollary of the previous point).

<LI> NF is at least as strong as Russell's theory of types with the
Axiom of Infinity (corollary of previous point and the definition of
the theory).

<LI> No evidence exists that NF is any stronger than the theory of
types with the Axiom of Infinity.

</UL>

<A HREF = "#Contents">Back to contents</A>

<A NAME = "Consistent"><H2> Consistent subsystems </H2></A>

Certain subsystems of New Foundations are known to be consistent.
These include:

<UL>

<LI> NFU: New Foundations with urelements.  This system is consistent,
consistent with Choice, and does not prove Infinity but is consistent
with it (<A HREF = "Bibliography/setbiblio.html#Jensen"> Jensen, 1969</A>).
  NFU + Infinity + Choice has the same consistency strength as the
theory of types with the Axiom of Infinity.  Its model theory is
fairly simple and NFU can safely be extended as far as you think ZFC
can be extended.  The consistency of NFU, which has the full scheme of
stratified comprehension, shows that the comprehension scheme and
resulting presence of "big" sets is not the problem with NF.  For an
extended study of set theory in NFU, click <A HREF =
"http://www.lofs.ucl.ac.be/log/Cahiers/Cahier10.html" > here</A>.  Extensions
of NFU are adequate vehicles for mathematics in a basically familiar
style.

<LI> Extensions of NFU: Robert Solovay has shown that the
extension of NFU + Infinity + Choice with the axiom "all Cantorian
sets are strongly Cantorian" (this axiom was proposed for NF by
C. Ward Henson) has the exact strength of ZFC + "there is an n-Mahlo
cardinal" for each concrete natural number n (unpublished).  Solovay
calls this system NFUA.  Holmes has proposed stronger extensions whose
status has now been settled by Solovay and Holmes.  The system NFUB,
which adds to NFUA an axiom scheme which asserts that each definable
class of Cantorian ordinals is the intersection of some set with the
class of Cantorian ordinals, has been <A HREF =
"Bibliography/setbiblio.html#Solovay">shown by Solovay</A> to have the exact
strength of ZFC - Power Set + "there is a weakly compact cardinal".
The system NFUM, which adds to NFUB the assertion that the iterated
images of Omega (the order type of the natural order on the ordinals)
is downward cofinal in the non-cantorian ordinals, is shown by Holmes
to be equivalent to Kelley-Morse set theory plus the assertion that
there is a measure on the proper class ordinal (the description of
this theory requires care).  My paper on these results has appeared in
the JSL.<p>

Ali Enayat and Solovay have some new results relating the strength of
NFU + "the universe is finite" and some of its extensions (analogues
of NFUA, NFUB, and NFUM) to systems of arithmetic.  Enayat has also
shown that NFUA is equiconsistent with von Neumann-Godel-Bernays
predicative class theory with the proper class ordinal weakly compact.<p>

<LI> NFI: <A HREF = "Bibliography/setbiblio.html#Crabbe"> described by
Marcel Crabb&eacute; in 1983</A>, restricts comprehension to those
instances where no variable is mentioned in { x | P } of type more than
one higher than that of x.  This is a restriction on predicativity,
but NFI is still mildly impredicative.  The weaker system NFP
(predicative NF) results if one additionally forbids variables one
type higher than x from being bound in P.  NFI has strong
extensionality.  Holmes has shown that strong extensions of NFI are
consistent.

<LI> NF3: <A HREF = "Bibliography/setbiblio.html#Grishin"> described by Grishin in
 1969</A>, in which { x | P } exists if P can
be typed using no more than three types.

<LI> Other interesting fragments are mostly special subsets of those
above.  For example, NFO (NF with the formula P required to be open)
is (although this is not obvious!) a subtheory of NF3.

<LI> INF (intuitionistic NF) is being studied by
<A HREF = "Bibliography/setbiblio.html#Daniel"> Daniel Dzierzgowski</A>
at the Catholic University in Louvain-la-Neuve, but is not known to be
consistent.

<LI> Another interesting subtheory of NF (which is also a subtheory of
the usual set theory) is KF, which is the theory which one obtains
from Zermelo set theory by weakening comprehension to bounded (all
quantifiers restricted to sets) stratified formulas.  KF with Infinity
is as strong as the theory of types with infinity and represents the
intersection between bounded Zermelo set theory (MacLane set theory)
and NF.  <A HREF = http://www.dpmms.cam.ac.uk/~tf>
Thomas Forster</A> is the one to ask about this.  Adding the assertion
of the existence of the universal set to KF yields NF exactly.

</UL>

<P>
<A HREF = "#Contents">Back to contents</A>

<P>
<I>
Last revision June 10, 2020 (by Holmes).
<P>

Thanks to Paul West for refining
Holmes's html code and putting bibliographies into HTML.  
<P>
Please send all
comments and corrections to <A HREF = "mailto: holmes@math.boisestate.edu">
holmes@math.boisestate.edu</A> (Randall Holmes).