# 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 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$".

-
David: I don't know. I simply want a reference! – Tom Leinster Dec 2 '12 at 22:14
@xuhan: I guess I'm not sure 26 letters suffice to write every word in English since I haven't read the entire OED... – François G. Dorais Dec 2 '12 at 23:15
@Xuhan. The fact is that little of EGA or SGA raises any set theoretic issues. Much of it is commutative algebra transparently formalizable in second order arithmetic. While crystalline cohomology does go beyond that, it may not go beyond third order arithmetic, and clearly is far short of arithmetic of all finite orders. The stronger claims in "arxiv.org/abs/1102.1773" are supported by arguments in the paper. – Colin McLarty Dec 3 '12 at 0:23
As Tom knows, ETCS in the original published form is proof theoretically equivalent to Zermelo set theory with the separation axiom restricted to formulas with all quantifiers bounded. That proof is published in several places. Both those theories are equivalent to the arithmetic of all finite orders. The result does follow from the result I address in arxiv.org/abs/1207.6357 but that draft is defective and I have a repair in progress. I first said the fact about finite order arithmetic is simpler than that paper, but actually I do not know it is, and anyway I do not know a reference for it. – Colin McLarty Dec 3 '12 at 0:27
@Joel David Hamkins. The place to go for intuition on set theoretic issues in ETCS is A.R.D. Mathias, 1992: "What is Mac Lane missing", in W.J.H. Judah and H.Woodin (eds), `Set Theory of the Continuum', although that paper puts ETCS into a membership-based form. The title is a joke as Adrien uses "MacLane" as the name of a set theory. In short, you cannot use induction on the natural numbers in unbounded set theoretic constructions so you can prove each transfinite cardinal has a successor but not that there are unboundedly many of them. – Colin McLarty Dec 3 '12 at 0:41

Ah, Thomas Forster's 1998 paper "Weak systems of set theory related to HOL" is available on-line at various places including https://www.dpmms.cam.ac.uk/~tf/maltapaper.ps

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.

Lake J "Comparing Type theory and Set theory" Zeitschrift fur Matematische Logik 21 1975 pp 355-56.

For a fanatically detailed proof and discussion see Mathias at https://www.dpmms.cam.ac.uk/~ardm/maclane.pdf

-
Thanks a lot, Colin, but I'm pretty confused. None of Forster, Jensen or Mathias seem to mention finite order arithmetic (or $n$th order arithmetic) by name. I haven't been able to get hold of Lake yet. Forster says that Jensen and Lake prove the equivalence of ETCS (or rather, what he calls Mac Lane set theory) with something he calls TST. But then, neither of the strings "TST" or "theory of simple types" appear in Jensen. – Tom Leinster Dec 3 '12 at 13:57
So here's my understanding. We know that ETCS is equivalent to bounded Zermelo with choice, also called Mac Lane set theory: there are plenty of references for that. Forster says that Jensen and Lake prove that Mac Lane set theory is equivalent to something that Forster calls TST (Theory of Simple Types). Jensen doesn't mention anything by this name, nor finite order arithmetic. – Tom Leinster Dec 3 '12 at 14:01
Yes. More than knowing ETCS has the strength of bounded Zermelo (which equals the strength of bounded Zermelo with choice) we have many published proofs. I did not look at Jensen or Lake. I could not get Jensen here at home. And I always like to read Mathias. ETCS is actually bi-interpretable with certain variants of bounded Z with choice, meaning they not only have the same strength but prove exactly the same theorems. The main issue there seems to be existence of transitive closures. – Colin McLarty Dec 3 '12 at 15:47
Ok, so I notice you (Colin) say "It has the proof theoretic strength of finite order arithmetic, in the sense of the simple theory of types with infinity (see Takeuti (1987, Part II))." (For others, Takeuti's book is reviewed in Zentralblatt here zentralblatt-math.org/zmath/… (first edition) and here zentralblatt-math.org/zbmath/search/?q=an%3A0609.03019 (second edition)). Where in Takeuti is it shown that TST is equivalent to finite-order arithmetic? – David Roberts Dec 4 '12 at 0:24
For Takeuti, "simple type theory" is synonymous with "higher (finite) order predicate logic," and does not include an axiom of infinity (though I think for most people simple type theory does include infinity). this is my favorite reference on simple type theory. So I call simple type theory with infinity "finite order arithmetic." – Colin McLarty Dec 4 '12 at 2:21