Report Number: CS-TR-73-330
Institution: Stanford University, Department of Computer Science
Title: Axioms and theorems for integers, lists and finite sets in LCF.
Author: Newey, Malcolm C.
Date: January 1973
Abstract: LCF (Logic for Computable Functions) is being promoted as a formal language suitable for the discussion of various problems in the Mathematical Theory of Computation (MTC). To this end, several examples of MTC problems have been formalised and proofs have been exhibited using the LCF proof-checker. However, in these examples, there has been a certain amount of ad-hoc-ery in the proofs; namely, many mathematical theorems have been assumed without proof and no axiomatisation of the mathematical domains involved was given. This paper describes a suitable mathematical environment for future LCF experiments and its axiomatic basis. The environment developed, deemed appropriate for such experiments, consists of a large body of theorems from the areas of integer arithmetic, list manipulation and finite set theory.
http://i.stanford.edu/pub/cstr/reports/cs/tr/73/330/CS-TR-73-330.pdf