Logic – Finite Order Arithmetic and ETCS

ct.category-theorylo.logicreference-requestset-theory

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


Further edit Maybe I can make this question more transparent to experts in non-categorical set theory. ETCS is well-known to have the same strength as the membership-based theory known as "bounded Zermelo with choice" or "restricted Zermelo with choice". (One reference: Mac Lane and Moerdijk, Sheaves in Geometry and Logic, Section VI.10.) The axioms are extensionality, empty set, pairing, union, power set, foundation, restricted comprehension, infinity, and choice. Here "restricted comprehension" means that we only consider formulas that are restricted in the sense that all quantifiers are of the form "$\forall x \in y$" or "$\exists x \in y$".

Best Answer

Ah, Thomas Forster's 1998 paper

  • Forster T. (1994) Weak systems of set theory related to HOL. In: Melham T.F., Camilleri J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. doi:10.1007/3-540-58450-1_43

is available on-line at various places including here.

He says it is proved in

  • Jensen RB, On the consistency of a slight (?) modification of Quine's NF, Synthese 19 1969 pp 25--63, doi:10.1007/978-94-010-1709-1_16

  • Lake J, Comparing Type theory and Set theory, Zeitschrift fur Matematische Logik 21 1975 pp 355-56. doi:10.1002/malq.19750210144

For a fanatically detailed proof and discussion see

Related Question