Return to Question

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

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

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 variously known as "bounded Zermelo with choice", "restricted Zermelo with choice", and "Mac Lane set theory". (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$".

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

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?

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 variously known as "bounded Zermelo with choice", "restricted Zermelo with choice", and "Mac Lane set theory". (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$".