Workshop on History of Logics, Types and Rewriting

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.