Abstract

First is a quick review of axiomatic set theory, (naive, Zermelo-Fraenkel, Von Neumann-Bernays-Godel, Quine's New Foundations), focusing on how the various theories avoid Russell's paradox. Second is a quick survey of automated deduction and formal methods projects that use axiomatic set theory. Third is a description of an ongoing project to investigate the consistency problem in Quine's New Foundations (NF). There is a simple first-order theory (TRC, for "Type Restricting Combinators") that is known to be equiconsistent with NF. We report on experiments with an automated theorem prover, trying to show the inconsistency of TRC.