Seminar: Tuesday May 16, 2000 Carsten Butz Title: Quine's New Foundations `is' higher-order arithmetic. Abstract: If higher-order arithmetic were not a well-defined term the title of this talk would be literally true. We will show in this talk that with a little twist the statement makes sense. However, this does not mean that we are any closer to a consistency proof of New Foundations. It is well-known that Goedel-Bernays set-theory is finitely axiomatizable. In 1944 Hailperin showed in his thesis (under the direction of Rosser) that New Foundations is also finitely axiomatizable, by adapting the proof for GB. Since then a couple of other finite axiomatizations of NF have been proposed, but all are minor variations of the original one. It is generally agreed in the NF community that the finite axioms for NF are of technical nature, made up to make the proof go through. In particular, people do not understand (all of) the axioms, and this has lead to some misinterpretation of the axioms. In this talk I will give an interpretation of the axioms, and show that with some modifications the axioms are a suitable formulation of higher-order arithmetic, adapted to the fact that arithmetic looks differently if cardinals are Frege cardinals. (By this I mean that the cardinal number of a set x is the set containing all sets that are in one-to-one correspondence with x.) Our interpretation of the axioms relates nicely to the fact that NF can be axiomatized as KF ( = Mac Lane set-theory with separation restricted to stratified formulae ) plus the existence of a universal set.