Axioms and Theorems for Integers, Lists and Finite Sets in Logic for Computable Functions (LCF)
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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. The 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.
- Theoretical Mathematics