Ultra-Formal Verification of a Result in a System of Combinatory Logic

In the present thesis I show how to use the automated theorem prover OTTER [1] to create an ultra-formal verification of a recent result in combinatory logic. This result is a main technical lemma of M. R. Holmes [2], who found a system of combinatory logic, which he calls TRC, equivalent to Quine's set theory New Foundations [3]. The automated reasoning techniques build on those of Art Quaife [4], who showed how to use the automated theorem prover OTTER as a proof finder/verifier in set theory. I believe that this thesis provides evidence that a combinatory logic formulation of set theory is more amenable to automated theorem proving than the usual formulation in the language of set theory.

In this work I have heavily used not only OTTER, but also custom programs that I have written in a variety of languages, including Scheme, Emacs Lisp, and Java. Perhaps the most valuable aspect of my work is that it gives a very preliminary glimpse---a prototype for a prototype---of how a powerful proof-finding engine like OTTER could be combined with software for preparing, managing and organizing input and output files to provide a powerful and user-friendly environment for painlessly writing, storing, retrieving, and creating proofs that are verified on an ultra-formal level. A desirable continuation of the present work would be to design and build a mathematical integrated development environment that would do all of these things.

The result that I verify is that, in TRC, a particular term push defines a bijection from the universe to the characteristic functions (in the sense of Holmes[2]; details follow in later sections). I do this by verifying three separate statements:

First: The function defined by push is one-to-one, or more formally, TRC proves that if push x = push y then x = y.
Second: The function defined by push x is always a characteristic function.
Third: For every characteristic function y there is some x such that push x = y.

The development consists of ten definitions of terms, and sixty-five proofs. I made hundreds or thousands of OTTER runs over a period of years, sometimes letting OTTER run continuously for weeks at a time, trying different ways of building up the definition of push, exploring different branches and collecting those definitions and proofs that seemed to be leading in the right direction. Desirable continuations of this work would be to further systematize and automate this work, and perhaps to somehow collect and analyze some sort of statistics on which approaches do and do not work. It would also be desirable to produce a novel proof of a more challenging result such as Specker's theorem.
up show outline