Alonzo Church, "A Formulation of the Simple Theory of Types," Journal of Symbolic Logic, Vol. 5, 1940, 56-68.

The author defines the syntax of simple type theory (taking negation, conjunction, and pi as primitive), abbreviations (including those for "natural numbers" [as Church numerals] from each type alpha), the rules of deduction (lambda conversion, substitution, modus ponens, and generalization), and the axioms (the expected logical axioms plus axioms giving infinity, descriptions, extensionality, and choice). He proves the deduction theorem and then examines the Peano axioms for naturals for each type a (such naturals are actually of type a'=aa(aa), as opposed to Andrew's representation at type o(oa)). These hold for i, i', i'', etc., but the successor need not be one to one for other types. He then shows how to make primitive recursive definitions for such types (the prototype example being the predecessor function). Primitive recursion involves a pairing operation on numerals (giving, of course, a higher type) and an interplay between numerals of different types (which have a correspondence given by a "translation" operator T [which uses the description operator and takes type a' to type a''] proven in the paper).