FOM: Is reasoning in NF "tricky"?

[Allen Hazen]

   It shouldn't be too surprising that construction of proofs in NF is
reasonably straightforward and natural: Quine "designed" the system for
pedagogical purposes, with ease of proving standard theorems doubtless a
major desideratum.  He had learned his set theory by studying "Principia
Mathematica," and his dissertation/first book ("A System of Logistic" in
its book incarnation) had been devoted to developing a variant of type
theory.*  His sense of the "natural" in these matters, therefore, would
have been thoroughly type-theoretic.  (In the 1930s this would not have
been unusual: Tarski and Gödel both put their early works into a
type-theoretic framework, as did such logically minded philosophers as
Carnap.  My impression, for what it is worth-- I'm too young to have
first-hand knowledge-- is that ZF-style set theory only became the STANDARD
framework for workers in foundations after the Second World War.)  NF was
his effort to design a system which was rigorously formalized, allowed
standard approaches to standard material in a graduate logic/set-theory
course, avoided the known paradoxes in the same way-- apparently!-- as type
theory, and was SIMPLE: where a prime component of simplicity was
systactical-- NF is formulated in Single-sorted First Order Logic, the
language Quine calls the "canonical framework" and which has, since then,
become utterly standard in logical work.
    Source: Quine tells the story on pp. 126-127 of his autobiography, "The
Time of My Life" (MIT Press, 1985).  (The "intellectual autobiography" in
Hahn & Schilpp, eds., "The Philosophy of W.V. Quine" is less informative.)
--
   *  The framework of "A System of Logistic" is simple type theory, with
predicate types rather than functional as in Church-style HOL.  In his
later writings Quine fell in love with the set-theoretic definition of
ordered pair-- cf. section 53 of his "Word and Object" for philosophical
expression of this infatuation-- but in his first book he took the
formation of pairs and finite sequences as a primitive operation, allowing
a very elegant treatment of the theory of relations.  I wouldn't recommend
the book for use as a modern introduction to set theory-- if nothing else,
it has long been out of print, and the exposition is very
notation-dependent-- but I'm not sure it FULLY deserves its relegation to
the status of historical curiosity.