Just a quick note: many, if not most, of the questions I posed yesterday about second-order arithmetic are answered in the books referenced. I've skimmed them and am still grokking the details.
These books also give nicer pairing functions than the one I came up with on my own, but it's nice to note that they're recognizably similar.
Voda's book in particular bulds up a great deal of definitional machinery, much of it geared towards computer science applications.