Forster Term Models and the Consistency of New Foundations
by
Randall Holmes
Boise State University

I will discuss a strong notion of "term model" of a set theory favored by Thomas Forster. A Forster term model of a set theory is a model which consists entirely of referents of terms {x | P(x)}, where the term contains no free variables and its existence is provided by the axiom of comprehension appropriate to the theory. It is unclear whether any theory of significant strength whose only primitives are equality and membership has Forster term models. I will discuss a consistent set theory whose Forster term models (if it has any) are models of Quine's New Foundations. This example will make it clear that existence of a Forster term model is a strong hypothesis: in this case the base theory is weaker than arithmetic and the theory of the Forster term model is at least as strong as type theory with infinity. I will state a conjecture about cut elimination in suitable higher-order logics which implies the existence of Forster term models. No result about the consistency of New Foundations is claimed!

Date received: March 9, 2005