I'm looking for a reference to the statement that Lawvere's [Elementary Theory of the Category of Sets (ETCS)](http://www.tac.mta.ca/tac/reprints/articles/11/tr11abs.html) is equal in proof-theoretic strength to finite order arithmetic. The person who informed me of this said it was well-known in certain circles, but he couldn't think of a reference. Actually, all I need is a reference to one half of the equivalence: that anything provable in finite order arithmetic is provable in ETCS. The story: I've been looking at Colin McLarty's paper [A finite order arithemetic foundation for cohomology](http://arxiv.org/abs/1102.1773), which shows that nothing stronger than finite order arithmetic is needed anywhere in EGA or SGA. I want to state that nothing stronger than ETCS is needed anywhere in EGA or SGA. To back that up with references, I therefore need something that relates ETCS to finite order arithmetic. ---- **Edit** This question has generated lots of discussion about McLarty's paper. I'm genuinely interested in that discussion, but I'd also like to emphasize that it's peripheral to my question, which is simply a reference request: where can I find it stated/proved that ETCS is equal in strength to finite order arithmetic?