Skip to main content
1 of 5
Tom Leinster
  • 27.7k
  • 5
  • 109
  • 159

Finite order arithmetic and ETCS

I'm looking for a reference to the statement that Lawvere's Elementary Theory of the Category of Sets (ETCS) is equivalent 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, 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.

Tom Leinster
  • 27.7k
  • 5
  • 109
  • 159