# Bibliography: Set Theory with a Universal Set

## Introduction

This is a comprehensive bibliography on axiomatic set theories which have a universal set. The policy has been to put in pointers to anything that anyone doing a literature search on set theory with a universal set might hope to find. (``Completeness is all''!) This policy has been adhered to even at the cost of including articles that are obsolete, erroneous or just plain worthless. Less discouragingly, it also means that we have included numerous papers that contain results that are of interest to people who study set theories with a universal set (even when those papers do not bear on the subject directly) simply because this is a place where people who might want them could be foraging.

As we update the bibliography we gradually enlarge the set of items that have linked text. The two constraints on this of course are effort and copyright, and there is a large archive of NF-related manuscripts that are in various stages of becoming public. Some are itemised here and available publicly (linked) in electronic form; some are itemised here and are scanned but not publicly available because of copyright etc concerns; some are itemised but not even scanned. There is even a body of material not listed here - yet! Feel free to contact the managers if there is a document in the penumbra that you desire or whose existence you suspect.

At present the field includes two main areas of study:

• The positive set theory originally proposed by Helen Skala and Isaac Malitz (readers of this page may be more likely to be aware of the work of Marco Forti and others on hyperuniverses and the specific theory GPK+ formulated by Oliver Esser).

The model construction of Alonzo Church and Urs Oswald probably really belongs with NF: the models created by their technique are really best uderstood as fancy models of NF2 or NF0. If the NF bloc is to be divided into two the natural division one would reach for is the division between NF (and fragments thereof) with full extensionality, and the systems that allow distinct empty sets or urelemente. These systems arise from Jensen's consistency proof for NFU (actually of NFU + Infinity + Choice). Specker's disproof of Choice in NF shows that NF is quite different from NFU+Choice. The latter theory is perhaps best understood as a cunning way of describing a model of ZF (or rather KF) with an automorphism.

Do these areas exhaust set theory with a universal set? Perhaps not. Recent papers by Holmes (and the original papers of Andrzej Kisielewicz) on "double extension set theory" are referenced in the main body of the bibliography but not under "recent work"; the jury is still out on this system (two versions of which have been shown to be inconsistent) but it must be admitted that if the surviving version is consistent it is a set theory with a universal set. - MRH

For those unfamiliar with the field, two places to start are the New Foundations Home Page and Thomas Forster's book Set Theory with a Universal Set. A new option is afforded by the recent appearance of Holmes's elementary text.

Comments, corrections, and information about new publications should be sent to Randall Holmes. Announcements about both print and eprint publications are welcome.

This bibliography is a lineal descendent of the bibliography in Forster's thesis, which was the first attempt at a comprehensive NF bibliography, and thanks are due to Paul West, who did the first round of virtual typesetting.

Last revision: late January (by Randall Holmes), in progress (and we don't always remember to update this date when we change it).

## Recent Work

• Vu, D. [2010].
Symmetric Sets and Graph Models of Set and Multiset Theories.
Ph.D Thesis, University of Cambridge

• Tupailo, S. [2010]
Consistency of strictly impredicative NF and a little more...
Journal of Symbolic Logic 75 (4) pp. 1326-1338.

• Forster, T. E. and Holmes, M. R. [2009]
Permutation methods in NF and NFU
NF 70th anniversary volume, Cahiers du Centre de Logique, 16 2009 pp 33--76.

• Forster, T. E. and Bowler, N. [2009]
Normal Subgroups of Infinite Symmetric Groups, with an Application to Stratified Set Theory.
Journal of Symbolic Logic
74 (2009) pp 17--26.

• Forster, T. E. [2009]
A Tutorial on Constructive NF
in the NF 70th anniversary volume, Cahiers du Centre de Logique, 16 2009 pp 137--171.

• G. Dowek. [2001]
The Stratified Foundations as a theory modulo.[sic]
S. Abramsky (Ed.) Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 2044, Springer-Verlag, 2001.

• Hinnion, R. [1975], trans. by Forster, T, [2009]
Sur la théorie des ensembles de Quine.
Ph.D. thesis, ULB Brussels.
There is an annotated translation into English (prepared by Forster) available here . (It is not Hinnion's thesis that is new here but the annotated translation.)

• Solovay, R. [2008]
Correspondence describing Solovay's proof that NFU* (NFU + Counting + "every definable subclass of a strongly cantorian set is a set") is equiconsistent with Zermelo + Sigma-2 Replacement. This proof was presented in a talk at Stanford in October 2008.
http://math.berkeley.edu/~solovay/NFU_star.html

• Libert, T. [2008].
Positive Frege and its Scott-style semantics.
Math. Log. Quart. 54, No. 4, 378 – 402

• Hinnion, R. and Libert, T. [2008].
Topological Models for Extensional Partial Set Theory
Notre Dame J. Formal Logic, Volume 49, Number 1 (2008), 39-53.

• Holmes, M. Randall [2008]
Symmetry as a criterion for comprehension motivating Quine's ``New Foundations''
Studia Logica, 88, no. 2 (March 2008).

• Feferman, S. [2006]
Enriched stratified systems for the foundations of category theory,
in What is Category Theory? (G. Sica, ed.) Polimetrica, Milano (2006), 185-203.
Dr. Feferman says: ?A pdf file is available on my home page at
http://math.stanford.edu/~feferman/papers.html, item #62,
with publication data.  Also, his unpublished 1972 MS on which this is based, can be found there at item #58 (#57 also looks interesting--MRH).?

• Enayat, A. [2006]
From Bounded Arithmetic to Second Order Arithmetic via Automorphisms
Logic in Tehran, pp. 87--113, Lect. Notes Logic, 26, Assoc. Symbol. Logic, La Jolla, CA
Note: the author says "includes the core results about automorphisms relevant to NFU + "the universe is finite". The results about NFU are announced in section 5.1 (but see also the introduction)."

• Libert, T. [2008].
Positive Frege and its Scott-style semantics.
Math. Log. Quart. 54, No. 4, 378 ? 402

• Libert, T. [2006]
More studies on the axiom of comprehension
Cahiers du Centre de Logique, no. 15, Academia-Bruylant, Louvain-la-Neuve (Belgium).

• Hinnion, R. [2006]
Intensional positive set theory
Reports on Mathematical Logic, 40.

• O. Esser and T. Libert [2005]
On topological set theory
Mathematical Logic Quarterly, 51, pp. 263-273.

• Libert, T. [2005]
Models for a Paraconsistent Set Theory
Journal of Applied Logic, 3, pp. 15-41.

• Esser, Olivier [2004]
Une theorie positive des ensembles.
Cahiers du Centre de Logique, 13, Academia-Bruylant, Louvain-la-Neuve (Belgium), ISBN 2-8729-687-6.

• Libert, T. [2004]
Semantics for naïve set theory in many-valued logics, technique and historical account
in, J. van Benthem and G. Heintzmann, eds., The age of alternative logics, Kluwer, 2004.

• Crabbé, M. [2004]
Cuts and Gluts.
To appear in the Journal of Applied Non-Classical Logics. Still downloadable at www.lofs.ucl.ac.be/log/perso/Crabbe/textes/

• Crabbé, M. [2004] L'égalité et l'extensionnalité.

• Crabbé, M. [2004] Une élimination des coupures ne tolérant pas l'extensionnalité.
Note:Marcel says "Though not yet published, the [above] are connected with stratification and positive stuff"

• Enayat, Ali [2004]
Automorphisms, Mahlo Cardinals, and NFU
in Nonstandard Models of Arithmetic and Set Theory, (Enayat, A. and Kossak, R., eds.), Contemporary Mathematics, 361, American Mathematical Society. Also available here.

• Hinnion, R. [2003]
About the coexistence of classical sets with non-classical ones: a survey
Logic and Logical Philosophy, 11, pp. 79-90.

• Holmes, M. R. [2002]
Forcing in NFU and NF
in M. Crabbe, C. Michaux, and F. Point, eds., A tribute to Maurice Boffa, Belgian Mathematical Society, 2002.

• Holmes, M. R. [2001]
Foundations of mathematics in polymorphic type theory.
Topoi, 20, pp. 29-52.
NOTE: this is my official answer to the claim by certain parties on the FOM list that mathematics must be defined in terms of what we can do in ZFC...

• Holmes, M. R. [2001]
Strong axioms of infinity in NFU.
Journal of Symbolic Logic, 66, no. 1, pp. 87-116.
(brief notice of errata with corrections to appear in a future issue).

• Holmes, M. R. and Alves-Foss, J. [2001]
The Watson theorem prover.
Journal of Automated Reasoning, 26, no. 4, pp. 357-408.

## Comprehensive Bibliography

• Aczel, Peter [1988]
Non-Well-Founded Sets CSLI

Note: the connections of this material to NF studies are somewhat tangential: the reasons for interest in non-well-foundedness are different in the two areas. But there are some connections.

• Gian Aldo Antonelli [1998]
Extensional Quotients for Type Theory and the Consistency Problem for NF.
Journal of Symbolic Logic, 63, n. 1, pp. 247-61, 1998.

• Arruda, A. [1970a]
Sur les systèmes NFi de Da Costa.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 270, pp. 1081-1084.

• Arruda, A. [1970b]
Sur les systèmes NF-ω.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 270, pp. 1137-1139.

• Arruda, A. [1971]
La mathématique classique dans NF-ω.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 272, p. 1152.

• Arruda, A. and Da Costa, N.C.A. [1964]
Sur une hiérarchie de systèmes formels.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 259, pp. 2943-2945.

• Barwise, J. [1984]
Situations, sets and the axiom of foundation.
Logic Colloquium '84, ed. J. Paris, A. Wilkie, and G. Wilmers, North-Holland, pp. 21-36.

• Benes, V.E. [1954]
A partial model for NF.
Journal of Symbolic Logic 19, pp. 197-200.

• Boffa, M. [1971]
Stratified formulas in Zermelo-Fränkel set theory.
Bulletin de l'Académie Polonaise des Sciences, série Math. 19, pp. 275-280.

• Boffa, M. [1973]
Entre NF et NFU.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 277, pp. 821-822.

• Boffa, M. [1975a]
Sets equipollent to their power sets in NF.
Journal of Symbolic Logic 40, pp. 149-150.

• Boffa, M. [1975b]
On the axiomatization of NF.
Colloque international de Logique, Clermont-Ferrand 1975, pp. 157-159.

• Boffa, M. [1977a]
A reduction of the theory of types.
Set theory and hierarchy theory, Springer Lecture Notes in Mathematics 619, pp. 95-100.

• Boffa, M. [1977b]
The consistency problem for NF.
Journal of Symbolic Logic 42, pp. 215-220.

• Boffa, M. [1977c]
Modèles cumulatifs de la théorie des types.
Publications du Département de Mathématiques de l'Université de Lyon 14 (fasc. 2), pp. 9-12.

• Boffa, M. [1981]
La théorie des types et NF.
Bulletin de la Société Mathématique de Belgique (série A) 33, pp. 21-31.

• Boffa, M. [1982]
Algèbres de Boole atomiques et modelès de la théorie des types.
Cahiers du Centre de Logique (Louvain-la-neuve) 4, pp. 1-5.

• Boffa, M. [1984a]
Arithmetic and the theory of types.
Journal of Symbolic Logic 49, pp. 621-624.

• Boffa, M. [1984b]
The point on Quine's NF (with a bibliography).
TEORIA 4 (fasc. 2), pp. 3-13.

• Boffa, M. [1988]
ZFJ and the consistency problem for NF.
Jahrbuch der Kurt Gödel Gesellschaft (Wien), pp. 102-106

• Boffa, M. [1989]
A set theory with approximations.
Jahrbuch der Kurt Gödel Gesellschaft 1989, p.95-97.

• Boffa, M. [1992]
Decoration ensembliste de graphes par approximations.
Cahiers du Centre de Logique (Louvain-la-Neuve), 7 (1992), p.45-50.

• Boffa, M. and Casalegno, P. [1985]
The consistency of some 4-stratified subsystems of NF including NF3.
Journal of Symbolic Logic 50, pp. 407-411.

• Boffa, M. and Crabbé, M. [1975]
Les théorèmes 3-stratifiés de NF3.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 280, pp. 1657-1658.

• Boffa, M. and Pétry, A. [1993]
On self-membered sets in Quine's set theory NF.
Logique et Analyse 141-142, pp. 59-60.

• Church, A. [1974]
Set theory with a universal set.
Proceedings of the Tarski Symposium. Proceedings of Symposia in Pure Mathematics XXV, ed. L. Henkin, American Mathematical Society, pp. 297-308.
Reprinted in International Logic Review 15, pp. 11-23.
The managers have a photocopy of a manuscript of Church's pertaining to this material, supplied to us by the late Herb Enderton. Its copyright status is unclear so we are not posting the scan of it. Readers who want to come to grips with Church's theory should probably start with Forster's survey article. This document is also referenced in Flash Sheridan's thesis, which is listed in this bibliography.

• Cocchiarella, N.B. [1976]
A note on the definition of identity in Quine's New Foundations.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 22, pp. 195-197.

• Cocchiarella, N.B. [1985]
Frege's double-correlation thesis and Quine's set theories NF and ML
Journal of Philosophical Logic, 14, no. 4: 253-326.

• Cocchiarella, N.B. [1992a]
Cantor's power-set theorem versus Frege's double-correlation thesis
History and Philosophy of Logic, 13: 179-201.

• Cocchiarella, N.B. [1992b]
Conceptual realism versus Quine on classes and higher-order logic,
Synthese, 90: 379-436.

• Collins, G.E. [1955]
The Modelling of Zermelo Set Theories in New Foundations
Ph.D. Thesis, Cornell University, 1955.

• Coret, J. [1964]
Formules stratifiées et axiome de fondation.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 264, pp. 809-812 and 837-839.

• Coret, J. [1970]
Sur les cas stratifiés du schema de remplacement.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 271, pp. 57-60. Annotated English translation by Thomas Forster

• Crabbé, M. [1975]
Non-normalisation de ZF
Note: Marcel says "My old unpublished counterexample to normalisation of ZF might also be of interest..."

• Crabbé, M. [1973]
NF en un nombre fini d'axiomes.

• Crabbé, M. [1975]
Types ambigus.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 280, pp. 1-2. also in minutes of the meeting of the Groupe de Contacte: Algebre et Logique

• Crabbé, M. [1976]
La prédicativité dans les théories élémentaires.
Logique et Analyse 74-75-76, pp. 255-266.

• Crabbé, M. [1978a]
Ramification et prédicativité.
Logique et Analyse 84, pp. 399-419.

• Crabbé, M. [1978b]
Ambiguity and stratification.
Fundamenta Mathematicae CI, pp. 11-17.

• Crabbé, M. [1982a]
On the consistency of an impredicative subsystem of Quine's NF.
Journal of Symbolic Logic 47, pp. 131-136.

• Crabbé, M. [1982b]
À propos de 2α.
Cahiers du Centre de Logique (Louvain-la-neuve) 4, pp. 17-22.

• Crabbé, M. [1983]
On the reduction of type theory.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 29, pp. 235-237.

• Crabbé, M. [1984]
Typical ambiguity and the axiom of choice.
Journal of Symbolic Logic 49, pp. 1074-1078.

• Crabbé, M. [1986]
Le schéma d'ambiguïté en théorie des types.
Bulletin de la Société Mathématique de Belgique (série B) 38, pp. 46-57.

• Crabbé, M. [1991]
Stratification and cut-elimination.
Journal of Symbolic Logic 56, pp. 213-226

• Crabbé, M. [1992a]
On NFU.
Notre Dame Journal of Formal Logic 33, pp 112-119.

• Crabbé, M. [1992b]
Soyons positifs: la complétude de la théorie näive des ensembles.
Cahiers du Centre de Logique 1992, volume 7, pp.51-68.

• Crabbé, M. [1994]
The Hauptsatz for stratified comprehension: a semantic proof.
Mathematical Logic Quarterly 40, pp, 481-489.

• Crabbé, M. [1999]
L'axiome de l'infini dans NFU.
C. R. Acad. Sci. Paris, t. 329, Série I, p. 1033-1035, 1999.

• Crabbé, M. [2000]
On the set of atoms.
L. J. of the IGPL, 8, no. 6, pp. 751-759.

• Crabbé, M. [2000]
The rise and fall of typed sentences
Journal of Symbolic Logic, 65, no. 4, pp. 1858-1862.

• Curry, H.B. [1954]
Review of Rosser [1953a].
Bulletin of the American Mathematical Society 60, pp. 266-272

• Da Costa, N.C.A. [1964]
Sur une système inconsistent de théorie des ensembles.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 258, pp. 3144-3147.

• Da Costa, N.C.A. [1965a]
Sur les systèmes formels Ci, Ci*, Ci=, Di et NF.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 260, pp. 5427-5430.

• Da Costa, N.C.A. [1965b]
On two systems of set theory.
Proc. Koningl. Nederl. Ak. v. Wetens. (serie A) 68, pp 95-99.

• Da Costa, N.C.A. [1969]
On a set theory suggested by Dedecker and Ehresmann I and II.
Proceedings of the Japan Academy 45, pp. 880-888.

• Da Costa, N.C.A. [1971]
Remarques sur le système NF1.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 272, pp. 1149-1151.

• Da Costa, N.C.A. [1974]
Remarques sur les Calculs Cn, Cn*, Cn=, et Dn.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 278, pp. 818-821.

• G. Dowek. [2001]
The Stratified Foundations as a theory modulo.[sic]
S. Abramsky (Ed.) Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 2044, Springer-Verlag, 2001.

• Dzierzgowski, D. [1991]
Intuitionistic typical ambiguity.
Archive for Mathematical Logic 31, pp. 171-182.

• Dzierzgowski, D. [1993a]
Typical ambiguity and elementary equivalence.
Mathematical Logic Quarterly 39, pp. 436-446.

• Dzierzgowski, D. [1993b]
Le théorème d'ambiguïté et son extension à la logique intuitionniste.
Dissertation doctorale. Université catholique de Louvain, Institut de mathématique pure et appliquée.

• Dzierzgowski, D. [1995]
Models of intuitionistic TT and NF.
Journal of Symbolic Logic 60, pp. 640-653.

• Dzierzgowski, Daniel [1996]
Finite sets and natural numbers in intuitionistic TT,
Notre Dame Journal of Formal Logic. 37, no. 4 (1996), pp. 585-601.

• Dzierzgowski, Daniel [1998]
Finite sets and natural numbers in intuitionistic TT without extensionality.
Studia Logica, 61, no. 3 (November 1998), pp. 417-428.

• Enayat, A. [2006]
From Bounded Arithmetic to Second Order Arithmetic via Automorphisms
Logic in Tehran, pp. 87--113, Lect. Notes Logic, 26, Assoc. Symbol. Logic, La Jolla, CA
Note:the author says "includes the core results about automorphisms relevant to NFU + "the universe is finite". The results about NFU are announced in section 5.1 (but see also the introduction)."

• Enayat, Ali [2004]
Automorphisms, Mahlo Cardinals, and NFU
in Nonstandard Models of Arithmetic and Set Theory, (Enayat, A. and Kossak, R., eds.), Contemporary Mathematics, 361, American Mathematical Society. Also available here.

• Engeler, E. and Röhrli, H. [1969]
On the problem of foundations of category theory.
Dialectica 23, pp. 58-66.

• Esser, Olivier [1996]
Inconsistency of GPK + AFA.
Mathematical Logic Quarterly, 42, pp. 104-108.

• Esser, O. [1997]
An interpretation of ZF and KM in a positive set theory.
Mathematical Logic Quarterly 43, pp. 369-377.

• Esser, Olivier [1999]
On the consistency of a positive theory.
Mathematical Logic Quarterly, 45, no. 1, pp. 105-116.

• Esser, Olivier [2000]
Inconsistency of the axiom of choice with the positive set theory GPK + infinity.
Journal of Symbolic Logic, 65, pp. 1911-1916.

• Esser, Olivier [2003]
On the axiom of extensionality in the positive set theory.
Mathematical Logic Quarterly, 49, pp. 97-100.

• Esser, Olivier [2003]
A strong model of paraconsistent logic.
Notre Dame Journal of Formal Logic, 44.

• Esser, Olivier [2004]
Une theorie positive des ensembles.
Cahiers du Centre de Logique, 13, Academia-Bruylant, Louvain-la-Neuve (Belgium), ISBN 2-8729-687-6.

• O. Esser and T. Libert [2005]
On topological set theory
Mathematical Logic Quarterly, 51, pp. 263-273.

• Feferman, S. [1972]
Some formal systems for the unlimited theory of structures and categories.
Unpublished.

• Feferman, S. [2006]
Enriched stratified systems for the foundations of category theory,
in What is Category Theory? (G. Sica, ed.) Polimetrica, Milano (2006), 185-203.
Dr. Feferman says "A pdf file is available on my home page at
http://math.stanford.edu/~feferman/papers.html, item #62,
with publication data.  Also, my unpublished 1972 MS on which this is based, can be found there at item #58 (item #57 also looks interesting --MRH).

• Forster, T.E. [1976]
"N.F."
Ph.D. thesis, University of Cambridge.

• Forster, T.E. [1982]
Axiomatising set theory with a universal set.
Cahiers du Centre de Logique (Louvain-la-neuve) 4, pp. 61-76.

• Forster, T.E. [1983a]
Quine's New Foundations, an introduction.
Cahiers du Centre de Logique (Louvain-la-neuve) 5. 100 pp.

• Forster, T.E. [1983b]
Further consistency and independence results in NF obtained by the permutation method.
Journal of Symbolic Logic 48, pp. 236-238.

• Forster, T.E. [1985]
The status of the axiom of choice in set theory with a universal set.
Journal of Symbolic Logic 50, pp. 701-707.
(The author reports that the definition of "φ-hat" in this paper is faulty.)

• Forster, T.E. [1987a]
Permutation models in the sense of Rieger-Bernays.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 33, pp. 201-210.
(Theorem 2.3 is misstated. The correct version is theorem 3.1.30 of Forster [1992b] and [1995].)

• Forster, T.E. [1987b]
Term models for weak set theories with a universal set.
Journal of Symbolic Logic 52, pp. 374-387.

• Forster, T.E. [1989]
A second-order theory without a (second-order) model.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 35, pp. 285-286.

• Forster, T.E. [1990]
Permutation Models and Stratified Formulae, a Preservation Theorem.
Zeitschrift für Mathematische Logic und Grundlagen der Mathematik, 36 (1990) pp 385-388.

• Forster, T.E. [1992a]
On a problem of Dzierzgowski.
Bulletin de la Société Mathématique de Belgique (série B) 44, pp. 207-214.

• Forster, T.E. [1992b]
Set Theory with a Universal Set; exploring an untyped Universe
Oxford Logic Guides Clarendon Press, Oxford.

• Forster, T.E. [1993]
A semantic characterisation of the well-typed formulae of lambda calculus
Theoretical Computer Science 110, pp 405-408.

• Forster, T.E. [1994]
Why Set theory without the axiom of foundation?
Journal of Logic and Computation, 4, number 4 (August 1994) pp. 333-335.

• Forster, T. E. [1994]
Weak Systems of Set Theory Related to HOL.
(Invited talk given at the 1994 meeting of HUG) HUG94, Springer lecture notes in Computer Science 859 pp 193-204.

• Forster, T.E. [1995]
Set Theory with a Universal Set, exploring an untyped Universe
Second edition. Oxford Logic Guides, Oxford University Press, Clarendon Press, Oxford.

• Forster, T. E. [1997]
60 years of NF
The American Mathematical Monthly
104, no. 9 (November 1997), pp. 838-845. (Reprinted in Follesdal, ed: Philosophy of Quine, IV Logic, Modality and Philosophy of Mathematics) Taylor-and-Francis 2001.

• Forster, T.E. [2001]
Church's Set Theory with a Universal Set
in: Logic, Meaning and Computation: essays in memory of Alonzo Church, Synthese library 305, Kluwer, Dordrecht, Boston and London 2001.
(The linked version is to be preferred to the version in print, as I remove typos and mathematical errors from it as they come to my notice. Readers who want to learn about Church's set theory with a universal set should probably start with this article. I have some more cutting-edge stuff concerning inter alia the possibility of iterating this construction which i am writing up. I want to do some more work on it before I publish it but I am happy to show it to interested parties if asked.)

• Forster, T. E. [2001]
Translation of Specker, E.P. Dualität
(Dialectica, 12, pp 451--465; 1957) with a commentary
in Follesdal, ed: Philosophy of Quine,
IV Logic, Modality and Philosophy of Mathematics pp 7-16. Taylor-and-Francis 2001.

• Forster, T.E. [2001]
Games played on an illfounded membership relation.
in A Tribute to Maurice Boffa ed Crabbé, Point, and Michaux. (Supplement to the December 2001 number of the Bulletin of the Belgian Mathematical Society)

These games were independently rediscovered later by Denis Saveliev .

• Forster, T. E. [2003]
3 World Scientific (UK), Imperial College Press 2003.

• Forster, T. E. [2003]
ZF + Every set is the same size as a wellfounded set
Journal of Symbolic Logic,
58, (2003) pp 1-4.

• Forster, T. E. [2004]
AC fails in the natural analogues of V and L that model the stratified fragment of ZF
in Nonstandard Models of Arithmetic and Set Theory, (Enayat, A. and Kossak, R., eds.), Contemporary Mathematics,
361, American Mathematical Society.

• Forster, T. E. [2006]
Permutations and Wellfoundedness: the True Meaning of the Bizarre Arithmetic of Quine's NF
Journal of Symbolic Logic,
71 (2006) pp 227-240.

• Forster, T. E. [2007]
Implementing Mathematical Objects in Set theory
Logique et Analyse, 50 No.197 (2007)

• Forster, T. E. [2008]
The Iterative Conception of Set.
Review of Symbolic Logic, 1 (2008) pp 97-110. (This was voted one of the ten best philosophy articles of 2008 by The Philosophers' Annual!!)

• Forster, T. E. and Bowler, N. [2009]
Normal Subgroups of Infinite Symmetric Groups, with an Application to Stratified Set Theory. Journal of Symbolic Logic 74 (2009) pp 17--26.

• Forster, T. E. [2009]
A Tutorial on Constructive NF
in the NF 70th anniversary volume, Cahiers du Centre de Logique, 16 2009 pp 137--171.

• Forster, T. E. [2010]
NF at (nearly) 75. In the Special Quine number of Logique et Analyse, edited by Cresswell and Rini. 2010 pp xx--xx

• Forster, T.E. and Kaye, R. [1991]
End-extensions preserving power set.
Journal of Symbolic Logic 56, pp. 323-328.
(Errata in Forster [1992b], p. 139; repeated in Forster [1995], p. 152.)

• Forster, T. E. and Rood, C.M. [1996]
Sethood and situations.
Computational Linguistics. 22 (1996) pp 405-408.

• Forster, T. E., Holmes, M.R., and Libert, T.
``Alternative Set Theories"
in volume 6 (``Sets in the Twentieth Century'') of the Handbook of the History of Logic, Elsevier/North-Holland.

• Forster, T. E. and Esser, O.E.[2007]
Relaxing Stratification
Bull. Belg. Math. Soc. Simon Stevin, vol 14, (2007), pp. 247-258.

• Forster, T. E. and Holmes, M. R.[2009]
Permutation methods in NF and NFU.
NF 70th anniversary volume, Cahiers du Centre de Logique, vol 16 2009 pp 33--76.

• Forti, M. [1987]
Models of the generalized positive comprehension principle.
Preprint, Università di Pisa.

• Forti, M. and Hinnion, R. [1989]
The consistency problem for positive comprehension principles.
Journal of Symbolic Logic 54, pp. 1401-1418.

• Forti, M. and Honsell, F. [1983]
Set theory with free construction principles.
Annali della Scuola Normale Superiore di Pisa, Scienze fisiche e matematiche 10, pp. 493-522.

• M. Forti and F. Honsell.[1989]
Models of Selfdescriptive Set Theories.
in Partial Differential equations and the calculus of Variations, Essays in Honor of Ennio De Giorgi, I. (F. Colombini et al., eds), Birkhäuser, Boston (1989), pp. 473-518.

• Forti, M. and Honsell, F. [1992a]
Weak foundation and anti-foundation properties of positively comprehensive hyperuniverses.
Cahiers du Centre de Logique (Louvain-la-Neuve) 7, pp. 31-43.

• Forti, M. and Honsell, F. [1992b]
A general construction of hyperuniverses.
Preprint, Università di Pisa.

• M. Forti and F. Honsell.[1996]
Choice Principles in Hyperuniverses.
Annals of Pure and Applied Logic 77 (1996), pp. 35-52.

• M. Forti and F. Honsell.[1998]
Addendum and Corrigendum to "Choice Principles in Hyperuniverses".
Annals of Pure and Applied Logic 92 (1998), pp. 211-214.

• Paul C. Gilmore [1974]
The Consistency of partial Set Theory without Extensionality.
Axiomatic Set Theory, Proceedings of Symposia in Pure Mathematics, 13, part 2, AMS, Providence RI, pp.147-153.

• Paul C. Gilmore [1986]
Natural Deduction Based Set Theories: A New Resolution of the Old Paradoxes.
JSL, Vol.51, pp.393-411.

• Grishin, V.N. [1969]
Consistency of a fragment of Quine's NF system
Soviet Mathematics Doklady 10, pp. 1387-1390.

• Grishin, V.N. [1972a]
The equivalence of Quine's NF system to one of its fragments (in Russian).
Nauchno-tekhnicheskaya Informatsiya (series 2) 1, pp. 22-24.

• Grishin, V.N. [1972b]
Concerning some fragments of Quine's NF system (in Russian).
Issledovania po matematicheskoy lingvistike, matematicheskoy logike i informatsionym jazykam (Moscow), pp. 200-212.

• Grishin, V.N. [1972c]
The method of stratification in set theory (in Russian).
Ph.D. thesis, Moscow University.

• Grishin, V.N. [1973a]
The method of stratification in set theory (Abstract of Ph.D. thesis, in Russian).
Academy of Sciences of the USSR (Moscow). 9pp.

• Grishin, V.N. [1973b]
An investigation of some versions of Quine's systems.
Nauchno-tekhnicheskaya Informatsiya (series 2) 5, pp. 34-37.

• Hailperin, T. [1944]
A set of axioms for logic.
Journal of Symbolic Logic 9, pp. 1-19.

• Hatcher, W.S. [1963]
La notion d'équivalence entre systèmes formels et une généralisation du système dit "New Foundations" de Quine.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 256, pp. 563-566.

• Henson, C.W. [1969]
Finite sets in Quine's New Foundations.
Journal of Symbolic Logic 34 , pp. 589-596.

• Henson, C.W. [1973a]
Type-raising operations in NF.
Journal of Symbolic Logic 38 , pp. 59-68.

• Henson, C.W. [1973b]
Permutation methods applied to NF.
Journal of Symbolic Logic 38, pp. 69-76.

• Hiller, A.P. and Zimbarg, J.P. [1984]
Self-reference with negative types.
Journal of Symbolic Logic 49, pp. 754-773.

• Hinnion, R. and Libert, T. 2008].
Topological Models for Extensional Partial Set Theory
Notre Dame J. Formal Logic, Volume 49, Number 1 (2008), 39-53.

• Hinnion, R. [1972]
Sur les modèles de NF.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 275, p. 567.

• Hinnion, R. [1974]
Trois résultats concernant les ensembles fortement cantoriens dans les "New Foundations" de Quine.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 279, pp. 41-44.

• Hinnion, R. [1975]
Sur la théorie des ensembles de Quine.
Ph.D. thesis, ULB Brussels.
Annotated English translation by Thomas Forster.

• Hinnion, R. [1976]
Modèles de fragments de la théorie des ensembles de Zermelo-Fraenkel dans les "New Foundations" de Quine.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 282, pp. 1-3. Also in minutes of the meeting of the Groupe de Contacte: Algebre et Logique

• Hinnion, R. [1979]
Modèle constructible de la théorie des ensembles de Zermelo dans la théorie des types.
Bulletin de la Société Mathématique de Belgique (série B) 31, pp. 3-11.

• Hinnion, R. [1980]
Contraction de structures et application à NFU: Définition du "degré de non-extensionalité" d'une relation quelconque.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 290, pp. 677-680.

• Hinnion, R. [1981]
Extensional quotients of structures and applications to the study of the axiom of extensionality.
Bulletin de la Société Mathématique de Belgique (série B) 33, pp. 173-206.

• Hinnion, R. [1982]
NF et l'axiome d'universalité.
Cahiers du Centre de Logique (Louvain-la-neuve) 4, pp. 45-59.

• Hinnion, R. [1986]
Extensionality in Zermelo-Fraenkel set theory.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 32, pp. 51-60.

• Hinnion, R. [1987]
Le paradoxe de Russell dans des versions positives de la theorie naïve des ensembles
Comptes Rendus de l'Academie des Science de Paris, 304, pp. 307-310.

• Hinnion, R. [1989]
Embedding properties and anti-foundation in set theory.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 35, pp. 63-70.

• Hinnion, R. [1990]
Stratified and positive comprehension seen as superclass rules over ordinary set theory.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 36, pp. 519-534.

• Hinnion, R. [1994]
Naïve set theory with extensionality in partial logic and in paradoxical logic.
Notre Dame Journal of Formal Logic, 35, pp. 15-40..

• Hinnion, R. [2003]
About the coexistence of classical sets with non-classical ones: a survey
Logic and Logical Philosophy, 11, pp. 79-90.

• Hinnion, R. [2006]
Intensional positive set theory
Reports on Mathematical Logic, 40.

• R. Hinnion and T. Libert [2003]
Positive abstraction and extensionality
Journal of Symbolic Logic, 68, pp. 828-836.

• Holmes, M.R. [1991a]
Systems of combinatory logic related to Quine's 'New Foundations.'
Annals of Pure and Applied Logic 53, pp. 103-133.

• Holmes, M.R. [1991b]
The Axiom of Anti-Foundation in Jensen's 'New Foundations with Ur-Elements.'
Bulletin de la Société Mathématique de Belgique (série B) 43, pp. 167-179.

• Holmes, M.R. [1992]
Modelling fragments of Quine's 'New Foundations.'
Cahiers du Centre de Logique (Louvain-la-Neuve) 7, pp. 97-112.

• Holmes, M.R. [1993]
Systems of combinatory logic related to predicative and 'mildly impredicative' fragments of Quine's 'New Foundations.'
Annals of Pure and Applied Logic 59, pp 45-53.

• Holmes, M.R. [1994]
The set theoretical program of Quine succeeded (but nobody noticed).
Modern Logic 4, pp. 1-47.

• Holmes, M.R. [1995a]
The equivalence of NF-style set theories with "tangled" type theories; the construction of omega-models of predicative NF (and more).
Journal of Symbolic Logic 60, pp. 178-189.

• Holmes, M.R. [1995b]
Untyped lambda-calculus with relative typing.
Typed Lambda-Calculi and Applications (Proceedings of TLCA '95), Springer, pp. 235-248.

• Holmes, M. R. [1998]
Elementary set theory with a universal set.
volume 10 of the Cahiers du Centre de logique, Academia, Louvain-la-Neuve (Belgium), 241 pages, ISBN 2-87209-488-1. See here for an on-line errata slip. By permission of the publishers, a corrected text is published online here; an official second edition will appear online eventually.
Marcel reminds me that the official online version is at http://www.logic-center.be/cahiers/cahiersangl.html; this should be free of the errors in the original errata slip, but will not reflect more recent revisions found in the version on my site.

• Holmes, M. R. [1999]
Subsystems of Quine's ``New Foundations'' with Predicativity Restrictions
Notre Dame Journal of Formal Logic, 40, no. 2, pp. 183-196.
appeared physically in 2001.

• Holmes, M. R. and Alves-Foss, J. [2000]
A strong and mechanizable grand logic.
in Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, Lecture Notes in Computer Science, 1869, Springer-Verlag, pp. 283-300.
This is the theoretical paper on the foundations of the Watson theorem prover.

• Holmes, M. R. [2001]
Foundations of mathematics in polymorphic type theory.
Topoi, 20, pp. 29-52.
NOTE: this is my official answer to the claim by certain parties on the FOM list that mathematics must be defined in terms of what we can do in ZFC... - MRH

• Holmes, M. R. [2001]
Strong axioms of infinity in NFU.
Journal of Symbolic Logic, 66, no. 1, pp. 87-116.
(brief notice of errata with corrections to appear in a future issue).

• Holmes, M. R. [2001]
The Watson theorem prover.
Journal of Automated Reasoning, 26, no. 4, pp. 357-408.
This paper describes a theorem prover using a higher order logic based on NFU.

• Holmes, M. R. [2001]
Tarski's Theorem and NFU
in C. Anthony Anderson and M Zeleny (eds.), Logic, Meaning and Computation, Kluwer, 2001, pp. 469--478.

• Holmes, M. R. [2002]
Forcing in NFU and NF
in M. Crabbé, C. Michaux, and F. Point, eds., A tribute to Maurice Boffa, Belgian Mathematical Society, 2002.

• Holmes, M. R. [2004]
Paradoxes in double extension set theories
Studia Logica, 77 (2004), pp. 41-57.

• Holmes, M. R. [2005]
The structure of the ordinals and the interpretation of ZF in double extension set theory
Studia Logica, 79, pp. 357-372.

• Jamieson, M.W. [1994]
Set theory with a Universal Set.
Ph.D. thesis, University of Florida. 114pp.

• Jech, T. [1995]
OTTER experiments in a system of combinatory logic
Journal of Automated Reasoning, 14, pp. 413-426.

• Jensen, R.B. [1969]
On the consistency of a slight(?) modification of Quine's NF.
Synthese 19, pp. 250-263.

• Kaye, R.W. [1991]
A generalisation of Specker's theorem on typical ambiguity.
Journal of Symbolic Logic 56, pp 458-466.

• Kaye, R.W. [1996]
The quantifier complexity of NF.
Bulletin of the Belgian Mathematical Societé Simon Stevin, ISSN 1370-1444, 3, pp 301-312.

• Kemeny, J.G. [1950]
Type theory vs. set theory (abstract of Ph.D. thesis).
Journal of Symbolic Logic 15, p. 78.

• Khakhanian.
Systema NFI ravnoneprotivoretchivaya c Systema Quine NF
Online journal "Logical Studies" 8 (2002)

• Kirmayer, G. [1981]
A refinement of Cantor's theorem.
Proceedings of the American Mathematical Society 83, p. 774.

• Kisielewicz, Andrzej [1989]
Double extension set theory
Reports on Mathematical Logic 23:81--89, 1989.

• Kisielewicz, Andrzej [1998]
A very strong set theory?
Studia Logica 61:171--178, 1998.
Note: as we comment above, the jury is still out on double extension set theory; but if the remaining version of the 1998 paper is consistent it is certainly appropriate here - MRH.

• Körner, F. [1994]
Cofinal indiscernibles and some applications to New Foundations.
Mathematical Logic Quarterly 40, pp. 347-356.

• Körner, F. [1998]
Automorphisms moving all non-algebraic points and an application to NF.
Journal of Symbolic Logic 63, p. 815-830.

• Kühnrich, M. and Schultz, K. [1980]
A hierarchy of models for Skala's set theory.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 26, pp. 555-559.

• Kuzichev, A.C. [1981]
Arithmetic theories constructed on the basis of lambda-conversion.
Soviet Mathematics Doklady 24, pp. 584-589.

• Kuzichev, A.C. [1983]
Nyeprotivoretchivost' Sistema NF Quine.

In the 1980's Kuzichev produced an alleged consistency proof for NF using ideas from λ-calculus, and some attempt was made in the West to come to grips with this work (since the idea that techniques from λ-calculus might eventually prove Con(NF) is not crazy at all) but not - so far - with any success. Some manuscript translations from that era survive and have now been scanned (by Zachiri McKenzie): here is a translation into English prepared by a professional translator (not a mathematician but a friend of tf); here is another english version of (i think) the same text (possibly due to Eliot Mendelson?) and finally here is a translation into French supplied by Marcel Crabbé. The matter certainly merits investigation, but these texts come with no guarantees! - tf

• Lake, J. [1974]
Some topics in set theory.
Ph.D. thesis, Bedford College, London University.
(Lake's thesis is listed here because towards the end of it he considers the possibility of having an inhomogeneous ordered pair function in NF.)

• Lake, J. [1975]
Comparing type theory and set theory.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 21, pp. 355-356.

• Libert, T. [2004]
Semantics for naïve set theory in many-valued logics, technique and historical account
in, J. van Benthem and G. Heintzmann, eds., The age of alternative logics, Kluwer, 2004.

• Libert, T. [2005]
Models for a Paraconsistent Set Theory
Journal of Applied Logic, 3, pp. 15-41.

• Libert, T. [2006]
More studies on the axiom of comprehension
Cahiers du Centre de Logique, no. 15, Academia-Bruylant, Louvain-la-Neuve (Belgium).

• O. Esser and T. Libert [2005]
On topological set theory
Mathematical Logic Quarterly, 51, pp. 263-273.

• R. Hinnion and T. Libert [2003]
Positive abstraction and extensionality
Journal of Symbolic Logic, 68, pp. 828-836.

• McLarty, C. [1992]
Failure of cartesian closedness in NF.
Journal of Symbolic Logic 57, pp. 555-556.

• McNaughton, R. [1953]
Some formal relative consistency proofs.
Journal of Symbolic Logic 18, pp. 136-144.

• Malitz, R.J. [1976]
Set theory in which the axiom of foundation fails.
Ph.D. thesis, UCLA.

• Manakos, J. [1984]
On Skala's set theory.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 30, pp. 541-546.

• Mitchell, E. [1976]
A model of set theory with a universal set.
Ph.D. thesis, University of Wisconsin, Madison, Wisconsin.

• Oberschelp, A. [1964]
Eigentliche Klasse als Urelemente in der Mengenlehre.
Mathematische Annalen 157, pp. 234-260.

• Oberschelp, A. [1973]
Set theory over classes.
Dissertationes Mathematicae 106. 62 pp.

• Oksanen, M. [1999]
Nordic Journal of Philosophical Logic, 4, No. 1, pp. 73-93, June 1999, Scandinavian University Press.
Also available on- line at http://www.hf.uio.no/filosofi/njpl/

• Orey, S. [1955]
Formal development of ordinal number theory.
Journal of Symbolic Logic 20, pp. 95-104.

• Orey, S. [1956]
On the relative consistency of set theory.
Journal of Symbolic Logic 21, pp. 280-290.
These two papers of Orey seem to be the most publicly visible record of a project Rosser had in the 1950's (and which he wished on at least three of his Ph.D. students), namely that of the converse consistency problem: How much of ZF can we prove consistent in (or relative to) NF? How much do we have to add to NF to obtain a system in which we can prove con Z or con ZF? One idea is that instead of Gödel's L as a class of sets, one defines it instead (or rather an isomorphic copy of it) as a special binary relation on the ordinals. These two papers of Orey's seem to be concerned with this possibility. So does the thesis of Firestone, and too (we think) Collins. There is also an article of Takeuti (Journal of the Mathematical Society of Japan, 6 no 2 pp 197-220) that seems to do the same thing. (I have copies of most of these works, tho' not the Collins thesis). This needs to be investigated properly - tf

• Orey, S. [1964]
New Foundations and the axiom of counting.
Duke Mathematical Journal 31, pp. 655-660.
This paper shows how to use Specker's tie-up between NF and Type-Theory to show that the assumption that every finite set is cantorian implies Con(NF). There are ideas in this paper that still need to be worked out. It's one of the fundamental papers in NF studies - tf.

• Oswald, U. [1974]
Sur les modeles d'un fragment de NF
in in the minutes of the meeting of the Groupe de Contacte: Algebre et Logique

• Oswald, U. [1976]
Fragmente von "New Foundations" und Typentheorie.
Ph.D. thesis, ETH Zürich. 46 pp.

• Oswald, U. [1981]
Inequivalence of the fragments of New Foundations.
Archiv für mathematische Logik und Grundlagenforschung 21 pp. 77-82.

• Oswald, U. [1982]
A decision method for the existential theorems of NF2
Cahiers du Centre de Logique (Louvain-la-neuve) 4, pp. 23-43.

• Oswald, U. and Kreinovich, V. [1982]
A decision method for the Universal sentences of Quine's NF.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 28, pp. 181-187.

• Pabion, J.F. [1980]
TT3I est équivalent à l'arithmétique du second ordre.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 290, pp. 1117-1118.

• Pétry, A. [1974]
À propos des individus dans les "New Foundations" de Quine.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 279, pp. 623-624.

• Pétry, A. [1975]
Sur l'incomparabilité de certains cardinaux dans le "New Foundations" de Quine.
Comptes Rendus hebdomadaires des séances de l'Académie des Sciences de Paris (série A) 281, pp. 673-675.

• Pétry, A. [1976]
Sur les cardinaux dans le "New Foundations" de Quine.
Ph.D. thesis, University of Liège. 66 pp. electronically accessible here

• Pétry, A. [1976]
On cardinal numbers in Quine's NF.
Set theory and hierarchy theory, Bierutowice 1976, Springer Lecture Notes in Mathematics 619, pp. 241-250.

• Pétry, A. [1979]
On the typed properties in Quine's NF.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 25, pp. 99-102.

• Pétry, A. [1982]
Une charactérisation algébrique des structures satisfaisant les mêmes sentences stratifiées.
Cahiers du Centre de Logique (Louvain-la-neuve) 4, pp. 7-16.

• Pétry, A. [1992]
Stratified languages.
Journal of Symbolic Logic 57, pp. 1366-1376.

• Prati, N. [1994]
A partial model of NF with E.
Journal of Symbolic Logic 59, pp. 1245-1253.

• Quine, W.V. [1937a]
New Foundations for Mathematical Logic.
American Mathematical Monthly 44, pp. 70-80.
Reprinted in Quine [1953a]

• Quine, W.V. [1937b]
On Cantor's theorem.
Journal of Symbolic Logic 2, pp. 120-124.

• Quine, W.V. [1945]
On ordered pairs.
Journal of Symbolic Logic 10, pp. 95-96.

• Quine, W.V. [1951a]
Mathematical logic, revised ed.
Harvard University Press.

• Quine, W.V. [1951b]
On the consistency of "New Foundations."
Proceedings of the National Academy of Sciences of the USA 37, pp. 538-540.

• Quine, W.V. [1953a]
From a logical point of view.
Harper & Row.

• Quine, W.V. [1953b]
On ω-inconsistency and a so-called axiom of infinity.
Journal of Symbolic Logic 18, pp. 119-124.
Reprinted in Quine [1966] (Selected Logic Papers).

• Quine, W.V. [1963]
Set theory and its logic.
Belknap Press.

• Quine, W.V. [assorted editions]
Selected logic papers.
Random House.

• Quine, W.V. [1969]
Set theory and its logic, revised edition.
Belknap Press.

• Quine, W.V. [1993]
The Inception of NF.
Bulletin de la Société Mathématique de Belgique (série B) 45, pp. 325-328.
(This paper was written for the NF 50th anniversary meeting in Oberwolfach in 1987. It can be found in all recent editions of Quine's Selected Logic Papers.)

• Rosser, J.B. [1939a]
On the consistency of Quine's new foundations for mathematical logic.
Journal of Symbolic Logic 4, pp. 15-24.

• Rosser, J.B. [1939b]
Definition by induction in Quine's new foundations for mathematical logic.
Journal of Symbolic Logic 4, p. 80.

• Rosser, J.B. [1942]
Journal of Symbolic Logic 7, pp. 11-17.

• Rosser, J.B. [1952]
The axiom of infinity in Quine's New Foundations.
Journal of Symbolic Logic 17, pp. 238-242.

• Rosser, J.B. [1953a]
Logic for mathematicians.
McGraw-Hill. The first edition is electronically accessible here; only in the second edition do you get the appendices on the proof of Infinity and the negation of Choice, but it is a wonderful book anyway.

• Rosser, J.B. [1953b]
Deux esquisses de logique.
Paris.

• Rosser, J.B. [1954]
Review of Specker [1953].
Journal of Symbolic Logic 19, p. 127.
This can be usefully read in conjunction with Specker [1953]

• Rosser, J. B. [1956]
The relative strength of Zermelo's set theory and Quine's new foundations.
Proceedings of the International Congress of Mathematicians (Amsterdam 1954) III, pp. 289-294.

• Rosser, J. B. [1978]
Logic for mathematicians, second edition.
Chelsea Publishing.

• Rosser, J.B. and Wang, H. [1950]
Non-standard models for formal logic.
Journal of Symbolic Logic 15, pp. 113-129.

• Russell, B.A.W. [1908]
Mathematical logic as based on the theory of types.
American Journal of Mathematics 30, pp. 222-262.

• Schultz, K. [1977]
Ein Standardmodell für Skala's Mengenlehre.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 23, pp. 405-408.

• Schultz, K. [1980]
The consistency of NF.
Unpublished. (The pdf linked here was scanned by Zachiri McKenzie from a photocopied typescript in the possession of Thomas Forster, who was probably given it by Boffa.)

• Scott, D.S. [1960]
Review of Specker [1958].
Mathematical Reviews 21, p. 1026.

A very useful summary of a fundamental paper.

• Scott, D.S. [1962]
Quine's individuals.
Logic, methodology and philosophy of science, ed. E. Nagel, Stanford University Press, pp. 111-115.

• Scott, D.S. [1980]
The lambda calculus: some models, some philosophy.
The Kleene Symposium, North-Holland, pp. 116-124.

• Sharlow, Mark [2001]
Broadening the Iterative Conception of Set
Notre Dame J. Formal Logic 42, Number 3 (2001), pp 149-170.

(The abstract concludes with the words: ``It is suggested that this modified iterative conception of set supports the axioms of Quine's set theory NF.'')

• Sheridan, Flash [2014]
A Variant of Church's Set Theory with a Universal Set in which the Singleton Function is a Set.
Doctoral thesis, University of Oxford, awaiting resubmission; an abridged version will appear in Logique et Analyse, 2014. The full version is online at http://www.logic-center.be/Publications/Bibliotheque/SheridanVariantChurch.pdf. Slides for a talk summarizing the results and philosophy are at http://pobox.com/~flash/Fixing_Freges_Set_Theory.pdf.

• Skala, H. [1974a]
Eine neue Methode, die Paradoxien der naïven Mengenlehre zu vermeiden.
Annalen der Österreichen Akademie der Wissenschaften Math-Nat. Kl. II, pp. 15-16.

• Skala, H. [1974b]
An alternative way of avoiding the set-theoretical paradoxes.
Zeitschrift für mathematische Logik und Grundlagen der Mathematik 20, pp. 233-237.

• Solovay, R. [2008]
Correspondence describing Solovay's proof that NFU* (NFU + Counting + "every definable subclass of a strongly cantorian set is a set") is equiconsistent with Zermelo + Σ2 Replacement. This proof was presented in a talk at Stanford in October 2008.
http://math.berkeley.edu/~solovay/NFU_star.html

• Specker, E.P. [1953]
The axiom of choice in Quine's new foundations for mathematical logic.
Proceedings of the National Academy of Sciences of the USA 39, pp. 972-975. See also Rosser's review.

• Specker, E.P. [1958]
Dualität.
Dialectica 12, pp. 451-465.
Note: There is an annotated English translation by Forster of this important and elegant article.

• Specker, E.P. [1962]
Typical ambiguity.
Logic, methodology and philosophy of science, ed. E. Nagel, Stanford University Press, pp. 116-123.

These three papers of Specker are absolutely fundamental to NF studies.

• Stanley, R.L. [1955]
Simplified foundations for mathematical logic.
Journal of Symbolic Logic 20, pp. 123-139.

• Wang, H. [1950]
A formal system of logic.
Journal of Symbolic Logic 15, pp. 25-32.

• Wang, H. [1952]
Negative types.
MIND 61 , pp. 366-368.

• Wang, H. [1953]
The categoricity question of certain grand logics.
Mathematische Zeitschrift 59, pp. 47-56.

This paper vanished from view almost immediately because it concerns the system NF + AC, which within months of this paper appearing was shown to be inconsistent. It may be that something useful can be saved of the ideas in it, but the matter seems never to have been investigated - tf.

• Weydert, E. [1989]
How to approximate the naïve comprehension scheme inside of classical logic.
Ph.D. thesis, Friedrich-Wilhelms-Universität Bonn.
Bonner mathematische Schriften 194.

• Whitehead, A.N. and Russell, B.A.W. [1910]
Principia Mathematica. Cambridge University Press.

• Yasuhara, Mitsuru. [1984]
A finite axiomatisation of New Foundations within four types
Unpublished

• Yasuhara, Mitsuru. [1984]
A consistency proof of Quine's New Foundations
Unpublished