Date: Mon, 17 Apr 89 16:14:42 BST Is it possible to have a numeral system in pure simply typed lambda calculus for which addition, multiplication, and subtraction or equality are lambda definable? This does not seem to be possible for simply typed Church numerals by the Schwichtenberg - Statman result on extended polynomials. David Wolfram.