#
**Workshop on History of Logics, Types and Rewriting**

**Heriot-Watt University, Edinburgh**

** Tuesday 5 December 2000**

http://www.cedar-forest.org/forest/events/history/

###
Quine's New Foundations (NF)

###
C. BUTZ

In the three volumes of the Principia Mathematica (1910 - 1913)
Russell and Whitehead formalised a large portion of mathematics.
However, the system used in the Principia Mathematica,
Russell's theory of ramified types (RTT),
is too complicated to serve as a serious foundations of mathematics.
Indeed, most mathematicians today favour the much simpler
Zermelo-Fraenkel set-theory (ZF).

In 1936 the logician and philosopher Quine suggestest a different system,
nowadays called New Foundations (NF),
combining positive aspects of (ZF) and of a simplified version of
Russell's ramified type theory (RTT).
New Foundations is a one-sorted theory based on
the binary membership relation,
with axioms extensionality and the comprehension scheme
restricted to so-called stratified formulae.
The theory (NF) is very powerful, but, up to today,
not known to be consistent relative to (ZF)
or any other accepted foundation for mathematics.

The first part of the talk will survey (NF) and related systems,
the second part will focus on a new finite axiomatisation of (NF)
which gives better motivation for (NF) than Quine's original axioms.