Theodore Hailperin found a finite set of axioms for Quine's NF set theory. This finite axiomatization consists of a short list of particular instances of the NF axiom scheme of "stratefied comprehension." The advantage of Hailperin's alternate axiomatization is that it eliminates the necessity of referring to the concept of type in the definition of NF.

  Hailperin's article "A set of axioms for logic" [Journal of Symbolic Logic, Volume 9, Issue 1 (1944), pp. 1-19] is available online (but not for free) at:

http://tinyurl.com/yk2bsqt

Theodore Hailperin found a finite set of axioms for Quine's NF set theory. This finite axiomatization consists of a short list of particular instances of the NF axiom scheme of "stratefied comprehension." The advantage of Hailperin's alternate axiomatization is that it eliminates the necessity of referring to the concept of type in the definition of NF. See Hailperin's article "A set of axioms for logic" [Journal of Symbolic Logic, Volume 9, Issue 1 (1944), pp. 1-19].