I'm trying to write down an axiomatic development of most of mathematics, and I'm wondering whether it's logically permissible to use natural numbers as subscripts before they have been defined in terms of the Peano Axioms. For instance... the idea of function is used in the Peano axioms (successor function), so clearly function has to be introduced before the Peano axioms. But the ideas of operation and sequence are closely related to the idea of a function, yet they use natural numbers either to denote the number of sets in a Cartesian product or the order of items in a list. So should those concepts come in a section about functions before the Peano axioms or afterwards? Do those "list-helper" natural numbers need to come after the Peano Axioms? Or are they simply "dummy numbers" and can thus come beforehand? I guess it comes down to whether we're okay with accepting the natural numbers for use as a pre-mathematical notion when they're not being used explicitly, sort of how the ideas of "implies" and "for every" are simply logical prerequisites. However, if you take this approach, you get into some murky waters, as the sequence idea can also be introduced in terms of a function which has the natural numbers as its domain. In that case, where numbers are the input of a function, it seems that we are using the actual natural numbers, not simply the list-helper natural numbers. Thoughts?