10
$\begingroup$

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

Improve this question
$\endgroup$
29
  • 1
    $\begingroup$ David: I don't know. I simply want a reference! $\endgroup$
    – Tom Leinster
    Commented Dec 2, 2012 at 22:14
  • 3
    $\begingroup$ @xuhan: I guess I'm not sure 26 letters suffice to write every word in English since I haven't read the entire OED... $\endgroup$
    – François G. Dorais
    Commented Dec 2, 2012 at 23:15
  • 3
    $\begingroup$ @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. $\endgroup$
    – Colin McLarty
    Commented Dec 3, 2012 at 0:23
  • 3
    $\begingroup$ 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. $\endgroup$
    – Colin McLarty
    Commented Dec 3, 2012 at 0:27
  • 2
    $\begingroup$ @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. $\endgroup$
    – Colin McLarty
    Commented Dec 3, 2012 at 0:41

1 Answer 1

Reset to default
4
$\begingroup$

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

Improve this answer
$\endgroup$
11
  • $\begingroup$ 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. $\endgroup$
    – Tom Leinster
    Commented Dec 3, 2012 at 13:57
  • $\begingroup$ 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. $\endgroup$
    – Tom Leinster
    Commented Dec 3, 2012 at 14:01
  • 1
    $\begingroup$ 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. $\endgroup$
    – Colin McLarty
    Commented Dec 3, 2012 at 15:47
  • $\begingroup$ 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? $\endgroup$
    – David Roberts ♦
    Commented Dec 4, 2012 at 0:24
  • $\begingroup$ 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." $\endgroup$
    – Colin McLarty
    Commented Dec 4, 2012 at 2:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .